Improving Techniques for Proving Undecidability of Checking Cryptographic Protocols

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 nonmatching 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 NeedhamSchroeder protocol, is unknown. The limitations have been observed independently and described similarly by Froschle in a recently published paper [9], 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 t...

• Type: Conference
• Year: 2008
• Where: IEEEARES
• Authors: Zhiyao Liang, Rakesh M. Verma
• Keywords: Checking, IEEEARES 2008, Open Problems, Public Key, Security Privacy