A Decision Procedure for Structured Cryptographic Protocols

Given a cryptographic protocol, it is possible to extract an inference system modelling exactly the set of messages an active intruder can learn by manipulating this protocol. Unfortunately, there is no general proof-search procedure to test whether or not a term belongs to the theory of an inference system. This paper presents the preliminary results obtained during an attempt to circumvent this problem. First, it explains a transformation process over inference systems; then presents a decision procedure (using the transformation process) for the security of a class of cryptographic protocols, called structured protocols; and finally argues that some basic security properties are decidable for such cryptographic protocols. The security properties include secrecy and chaoticity; the results can possibly be extended to cover authentication as well.