DocumentCode :
2173474
Title :
Computationally sound compositional logic for key exchange protocols
Author :
Datta, Anupam ; Derek, Ante ; Mitchell, John C. ; Warinschi, Bogdan
Author_Institution :
Dept. Comput. Sci., Stanford Univ., CA
fYear :
0
fDate :
0-0 0
Lastpage :
334
Abstract :
We develop a compositional method for proving cryptographically sound security properties of key exchange protocols, based on a symbolic logic that is interpreted over conventional runs of a protocol against a probabilistic polynomial-time attacker. Since reasoning about an unbounded number of runs of a protocol involves induction-like arguments about properties preserved by each run, we formulate a specification of secure key exchange that is closed under general composition with steps that use the key We present formal proof rules based on this game-based condition, and prove that the proof rules are sound over a computational semantics. The proof system is used to establish security of a standard protocol in the computational model
Keywords :
computational complexity; cryptography; formal specification; protocols; computational model; computational semantics; computationally sound compositional logic; cryptographically sound security properties; formal proof rules; game-based condition; induction-like arguments; key exchange protocols; secure key exchange specification; standard protocol; symbolic logic; Access protocols; Communication standards; Communication system security; Computer networks; Computer science; Computer security; Cryptographic protocols; Cryptography; Polynomials; Probabilistic logic;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Computer Security Foundations Workshop, 2006. 19th IEEE
Conference_Location :
Venice
ISSN :
1063-6900
Print_ISBN :
0-7695-2615-2
Type :
conf
DOI :
10.1109/CSFW.2006.9
Filename :
1648728
Link To Document :
بازگشت