protocols, one of which (Needham-Schroeder) is explained in detail, and to a new key management scheme based on controlled physical random functions [@Gassend03PhysicalRandomFunctions; @GassendETAL02ControlledPhysicalRandomFunctions].

Section 2 explains the key intuitions underlying the approach, using Needham Schroeder as an example. Section 3 shows the complete formalization of this example, including the statement of the security goal, and a discussion of the counterexample corresponding to the well-known attack. Section 4 gives a mathematical summary of the approach without reference to any particular modeling language that might serve as a basis for implementations in other tools, and which makes precise the assumptions underlying the model. The paper closes with an evaluation and a discussion of related work.

Knowledge Flow Basics
=====================

The key idea behind knowledge flow analysis is the observation that, at the most basic level, the purpose of a security protocol is to distribute knowledge among its legitimate participants. A protocol is flawed if it allows an intruder to learn a value that is intended to remain strictly within the legitimate principals’ pool of knowledge. To gain more intuition about knowledge flows in security applications, consider the Needham-Schroeder Public Key Protocol [@NS78] shown in Figure \[ns-diagram\].

![image](ns-flow.eps)

We have two principals, 