9.04.2003

Decidable subclasses of security protocols

Security protocol analysis aims to find logical flaws in protocols which lead to failures even while using perfect cryptographic mechanisms. One of the important problems is to check if a given protocol preserves secrecy. Generally security protocols turn out to be infinite state systems, the two main sources of unboundedness being the agents' ability to communicate arbitrarily long messages and the ability to generate unbounded amount of new data. It has been shown that even if only one of the above two parameters are unbounded, checking secrecy of protocols is undecidable. We prove two decidability results. We identify a subclass of protocols for which the secrecy problem is decidable assuming bounded message length. We identify a different subclass of protocols for which the secrecy problem is decidable assuming boundedly many nonces.