Paper 2007/165 Original: eprint.iacr.org/2007/165 ↗
Inductive Proof Method for Computational Secrecy
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
- Preprint.
- History
- 2007-05-07: last updated
- 2007-05-07: published
- Short URL
- https://ia.cr/2007/165
- License
- https://creativecommons.org/licenses/by/4.0/
BibTeX
@misc{cryptoeprint:2007/165,
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},
url = {https://eprint.iacr.org/2007/165}
}