Algorithmic Problems in the Symbolic Approach to the Verification of Automatically Synthesized Cryptosystems

Automated methods can be used to generate cryptosystems by combining the primitives in an arbitrary fashion, to weed out insecure cryptosystems, and to prove the security of those that survive. In this paper, we study several algorithmic problems arising from the verification of automatically synthesized cryptosystems built from block ciphers, in a theory that includes ACUN. One of these is static equivalence to an algorithm that produces a sequence of random terms. The other is invertibility, the problem of determining whether, given an automatically synthesized cryptosystem, built from block ciphers, and the ability to compute inverses, is it always possible to compute the original plaintext from the ciphertext? We show that static equivalence to random in this theory is undecidable in general. In addition, we identify a reasonable special case for which there is a decidable condition implying security, along with an algorithm for verifying it. For invertibility, we identify a reasonable class of cryptosystems for which invertibility is equivalent to a simple syntactic condition that can be easily verified.