The use of formal methods to analyze the correctness of cryptographic
protocols became prevalent with the development of the BAN logic in 1989
[BAN89]. In this style of analysis a set of participant's final
*beliefs* is generated from a set of initial assumptions and the
protocol messages. If these beliefs satisfy the goal of the protocol, then
the protocol is validated. Since the publication of the BAN logic, several
papers have reported problems in its use for analysis of cryptographic
protocols, including
[Mea96, Sne91, Syv93]. These reports reveal
limitations of the logic or misunderstanding and misuse of the logic.
Descendents of the BAN logic such as GNY [GNY90] and SvO
[SvO94], called BAN-style logics, overcome several of these
limitations. A recent paper, by one of the authors of this paper,
demonstrates that the published failures of belief logic analysis has been
due to the improper use of the logics and not due to limitations of the
logics
[AF97]. This fact is also discussed in [SvO96]. In
[AF97], we suggest a more formalized approach to
cryptographic protocol analysis using BAN-style logics. This approach
reduces the likelihood of improper use of the logic.

This paper extends our other work by developing a *
weakest-precondition* (wp) calculus for belief logic analysis of
cryptographic protocols. This calculus, based on the SvO logic
[SvO94], provides a methodical approach to the specification and
analysis of cryptographic protocols. The application of the techniques
outlined in this paper provides users with a clear path toward protocol
validation, avoiding many of the pitfalls of the past. The development of a
wp-calculus for authentication protocols also lends itself toward
automating the development of secure protocols given specific system
requirements, using derivational programming techniques.

Specifically, we have classified the actions performed by participants of a cryptographic protocol into eight different operations (composition, message sending, message receiving, function application, key creation, shared secret creation, message decryption and proving). For each of these operations we define not only the general wps but also specific preconditions for each of the possible predicates defined by the semantics (e.g., believing, freshness, seeing, etc.). This separate treatment of each predicate is useful given the semantic nature of the operations and the belief logics, and provides users with precise guidelines for the application of the logics. In this paper we will present the wp-calculus, the specific preconditions defined for each operation, discuss how to use the wp-calculus and demonstrate its use on exemplary protocols.

Fri Aug 1 16:00:31 PDT 1997