loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2008 Third International Conference on Availability, Reliability and Security
Improving Techniques for Proving Undecidability of Checking Cryptographic Protocols
March 04-March 07
ISBN: 978-0-7695-3102-1
Existing undecidability proofs of checking secrecy of cryptographic protocols have the limitations of not considering protocols common in literature, which are in the form of communication sequences, since only protocols as non-matching roles are considered, and not considering an attacker who is an insider since only an outsider attacker is considered. Therefore the complexity of checking the realistic attacks, such as the attack to the public key Needham-Schroeder protocol, is unknown.The limitations have been observed independently and??described similarly by Froschle in a recently published paper, where two open problems are posted. This paper investigates these limitations, and we present a generally applicable approach by reductions with novel features from the reachability problem of 2-counter machines, and we solve the two open problems. We also prove the undecidability of checking authentication which is the first detailed proof to our best knowledge. A unique feature of the proof is to directly address the secrecy and authentication goals as defined for the public key Needham-Schroeder protocol, whose attack has motivated many researches of formal verification of security protocols.
Index Terms:
cryptographic protocol, undecidability, secrecy, authentication, insider, formal method
Citation:
Zhiyao Liang, Rakesh M Verma, "Improving Techniques for Proving Undecidability of Checking Cryptographic Protocols," ares, pp.1067-1074, 2008 Third International Conference on Availability, Reliability and Security, 2008
Usage of this product signifies your acceptance of the Terms of Use.