The model

  We view the environment as a system consisting of a finite collection of principals. We define for a principal P a local state as a tuple $(\Believes_P,\Once_P,\Sees_P,\Keys_P)$, with the intuitive interpretation:

• $\Believes_P$, the set of formulas that P currently believes;
• $\Once_P$, the set of (sub-)messages P once said;
• $\Sees_P$, the set of messages that P has seen so far;
• $\Keys_P$, the set of keys P possesses.

It is closed if it satisfies the following (mutually defined) closure properties, each of which corresponds directly to an axiom:

1.

(Rationality) Principals believe every theorem of the logic:
$$(\derives \phi) \Rightarrow \phi \in \Believes_P$$

2.

(Believing Modus Ponens) Principals apply Modus Ponens in their beliefs:

$$(\phiimplpsi) \in \Believes_P \land \phi \in \Believes_P \Rightarrow \psi \in \Believes_P$$

3.

(Saying parts of a joint message) If a principal said a combination of messages at a certain time, then that principal said each of the messages as well:

$$(X,Y) \in \Once_P \Rightarrow X \in \Once_P \land Y \in \Once_P$$

The reverse does not hold, since the presence of a joint message in $\Once_P$ implies that both components were uttered (as a joint message) at the same time;

4.

(Saying contents of an encrypted message) If a principal said an encrypted message and believes the key is good, then that principal said the contents of the encrypted message as well:

$$\encrypt{X}{K}{P} \in \Once_P \land \key{P}{Q}{K} \in \Believes_P \Rightarrow X \in \Once_P$$

5.

(Seeing parts of a joint message) If a principal sees a joint message, that principal sees each of the messages as well:

$$(X,Y) \in \Sees_P \Rightarrow X \in \Sees_P \land Y \in \Sees_P$$

(Note that the reverse does not hold, since a joint message implies utterance of its components at the same time, i.e., within the same message.)

6.

(Awareness) If a principal sees a message, then that principal also believes he sees it:

$$X \in \Sees_P \Rightarrow (P \sees X) \in \Believes_P$$

7.

(Possessing keys of a seen key statement) If a principal sees a key statement, then that principal possesses the key mentioned:

$$\key{Q}{R}{K} \in \Sees_P \Rightarrow K \in \Keys_P$$

8.

(Possessing believed keys) If a principal believes that a certain key is a good key statement, then that principal must possess that key as well:

$$\key{Q}{R}{K} \in \Believes_P \Rightarrow K \in \Keys_P$$

9.

(Decryption) If a principal P possesses a key K , and if P sees a message X labeled with Q and encrypted with K , then P also sees X itself:

$$K \in \Keys_P \land \encrypt{X}{K}{Q} \in \Sees_P \Rightarrow X \in \Sees_P$$

(Note that there is no closure property corresponding to the axiom Good key ensures the utterer.)

The closure of a local state s is the least closed local state s' such that $s \subseteq s'$, where the ordering is obtained by component-wise lifting of the set ordering. Note that taking the closure only adds elements to the sets involved, and leaves an already closed local state unchanged.

A global state is a mapping from principals to local states (for each principal in the environment). Global states are ordered by lifting the ordering on local states. The closure of a global state s , denoted by $\closure(s)$, is defined in the obvious way. The unqualified term ``state'' will, from now on, mean a closed global state.

We consistently use the convention that for a state denoted by the variable s its local state for principal P is denoted by the tuple $(\Believes_P,\Once_P,\Sees_P,\Keys_P)$,and likewise that for a state s' its local state for principal P is denoted by the tuple $(\Believes'_P,\Once'_P,\Sees'_P,\Keys_P')$