Correctness of protocols

Our aim now is to prove that if ${\cal C}$ can be derived in our logic from ${\cal A}$ together with (some yet-to-be-defined logic translation of) ${\cal P}$, then $\models \spec{{\cal A}}{{\cal P}}{{\cal C}}$holds. From that we can conclude a rectified version, so that we know that participants in protocols draw correct conclusions.

As we have seen, the sending of a message is modelled by adding the message to the sender's $\Once$ set of messages once-said, and to the receiver's $\Sees$ set of messages seen, and then to apply the closure as mentioned in section 4. We now define the logical equivalent of this:

 

Proof Let $\mbox{$a$}$ be $\send{P}{Q}{X}$.

Now let s be any state, and put $s' = \closure(s[\Once_P\becomes\Once_P\union\{X\},\, \Sees_Q\becomes\Sees_Q\union\{X\}])$.We have

 

Proof We prove $\rectify{{\cal A}} \allows \send{P}{Q}{X}$from ${\cal A} \allows \send{P}{Q}{X}$ with induction on X .

This is extended to finite sets of formulas: ${\cal F}$ is positive whenever the formula $\bigwedge{\cal F}$ is.

 

This follows immediately from the following lemma:

 

The proof of this lemma can be found in the appendix.

 

The following lemma follows immediately from the definition of safe.
 
We now formulate Lemma 23 for the weaker requirement of ${\cal A}$ being safe, rather than positive.

 

The proof of this lemma can be found in the appendix.

 

 

From Theorem 9 our main theorem now follows: a proof of a specification in the logic indeed ensures the right conclusions of the principals during the protocol.