Typing One-to-One and One-to-Many Correspondences in Security Protocols

Overview

Both one-to-one and one-to-many correspondences between events, sometimes known as injective and non-injective agreements, respectively, are widely used to specify correctness properties of cryptographic protocols. This paper shows how to typecheck one-to-many correspondences. Applications include checking security protocols intended only to offer one-to-many guarantees, but also checking protocols that in fact offer stronger one-to-one guarantees, but via mechanisms, such as timestamps, beyond the scope of the type system.