Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols

In this paper we investigate the applicability of a bottom-up evaluation strategy for a first-order fragment of affine linear logic that we introduced in Theory Prac. Log. Program. 4 (2004) 1 for the purposes of automated verification of secrecy in cryptographic protocols. Following the Proceedings of the 12th Computer Security Foundations Workshop (1999) 55, we use multi-conclusion clauses to represent the behaviour of agents in a protocol session, and we adopt the Dolev–Yao intruder model. In addition, universal quantification provides a formal and declarative way to express creation of nonces. Our approach is well suited to verifying properties which can be specified by means of minimal conditions. Unlike traditional approaches based on model checking, we can reason about parametric, infinite-state systems; thus we do not pose any limitation on the number of parallel runs of a protocol. Furthermore, our approach can be used both to find attacks and to verify secrecy for a protocol. We apply our method to analyse several classical examples of authentication protocols. Among them we consider the ffgg protocol (Proceedings of the Workshop on Formal Methods and Security Protocols (1999)). This protocol is a challenging case study in that it is free from sequential attacks, whereas it suffers from parallel attacks that occur only when at least two sessions are run in parallel. The other case studies are of the Otway–Rees protocol and several formulations of the Needham–Schroeder protocol.