Leakiness is decidable for well-founded protocols
First published in
Number in series
Lecture Notes in Computer Science 9036: 176-195 (2015)
A limit to algorithmic verification of security protocols is posed by the fact that checking whether a security property such as secrecy is satisfied is undecidable in general. In this paper we introduce the class of well-founded protocols. It is designed to exclude what seems to be common to all protocols used in undecidability proofs: the protocol syntax ensures that honest information cannot be propagated unboundedly without the intruder manipulating it. We show that the secrecy property of leakiness is decidable for well-founded protocols.
More Funding Information
This work is partially supported by the Niedersächsisches Vorab of the Volkswagen Foundation and the Ministry of Science and Culture of Lower Saxony as part of the Interdisciplinary Research Center on Critical Systems Engineering for Socio-Technical Systems.