Sciweavers

ICST
2009
IEEE

Proving Functional Equivalence of Two AES Implementations Using Bounded Model Checking

13 years 1 months ago
Proving Functional Equivalence of Two AES Implementations Using Bounded Model Checking
Bounded model checking--as well as symbolic equivalence checking--are highly successful techniques in the hardware domain. Recently, bit-vector bounded model checkers like CBMC have been developed that are able to check properties of (mostly low-level) software written in C. However, using these tools to check equivalence of software implementations has rarely been pursued. In this case study we tackle the problem of proving the functional equivalence of two implementations of the AES crypto-algorithm using automatic bounded model checking techniques. Cryptographic algorithms heavily rely on bit-level operations, which makes them particularly suitable for bit-precise tools like CBMC. Other software verification tools based on abstraction refinement or static analysis seem to be less appropriate for such software. We could semi-automatically prove equivalence of the first three rounds of the AES encryption routines. Moreover, by conducting a manually assisted inductive proof, we could ...
Hendrik Post, Carsten Sinz
Added 19 Feb 2011
Updated 19 Feb 2011
Type Journal
Year 2009
Where ICST
Authors Hendrik Post, Carsten Sinz
Comments (0)