forget values, the set of principals who know a value at the end of a protocol session subsumes the set of principals who drew the value at the beginning.

The goal of analyzing knowledge flows in a protocol is to verify that particular values never leak out of the honest participants’ pool of knowledge. In other words, *we are interested in analyzing the flow of knowledge from an intruder’s perspective*. This observation allows us to make sound simplifying assumptions that drastically reduce the effort needed to formalize a protocol in terms of knowledge flows:

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

We need not encode the flows of knowledge among the honest principals, such as the flow which allows Alice to learn $E_{PK(A)}(N_A, N_B)$ from $Encryptor$. Rather, we may assume that each honest principal draws all values in the total knowledge pool and specify protocols solely in terms of the intruders’ knowledge flows (sections \[kf-basic-defs\] and \[initial-knowledge\]).

We may model all adversaries, including the untrusted public network, with a single opponent whom we call $Oscar$. The soundness of this approach is formally proved in section \[adversary\]. Intuitively, the approach makes sense if we note that the potential adversaries will be most effective when they collaborate 