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 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.