Computationally Sound Secrecy Proofs by Mechanized Flow Analysis

Michael Backes; Peeter Laud

Paper 2006/266

Computationally Sound Secrecy Proofs by Mechanized Flow Analysis

Michael Backes and Peeter Laud

Abstract

We present a novel approach for proving secrecy properties of security protocols by mechanized flow analysis. In contrast to existing tools for proving secrecy by abstract interpretation, our tool enjoys cryptographic soundness in the strong sense of blackbox reactive simulatability/UC which entails that secrecy properties proven by our tool are automatically guaranteed to hold for secure cryptographic implementations of the analyzed protocol, with respect to the more fine-grained cryptographic secrecy definitions and adversary models. Our tool is capable of reasoning about a comprehensive language for expressing protocols, in particular handling symmetric encryption and asymmetric encryption, and it produces proofs for an unbounded number of sessions in the presence of an active adversary. We have implemented the tool and applied it to a number of common protocols from the literature.

Metadata

Available format(s): PDF PS
Category: Cryptographic protocols
Publication info: Published elsewhere. Full version of a paper published in the proceedings of the 13th ACM Conference on Computer and Communication Security (CCS 2006)
Keywords: security analysis reactive simulatability
Contact author(s): peeter laud @ ut ee
History: 2006-08-10: received
Short URL: https://ia.cr/2006/266
License: CC BY

BibTeX

@misc{cryptoeprint:2006/266,
      author = {Michael Backes and Peeter Laud},
      title = {Computationally Sound Secrecy Proofs by Mechanized Flow Analysis},
      howpublished = {Cryptology {ePrint} Archive, Paper 2006/266},
      year = {2006},
      url = {https://eprint.iacr.org/2006/266}
}