@inproceedings{gordon2001typing,
author = {Gordon, Andy and Jeffrey, Alan},
title = {Typing Correspondence Assertions for Communication Protocols},
booktitle = {Seventeenth Conference on the Mathematical Foundations of Programming Semantics (MFPS 2001)},
year = {2001},
month = {November},
abstract = {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.},
publisher = {Elsevier ScienceDirect},
url = {http://approjects.co.za/?big=en-us/research/publication/typing-correspondence-assertions-for-communication-protocols-2001/},
pages = {119-140},
volume = {45},
edition = {Seventeenth Conference on the Mathematical Foundations of Programming Semantics (MFPS 2001)},
}