Towards Unconditional Soundness: Computationally Complete Symbolic Attacker

Gergei Bana and Hubert Comon-Lundh

Abstract

We consider the question of the adequacy of symbolic models versus computational models for the verification of security protocols. We neither try to include properties in the symbolic model that reflect the properties of the computational primitives nor add computational requirements that enforce the soundness of the symbolic model. We propose in this paper a different approach: everything is possible in the symbolic model unless it contradicts a computational assumption. In this way, we obtain unconditional soundness almost by construction. And we do not need to assume the absence of dynamic corruption or the absence of key-cycles, which are examples of hypotheses that are always used in related works. We set the basic framework, for arbitrary cryptographic primitives and arbitrary protocols, however for trace security properties only.

Note: Corrected some typos

Available format(s)
Category
Foundations
Publication info
Published elsewhere. Full version with appendix added to publication accepted to POST'2012
Keywords
symbolic verificationcomputational soundness
Contact author(s)
bana @ math upenn edu
History
2012-09-21: last of 6 revisions
See all versions
Short URL
https://ia.cr/2012/019

CC BY

BibTeX

@misc{cryptoeprint:2012/019,
author = {Gergei Bana and Hubert Comon-Lundh},
title = {Towards Unconditional Soundness: Computationally Complete Symbolic Attacker},
howpublished = {Cryptology ePrint Archive, Paper 2012/019},
year = {2012},
note = {\url{https://eprint.iacr.org/2012/019}},
url = {https://eprint.iacr.org/2012/019}
}

Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.