Guarantees

Guarantees about the protocol operation are established in terms of theorems proved by Isabelle. When such proofs fail, they help to point out weaknesses of the protocol and even possible bugs. This is how a new bug in a variant of the Otway-Rees protocol has been discovered in [8].

The guarantees mentioned in [8] belong to five families.

Possibility properties

are usually the first to be dealt with. The most important one consists in showing that there are traces that reach the end of the protocol. Although the model does not force agents to act, the lack of a trace proceeding from the first message to the last would indicate the protocol to have been transcribed incorrectly.

Forwarding lemmas

are stated each time an agent forwards an item that it can not decrypt. They formally express that the spy will not learn anything new by seeing that item. Their proofs are trivial.

Regularity lemmas

state that a certain item X does not belong to the set of messages available to the spy, which means that the spy can not ever get hold of X. They are usually easy to prove because stated in terms of the parts operator.

Authenticity theorems

state that some valuable pieces of information as session keys and timestamps uniquely identify their message of origin. They provide guarantees about messages encrypted by keys believed to be secret (in general an encrypted message might have been faked if the key had been lost to the spy).

Secrecy theorems

are the most difficult to prove, as they are stated in terms of the analz operator. An important one states that no session key is used to encrypt other session keys, so that the spy can not use a stolen session key to learn others. A crucial one states that if the trusted party distributes a session key to two agents which have not lost their secret keys, and if this session key is not lost to the spy, then no other agent can get hold of it.