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.
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.)