Appendix

Proof of Lemma 24

Considering the semantics of specification triples, it is sufficient to prove for every positive formula $\phi$ with ${\cal A} \derives \phi$ that for arbitrary s , $\transf{a}{s} \models \phi$ follows from ${\cal A} \union \predprot{a}$ positive, ${\cal A} \allows a$ and $s \models {\cal A}$.We will prove this by induction on the structure of (positive) $\phi$. We write $a=\send{A}{B}{M}$ and $s'=\transf{a}{s}$.

First, assume that for some R : $X' \in \Contents{\Sees_R}$. Then:

Now assume that for no R : $X' \in \Contents{\Sees_R}$; in particular, $X' \not\in \Contents{\Sees_{R'}}$. We want to prove that also in that case $s' \models R' \sees X' \nomath{implies} s' \models S' \oncesaid Y'$. So assume $s' \models R' \sees X'$, i.e., $X' \in \Sees'_{R'}$, and therefore $X' \in \Contents{\Sees'_{R'}}$. The only participant R' that can have $\Sees_{R'} \not= \Sees'_{R'}$ is B . From $X' \in \Contents{\Sees'_{B}}\setminus\Contents{\Sees_B}$ and $\Contents{\Sees'_{B}} = \Contents{\Sees_B}\union\Contents{M}$ we see that $X' \in \Contents{M}$, and so $\encrypt{Y'}{K}{S'} \in \Contents{M}$. Note further that $s' \models A \oncesaid M$. We now prove by induction on the structure of messages that for all M :

If $s \models {\cal A}$, ${\cal A} \allows \send{A}{B}{M}$, $\encrypt{Y'}{K}{S'} \in \Contents{M}$ and $s' \models A \oncesaid M$,
then $s \models S' \oncesaid Y'$

Since $\Sees_P$, $\Once_P$ and $\Believes_P$ are also increase, the proofs for $P \sees X$, $P \oncesaid X$, $P \believes \phi$ and $P \believes \fresh X$ are analogous.

Proof of Lemma 28

The proof is analogous to the proof of Lemma 24. According to the semantics of specification triples, it is sufficient to prove for every formula $\psi$ in ${\cal A}$ that for arbitrary s , $\transf{a}{s} \models \psi$ follows from ${\cal A} \union \predprot{a}$ safe, ${\cal A} \allows a$ and $s \models {\cal A}$.For positive $\psi \in {\cal A}$ Lemma 24 ensures that $s' \models \psi$. For $\psi = \rectify{\phi}$ (where $\phi$ is positive) we must prove that either $\rectify{\phi}$ is positive, or $s' \models \rectify{\phi}$ under the assumptions mentioned. We prove this by induction on the structure of (positive) $\phi$.Before embarging on the induction, note that formulas of each of the forms $\key{P}{Q}{K}$, $P \possesses K$, $P \sees X$ and $P \oncesaid X$ are invariant under the mapping $\rectify{\placeh}$, so that we can skip them in the case analysis.

Finally, the postponed Case  Observe that $\rectify{P\believes \fresh X} = P \rightlybelieves \fresh X = P \believes \fresh X \land \fresh X$. The first conjunct of this expression is positive, which is enough to prove our claim. The second conjunct is not positive, hence we need to prove $s' \models \fresh X$ separately.

According to the definition of $\fresh X$, we can assume:

For all $P, \phi$ : $s \models P \oncesaid (X,\phi) \implies P \believes \phi$

We have to prove:

For all $P, \phi$ : $s' \models P \oncesaid (X,\phi) \implies P \believes \phi$

Let P and $\phi$ be given. We now distinguish three cases to prove the above implication: $(X,\phi) \in \Once_P$, $(X,\phi) \not\in \Once'_P$ and finally $(X,\phi) \in \Once'_P\backslash \Once_P$. Note that it is sufficient to prove $s' \models P \believes \phi$.

For $(X,\phi) \in \Once'_P\backslash \Once_P$, we first observe that P=A (only the sender's $\Once$ set has changed). We now prove the following statement by induction on M :

If $(X,\phi) \in \Once'_A\backslash \Once_A$, $(X,\phi) \in \Contents{M}$, ${\cal A} \allows \send{A}{B}{M}$, $s \models {\cal A}$
and $s' \models A \oncesaid M$, then $s' \models A \believes \phi$.

This proves by induction the claim

If $(X,\phi) \in \Once'_A\backslash \Once_A$, $(X,\phi) \in \Contents{M}$, ${\cal A} \allows \send{A}{B}{M}$, $s \models {\cal A}$
and $s' \models A \oncesaid M$, then $s' \models A \believes \phi$.

which concludes Case $\fresh X$ of the induction of Lemma 28.