@article{gordon2003typing,
author = {Gordon, Andy and Jeffrey, Alan},
title = {Typing Correspondence Assertions for Communication Protocols},
year = {2003},
month = {May},
abstract = {Woo and Lam propose correspondence assertions for specifying authenticity properties of security protocols. 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-2003/},
pages = {379-409},
journal = {Theoretical Computer Science},
volume = {300},
number = {1},
}