Typing Correspondence Assertions for Communication Protocols

  • Andy Gordon ,
  • Alan Jeffrey

Seventeenth Conference on the Mathematical Foundations of Programming Semantics (MFPS 2001) |

Published by Elsevier ScienceDirect

Publication | Publication

Woo and Lam propose correspondence assertions for specifying authenticity properties of security protocols. The only prior work on checking correspondence assertions depends on model-checking and is limited to finite-state systems. We propose a dependent type and effect system for checking correspondence assertions. Since it is based on type-checking, our method is not limited to finite-state systems. This paper presents our system in the simple and general setting of the π-calculus. We show how to type-check correctness properties of example communication protocols based on secure channels. In a related paper, we extend our system to the more complex and specific setting of checking cryptographic protocols based on encrypted messages sent over insecure channels.