A Verification of Rijndael in HOL

We present a verification of the Rijndael symmetric block cipher in the HOL-4 theorem prover. In general, the proofs were easy: they proceeded largely by symbolic execution along with a few applications of algebraic rewrite rules, which were also easy to prove. However, the proofs depend on tight control of symbolic execution; otherwise, the problem size became too large for an interactive system. An important aspect of the formalization was to phrase Rijndael as a functional program.

gzipped Postscript PDF