Typed Multiset Rewriting Specifications of Security Protocols

13 years 4 months ago

Download www.qatar.cmu.edu

The language MSR has successfully been used in the past to prove undecidability about security protocols modeled according to the Dolev-Yao abstraction. In this paper, we revise this formalism into a flexible specification framework for complex crypto-protocols. More specifically, we equip it with an extensible typing infrastructure based on dependent types with subsorting, which elegantly captures and enforces basic relations among objects, such as between a public key and its inverse. We also introduce the notion of memory predicate, where principals can store information that survives role termination. These predicates allow specifying complex protocols structured into a coordinated collection of subprotocols. Moreover, they permit describing different attacker models using the same syntax as any other role. We demonstrate this possibility and the precision of our type system by presenting two formalizations of the Dolev-Yao intruder. We discuss two execution models for this revise...

Iliano Cervesato

Real-time Traffic