Abstract
Secrecy properties of network protocols assert that no probabilistic polynomial-time distinguisher can win a suitable game presented by a challenger. Because such properties are not determined by traceby-trace behavior of the protocol, we establish a trace-based protocol condition, suitable for inductive proofs, that guarantees a generic reduction from protocol attacks to attacks on underlying primitives. We use this condition to present a compositional inductive proof system for secrecy, and illustrate the system by giving a modular, formal proof of computational authentication and secrecy properties of Kerberos V5. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Roy, A., Datta, A., Derek, A., & Mitchell, J. C. (2007). Inductive proofs of computational secrecy. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4734 LNCS, pp. 219–234). Springer Verlag. https://doi.org/10.1007/978-3-540-74835-9_15
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
