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.

Additional Metadata
Keywords Cryptographic protocols, Decidability, Inferences systems
Conference 5th International Conference on New Trends on in Software Methodologies, Tools and Techniques, SoMeT_06
Citation
Gagnon, F, & Mejri, M. (Mohamed). (2006). A decision procedure for structured cryptographic protocols. Presented at the 5th International Conference on New Trends on in Software Methodologies, Tools and Techniques, SoMeT_06.