posted on 1973-01-01, 00:00authored byIliano Cervesato
The language MSR has successfully been used in the past to prove undecidability results 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 revised version of MSR, one sequential and one parallel, and prove that the latter can be simulated by the former.