Typing One-to-One and One-to-Many Correspondences in Security Protocols
- Andy Gordon ,
- Alan Jeffrey
Mext-NSF-JSPS International Symposium, ISSS 2002 Tokyo, Japan, November 8-10, 2002 Revised Papers |
Published by Springer Berlin Heidelberg
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. In earlier work, we showed how to typecheck one-to-one correspondences for protocols expressed in the spi-calculus. We present a new type and e.ect system able to verify both one-to-one and one-to-many correspondences.