Proving Functional Equivalence of Two AES Implementations Using Bounded Model Checking