Typed Multiset Rewriting Specifications of Security Protocols

摘要

When it comes to security protocol analysis, the devil lies in the detail . . . or more precisely in how they are expressed. This report collects the formal definition of MSR 2.0, an unambiguous, flexible, powerful and relatively simple specification framework for cryptographic security protocols. MSR 2.0 is a strongly typed multiset rewriting language over first-order atomic formulas. It uses existential quantifiers to model the generation of fresh data and memory predicates to encode systems consisting of a collection of coordinated subprotocols. Its typing infrastructure, based on the theory of dependent types with subsorting, supports type-checking and data access validation, a static check that is shown to be intimately connected to the Dolev-Yao model. We show that MSR 2.0's dynamic semantics preserves typing and data access validy. We also provide a formal proof that the Dolev-Yao intruder can emulate any attacker that can be specified within the Dolev-Yao model of security, a fundamental assumption of many verification tools that however had never been proved before. We conclude with three specifications of increasing sophistication, starting with the classic Needham-Schroeder public-key authentication protocol and ending with the complex manipulations involved in the OFT group key management protocol.