Title :
Protocol-independent secrecy
Author :
Millen, Jon ; Rueß, Harald
Author_Institution :
SRI Int., Menlo Park, CA, USA
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 :
cryptography; data privacy; inference mechanisms; protocols; cryptographic protocols; first-order reasoning; induction; inductive proof; protocol messages; protocol-independent secrecy; secrecy theorem; verification conditions; Character generation;
Conference_Titel :
Security and Privacy, 2000. S&P 2000. Proceedings. 2000 IEEE Symposium on
Conference_Location :
Berkeley, CA
Print_ISBN :
0-7695-0665-8
DOI :
10.1109/SECPRI.2000.848449
