We provide a symbolic model for protocols using public-key encryption and hash function, and prove that this model is computationally sound: if there is an attack in the computational world, then there is an attack in the symbolic (abstract) model. Our original contribution is that we deal with the security properties, such as anonymity, which cannot be described using a single execution trace, while considering an unbounded number of sessions of the protocols in the presence of active and adaptive adversaries. Our soundness proof is different from all existing studies in that it does not require a computable parsing function from bit strings to terms. This allows us to deal with more cryptographic primitives, such as a preimage-resistant and collision-resistant hash function whose input may have different lengths. © 2012 Springer-Verlag.
CITATION STYLE
Comon-Lundh, H., Hagiya, M., Kawamoto, Y., & Sakurada, H. (2012). Computational soundness of indistinguishability properties without computable parsing. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7232 LNCS, pp. 63–79). https://doi.org/10.1007/978-3-642-29101-2_5
Mendeley helps you to discover research relevant for your work.