A Meta-Notation for Protocol Analysis

Most formal approaches to security protocol analysis are based on a set of assumptions commonly referred to as the "Dolev-Yao model." In this paper, we use a multiset rewriting formalism, based on linear logic, to state the basic assumptions of this model. A characteristic of our formalism is the way that existential quantification provides a succinct way of choosing new values, such as new keys or nonces. We define a class of theories in this formalism that correspond to finite-length protocols, with a bounded initialization phase but allowing unboundedly many instances of each protocol role (e.g., client, server, initiator, or responder). Undecidability is proved for a restricted class of these protocols, and PSPACE-completeness is claimed for a class further restricted to have no new data (nonces). Since it is a fragment of linear logic, we can use our notation directly as input to linear logic tools, allowing us to do proof search for attacks with relatively little progr...

• Type: Conference
• Year: 1999
• Where: CSFW
• Authors: Iliano Cervesato, Nancy A. Durgin, Patrick Lincoln, John C. Mitchell, Andre Scedrov
• Keywords: CSFW 1999, Linear Logic, Most Formal Approaches, Multiset Rewriting Formalism, Security Privacy