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.