Functional Correctness Proofs of Encryption Algorithms

Abstract. We discuss a collection of mechanized formal proofs of symmetric key block encryption algorithms (AES, MARS, Twofish, RC6, Serpent, IDEA, and TEA), performed in an implementation of higher order logic. For each algorithm, functional correctness, namely that decryption inverts encryption, is formally proved by a simple but effective proof methodology involving application of invertibility lemmas in the course of symbolic evaluation. Block ciphers are then lifted to the encryption of arbitrary datatypes by using modes of operation to encrypt lists of bits produced by a polytypic encoding method.

• Type: Conference
• Year: 2005
• Where: LPAR
• Authors: Jianjun Duan, Joe Hurd, Guodong Li, Scott Owens, Konrad Slind, Junxing Zhang
• Keywords: Block Encryption Algorithms, Decryption Inverts Encryption, LPAR 2005, Mechanized Formal Proofs