Paper 2007/165
Inductive Proof Method for Computational Secrecy
Arnab Roy and Anupam Datta and Ante Derek and John C. Mitchell
Abstract
We investigate inductive methods for proving secrecy properties of network protocols, in a ``computational" setting applying a probabilistic polynomial-time adversary. As in cryptographic studies, our secrecy properties assert that no probabilistic polynomial-time distinguisher can win a suitable game presented by a challenger. Our method for establishing secrecy properties uses inductive proofs of computational trace-based properties, and axioms and inference rules for relating trace-based properties to non-trace-based properties. We illustrate the method, which is formalized in a logical setting that does not require explicit reasoning about computational complexity, probability, or the possible actions of the attacker, by giving a modular proof of computational authentication and secrecy properties of the Kerberos V5 protocol.
Metadata
- Available format(s)
- Category
- Cryptographic protocols
- Publication info
- Published elsewhere. Unknown where it was published
- Contact author(s)
- arnab @ stanford edu
- History
- 2007-05-07: received
- Short URL
- https://ia.cr/2007/165
- License
-
CC BY