Specification and verification of security protocols

Security protocols describe messages exchanged by agents in a hostile environment and composed using cryptographic primitives. They are sometimes described in scientific literature using a semi-formal notation known as Alice-Bob language, which specifies the content of messages between protocol actors (agents). This syntax can be seen as a textual representation of Message Sequence Charts used in RFCs, among other places. This language is simple and concise for describing the overall flow of a protocol, but it is nevertheless ambiguous and obscures the local operations of each agent.

We have implemented a procedure for compiling Alice-Bob specifications into multi-set rewriting rules that precisely describe the operations of agents for analyzing received messages and constructing sent messages, as well as the capabilities of attackers. The translation of this intermediate language into input format (Horn clauses) for the daTac demonstrator, and subsequently for other tools, enables formal verification of protocols using narrowing procedures. The whole system, presented at LPAR’00, forms the CASRUL system, the first version of which was written at that time and which subsequently became a component of the European AVISS and its successor AVISPA.

Later, I worked with Stéphanie Delaune on similar problems (CSF’04, UNIF’04, CCS’04, JAT’06), improving in particular the CASRUL approach (narrowing) by adding explicit destructive symbols defined by equational theories and applying the basic strategy for narrowing (in the sense that this latter model allows more attacks to be detected).

This latter model also inspired studies of constrained tree automata, and, in a very different vein, membrane computations. Intuitively, the idea is that automata can be used to characterize the (infinite) set of messages that can be exchanged by a protocol. The automata model of (IJCAR’06, JAL’08 improves on that of CCS’04, and the satisfiability decision procedure for these automata models is a generalization of basic narrowing for equations to Horn clauses.