Regular Protocols and Attacks with Regular Knowledge

We prove that, if the initial knowledge of the intruder is given by a deterministic bottom-up tree automaton, then the insecurity problem for cryptographic protocols with atomic keys for a bounded number of sessions is NP-complete. We prove also that if regural languages (given by tree automata) are used in protocol descriptions to restrict the form of messages, then the insecurity problem is NexpTime-complete. Furthermore, we define a class of cryptographic protocols, called regular protocols, such that the knowledge which the intruder can gain during an unlimited number of sessions of a protocol is a regular language.

• Type: Conference
• Year: 2005
• Where: CADE
• Authors: Tomasz Truderung
• Keywords: Automated Reasoning, Bottom-up Tree Automaton, CADE 2005, Cryptographic Protocols, Insecurity Problem