Paper 2007/165

Inductive Proof Method for Computational Secrecy

Arnab Roy, Anupam Datta, Ante Derek, and John C. Mitchell


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.

Available format(s)
Cryptographic protocols
Publication info
Published elsewhere. Unknown where it was published
Contact author(s)
arnab @ stanford edu
2007-05-07: received
Short URL
Creative Commons Attribution


      author = {Arnab Roy and Anupam Datta and Ante Derek and John C.  Mitchell},
      title = {Inductive Proof Method for Computational Secrecy},
      howpublished = {Cryptology ePrint Archive, Paper 2007/165},
      year = {2007},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.