A BRICS Mini-Course
September 11 and 13, 2001
Glynn Winskel, firstname.lastname@example.org
Computer Laboratory, University of Cambridge, England
This course will introduce a, fairly elementary, 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.
The course is based on joint work with BRICS PhD student Federico Crazzolara which will appear in the proceedings of the Eighth ACM Conference on Computer and Communications Security in Philadelphia in November, 2001.