Types and effects for asymmetric cryptographic protocols
- 25 June 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
We present the first type and effect system for proving authenticity properties of security protocols based on asymmetric cryptography. The most significant new features of our type system are: (1) a separation of public types (for data possibly sent to the opponent) from tainted types (for data possibly received from the opponent) via a subtype relation; (2) trust effects, to guarantee that tainted data does not, in fact, originate from the opponent; and (3) challenge/response types to support a variety of idioms used to guarantee message freshness. We illustrate the applicability of our system via protocol examples.Keywords
This publication has 22 references indexed in Scilit:
- A compositional logic for protocol correctnessPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2005
- Authenticity by typing for security protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2005
- A semantic model for authentication protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Towards automatic verification of authentication protocols on an unbounded networkPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Authentication testsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Typing Correspondence Assertions for Communication ProtocolsElectronic Notes in Theoretical Computer Science, 2001
- Subtyping dependent typesTheoretical Computer Science, 2001
- Verifying authentication protocols in CSPIEEE Transactions on Software Engineering, 1998
- The SLam calculusPublished by Association for Computing Machinery (ACM) ,1998
- On the security of public key protocolsIEEE Transactions on Information Theory, 1983