Secrecy for Bounded Security Protocols: Disequality Tests and an Intruder with Existentials Lead to Undecidability
Informatics, Balkan Conference in (2009)
Sept. 17, 2009 to Sept. 19, 2009
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/BCI.2009.19
The complexity of the initial secrecy problem for protocols in restricted form, with bounded length messages, unbounded number of protocol sessions, bounded existentials, disequality tests and an intruder with existentials remained open. In this paper, we prove that the problem above is undecidable, using exactly the same setting and formalism as in the paper in that the problem was initially stated.To our knowledge, up to now there is no proof of undecidability of the open problem mentioned above that constructs a protocol (well-founded) in restricted form in multiset rewriting formalism.
security protocol, secrecy problem, undecidability
C. V. Bîrjoveanu, "Secrecy for Bounded Security Protocols: Disequality Tests and an Intruder with Existentials Lead to Undecidability," Informatics, Balkan Conference in(BCI), Thessaloniki, Greece, 2009, pp. 22-27.