Co-Induction and Computational Semantics for Public-Key Encryption With Key Cycles
The authors 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 by Herzog. It is known from that the standard notions of computational security cannot give a computationally-sound interpretation to key-cyclic expressions. However, the work of takes into account formal adversaries whose knowledge set is formulated using an inductive definition. In recent paper by Micciancio , an alternate way of specifying the knowledge set of formal adversaries is proposed, giving a co-inductive definition of security.