Decidability of context-explicit security protocols

Issue title: WITS'03

Guest editors: Roberto Gorrieri

Article type: Research Article

Authors: Ramanujam, R.^{a; *} | Suresh, S.P.^{b; **}

Affiliations: [a] The Institute of Mathematical Sciences, C.I.T. Campus, Chennai 600 113, India. E-mail: jam@imsc.res.in | [b] Chennai Mathematical Institute, 92 G.N. Chetty Road, T. Nagar, Chennai 600 017, India. E-mail: spsuresh@cmi.ac.in

Correspondence: [*] Corresponding author.

Note: [**] Work done while at The Institute of Mathematical Sciences.

Abstract: An important problem in the analysis of security protocols is that of checking whether a protocol preserves secrecy, i.e., no secret owned by the honest agents is unintentionally revealed to the intruder. This problem has been proved to be undecidable in several settings. In particular, Durgin et al. prove the undecidability of the secrecy problem in the presence of an unbounded set of nonces, even when the message length is bounded. In this paper we prove that even in the presence of an unbounded set of nonces the secrecy problem is decidable for a reasonable subclass of protocols, which we call context-explicit protocols.

DOI: 10.3233/JCS-2005-13106

Journal: Journal of Computer Security, vol. 13, no. 1, pp. 135-165, 2005