Computational soundness, co-induction, and encryption cycles

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 soundness results without the need to require syntactic restrictions, like the absence of encryption cycles, common to most previous work in the area. Encryption cycles are relevant only to the extent that the key recovery function associated to acyclic expressions can be shown to have a unique fixed point. So, when a cryptographic expression has no encryption cycles, the inductive (least fixed point) and co-inductive (greatest fixed 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. © 2010 Springer-Verlag.