Protocol independence through disjoint encryption
- 7 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
One protocol (called the primary protocol) is independent of other protocols (jointly called the secondary protocol) if the question whether the primary protocol achieves a security goal never depends on whether the secondary protocol is in use. We use multiprotocol strand spaces to prove that two cryptographic protocols are independent if they use encryption in non-overlapping ways. This theorem applies even if the protocols share public key certificates and secret key "tickets". We use the method of Guttman et al. (2000) to study penetrator paths, namely sequences of penetrator actions connecting regular nodes (message transmissions or receptions) in the two protocols. Of special interest are inbound linking paths, which lead from a message transmission in the secondary protocol to a message reception in the primary protocol. We show that bundles can be modified to remove all inbound linking paths, if encryption does not overlap in the two protocols. The resulting bundle does not depend on any activity of the secondary protocol. We illustrate this method using the Neuman-Stubblebine protocol as an example.Keywords
This publication has 19 references indexed in Scilit:
- Analysis of the Internet Key Exchange protocol using the NRL Protocol AnalyzerPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- How to prevent type flaw attacks on security protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Verifying authentication protocols: methodology and examplePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Towards a completeness result for model checking of security protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Casper: a compiler for the analysis of security protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A hierarchy of authentication specificationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Strand spaces: proving security protocols correctJournal of Computer Security, 1999
- The TLS Protocol Version 1.0Published by RFC Editor ,1999
- Internet Security Association and Key Management Protocol (ISAKMP)Published by RFC Editor ,1998
- The Kerberos Network Authentication Service (V5)Published by RFC Editor ,1993