You are looking at a specific version 20070507:211210 of this paper. See the latest version.

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)
PDF
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
Creative Commons Attribution
CC BY
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.