Leakiness is decidable for well-founded protocols

Publikationstyp
Conference Paper
Publikationsdatum
2015
Sprache
English
Author
Fröschle, Sibylle B. orcid-logo
TORE-URI
http://hdl.handle.net/11420/11092
First published in
Lecture notes in computer science 
Number in series
9036 LNCS
Start Page
176
End Page
195
Citation
Lecture Notes in Computer Science 9036: 176-195 (2015)
Contribution to Conference
4th International Conference on Principles of Security and Trust, POST 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015 
Publisher DOI
10.1007/978-3-662-46666-7_10
Scopus ID
2-s2.0-84926685994
Publisher
Springer
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.
DDC Class
004: Informatik
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.