International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Inductive Proof Method for Computational Secrecy

Authors:
Arnab Roy
Anupam Datta
Ante Derek
John C. Mitchell
Download:
URL: http://eprint.iacr.org/2007/165
Search ePrint
Search Google
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.
BibTeX
@misc{eprint-2007-13447,
  title={Inductive Proof Method for Computational Secrecy},
  booktitle={IACR Eprint archive},
  keywords={cryptographic protocols /},
  url={http://eprint.iacr.org/2007/165},
  note={ arnab@stanford.edu 13637 received 4 May 2007},
  author={Arnab Roy and Anupam Datta and Ante Derek and John C. Mitchell},
  year=2007
}