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.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com