done during the final step of the protocol in which Alice creates $E_{PK(B)}(N_B)$ and forwards it to Bob. Both Alice and Bob now know the two nonces and share all other knowledge except their secret keys.

Following the flow of knowledge in the Needham-Schroeder protocol provides a crucial insight underlying our analysis method. Namely, a principal can learn a value in one of three ways; he can

[$\cdot$]{}[ ]{}

*draw* the value at the start,

*compute* it using his current knowledge, or

*learn* it by communication.

Our analysis treats the latter two ways of obtaining knowledge as equivalent. Specifically, we can think of Alice’s computing $E_{PK(B)}(A, N_A)$ as her learning it from a principal called *Encryptor* whose initial pool of values includes all possible ciphers: Alice sends the tuple $(PK(B), (A, N_A))$ to *Encryptor* who responds by sending back the encryption of $(A, N_A)$ with $PK(B)$.

Treating cryptographic primitives as principals allows us to consider the total pool of knowledge to be *fixed*. That is, the set of all values before and after the execution of a security protocol is the same; the only difference is the distribution of those values among the principals. Since we assume that principals never 