Next: A Hierarchy of Extensional Up: Goals Discussed in Previous Previous: Goals in Algebraic Analysis

## Goals for Provable Protocols

Protocol analysis techniques are not (currently) able to provide a proof of the security, or otherwise, of an arbitrary protocol. However, Bellare and Rogaway, and others following them, have been able to design particular protocols which are proven secure in a specific sense [3,5,7]. Security in these models is based on the notion of matching conversations, an idea which seems to have been first introduced by Bird et al [6]. Roughly, a protocol is secure if a principal will successfully complete a protocol run only when the protocol partner has a `matching' conversation. The idea was also used by Diffie, Van Oorschot and Wiener [12] in their definition of a secure protocol. They give the following definition.

DVW
A secure protocol is a protocol for which the following conditions hold in all cases where one party, say Alice, executes the protocol faithfully and accepts the identity of the other:
• At the time that Alice accepts the other party's identity (before she sends or receives a subsequent message) the other party's record of the partial or full run matches Alice's record.
• It is computationally infeasible for the exchanged key if accepted by Alice to be recovered by anyone other than Alice and possibly the party whose identity Alice accepted. (This condition does not apply to authentication without key exchange.)

As well as this definition a detailed definition of what it means for protocols runs to match is also given. The first condition is intensional and concerns entity authentication. The second is extensional and concerns key establishment.

Bellare and Rogaway [3] consider a powerful (formally defined) adversary. They define a secure mutual authentication protocol as one in which two principals `accept' if they have matching conversations, but the probability of an unmatched conversation (in the presence of the powerful adversary) is negligible. The protocol that the authors present satisfies SVO1 and SVO2 but it is not clear that this is a minimal example that satisfies their definition. (The null protocol does satisfy the definition but should perhaps be excluded on the grounds that there is no possibility for any principal to accept.)

Next: A Hierarchy of Extensional Up: Goals Discussed in Previous Previous: Goals in Algebraic Analysis