DocumentCode
2087997
Title
Protocol-independent secrecy
Author
Millen, Jon ; Rueß, Harald
Author_Institution
SRI Int., Menlo Park, CA, USA
fYear
2000
fDate
2000
Firstpage
110
Lastpage
119
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Security and Privacy, 2000. S&P 2000. Proceedings. 2000 IEEE Symposium on
Conference_Location
Berkeley, CA
ISSN
1081-6011
Print_ISBN
0-7695-0665-8
Type
conf
DOI
10.1109/SECPRI.2000.848449
Filename
848449
Link To Document