Paper 2011/085

Co-induction and Computational Semantics for Public-key Encryption with Key Cycles

Mohammad Hajiabadi and Bruce M. Kapron

Abstract

We consider the computational soundness and completeness of formal indistinguishability in public-key cryptography, in the presence of key-cycles. This problem in the absence of key-cycles is addressed in [1] by Herzog. It is known from [2] that the standard notions of computational security cannot give a computationally-sound interpretation to key-cyclic expressions. However, the work of [2] takes into account formal adversaries whose knowledge set is formulated using an inductive definition. In recent work by Micciancio [3], an alternate way of specifying the knowledge set of formal adversaries is proposed, giving a co-inductive definition of security. Using this new specification, a soundness result in the presence of key-cycles is proved in the private key setting. In this paper, we explore the co-inductive definition of security in public-key cryptography, and extend the soundness result of Herzog by proving it for key-cyclic expressions. We also show that the completeness result is achievable in the absence of key-cycles with respect to any length-revealing computational encryption system. In the presence of key-cycles, we show that the completeness result does not hold even with respect to CCA-2 secrecy.