We consider the problem of automatically verifying infinite-state cryptographic protocols. Specifically, we present an algorithm that given a finite process describing a protocol in a hostile environment (trying to force the system into a ``bad'' state) computes a model of traces on which security properties can be checked. Because of unbounded inputs from the environment, even finite processes have an infinite set of traces; the main focus of our approach is the reduction of this infinite set to a finite set by a symbolic analysis of the knowledge of the environment. Our algorithm is sound (and we conjecture complete) for protocols with shared-key encryption/decryption that use arbitrary messages as keys; further it is complete in the common and important case in which the cryptographic keys are messages of bounded size.

(This is joint work with Martín Abadi which appears in the proceedings of the 14th Computer Security Foundations Workshop (CSFW-14), IEEE, Computer Society Press, 2001.)

We introduce a, fairly elementary and hands-on, event-based approach to reasoning about security protocols. The events of a security protocol and their causal dependency can play an important role in the analysis of security properties. This insight underlies both strand spaces and the inductive method. But neither of these approaches builds up the events of a protocol in a compositional way, so that there is an informal spring from the protocol to its model. By broadening the models to certain kinds of Petri nets, a compositional event-based semantics can be given to an economical, but expressive, language for describing security protocols; so the events and dependency of a wide range of protocols are determined once and for all. The net semantics can be formally related to a transition semantics, strand spaces and inductive rules, as well as trace languages and event structures, so unifying a range of approaches, and also providing conditions under which particular, more limited, models are adequate for the analysis of protocols. The net semantics allows the derivation of general properties and proof principles which will be demonstrated in establishing secrecy and authentication properties, the latter following a diagrammatic style of proof. I'll try at the end to indicate what I see as promising research directions.

(This is based on joint work with Federico Crazzolara which appears in the proceedings of the Eighth ACM Conference on Computer and Communications Security in Philadelphia, November, 2001.)