Typing correspondence assertions for communication protocols

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 ass...

Full description

Saved in:
Bibliographic Details
Published in:Theoretical computer science 2003-05, Vol.300 (1), p.379-409
Main Authors: Gordon, Andrew D, Jeffrey, Alan
Format: Article
Language:English
Subjects:
Algorithmics. Computability. Computer arithmetics
Applied sciences
Computer science
control theory
systems
Exact sciences and technology
Theoretical computing
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0304-3975
1879-2294
DOI:10.1016/S0304-3975(02)00333-X