Modeling
Cryptographic protocols: analysis using formal methods

To describe protocols, we have so far used an intuitive representation. This presentation is in fact very ambiguous, as only the normal course of the protocol is described. In the case of the Needham-Schroeder protocol, we don't know whether the second agent tests whether the nonce received is indeed a nonce, what it does if the message is not of the expected form or, above all, what exactly the agent's "expected form" is.

The study of cryptographic protocols therefore begins with an initial modeling stage. Over the last four years or so, numerous models dedicated to protocols have been developed. The model chosen here is based on a deductive system.