Paper 2009/227

Computational soundness, co-induction, and encryption cycles

Daniele Micciancio

Abstract

We analyze the relation between induction, co-induction and the presence of encryption cycles in the context of computationally sound symbolic equivalence of cryptographic expressions. Our main finding is that the use of co-induction in the symbolic definition of the adversarial knowledge allows to prove unconditional soundness results that do not require syntactic restrictions, like the absence of encryption cycles. Encryption cycles are relevant only to the extent that the key recovery function associated to acyclic expressions can be shown to have a unique fix-point. So, when a cryptographic expression has no encryption cycles, the inductive (least fix-point) and co-inductive (greatest fix-point) security definitions produce the same results, and the computational soundness of the inductive definitions for acyclic expressions follows as a special case of the soundness of the co-inductive definition.

Metadata
Available format(s)
PDF PS
Category
Foundations
Publication info
Published elsewhere. Unknown where it was published
Keywords
computational soundnessco-inductiongreatest fix-pointformal methods for securitysymbolic encryptionencryption cycles
Contact author(s)
daniele @ cs ucsd edu
History
2009-05-30: received
Short URL
https://ia.cr/2009/227
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2009/227,
      author = {Daniele Micciancio},
      title = {Computational soundness, co-induction, and encryption cycles},
      howpublished = {Cryptology ePrint Archive, Paper 2009/227},
      year = {2009},
      note = {\url{https://eprint.iacr.org/2009/227}},
      url = {https://eprint.iacr.org/2009/227}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.