Decidability of context-explicit security protocols

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.