Protocol-independent secrecy
- 7 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10816011,p. 110-119
- https://doi.org/10.1109/secpri.2000.848449
Abstract
Inductive proofs of secrecy invariants for cryptographic protocols can be facilitated by separating the protocol dependent part from the protocol-independent part. Our secrecy theorem encapsulates the use of induction so that the discharge of protocol-specific proof obligations is reduced to first-order reasoning. Also, the verification conditions are modularly associated with the protocol messages. Secrecy proofs for Otway-Rees (1987) and the corrected Needham-Schroeder protocol are given.Keywords
This publication has 6 references indexed in Scilit:
- Honest ideals on strand spacesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Verifying authentication protocols in CSPIEEE Transactions on Software Engineering, 1998
- The inductive approach to verifying cryptographic protocolsJournal of Computer Security, 1998
- A logic of authenticationACM Transactions on Computer Systems, 1990
- Reasoning about belief in cryptographic protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1990
- Efficient and timely mutual authenticationACM SIGOPS Operating Systems Review, 1987