Formal Verification of HMQV Using ASM-SPV

Model checking is widely used in the verification of security protocols. However, difficulties were often encountered when trying to formalize the complex underlying computations in security protocols. Some flaws of the security protocols, especially the ones that caused by the computations weakness, cannot be detected owing to the simple abstractions of its underlying computations. In this paper, we present a method to verify a key establishment protocol HMQV, where we propose a simple formalization of its underlying Diffie-Hellman exponentiation. The formal model of HMQV is verified by our newly released model checker ASM-SPV (Abstract State Machines-Security Protocol Verifier). Experiments show that the attacks (reported by Sarr et al.) can be found under the proposed formal model of HMQV by ASM-SPV.