Automated Protocol Verification in Linear Logic

In this paper we investigate the applicability of a bottom-up evaluation strategy for a first order fragment of linear logic for the purposes of automated validation of authentication protocols. We use multi-conclusion clauses to represent the behaviour of agents in a protocol session, and we adopt the Dolev-Yao intruder model and related message and cryptographic assumptions. Also, we use universal quantification to provide a logical and clean way to express creation of nonces. Our approach is well suited to verify properties which can be specified by means of minimality 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 given protocol. Furthermore, our approach can be used both to find attacks and to prove correctness of protocols. We present some preliminary experiments which we have carried out using the above approach. In particular, we analyze the ffgg protocol introduced by Millen. 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