Formal verification of G-PAKE using Casper/FDR2: Securing a group PAKE protocol using Casper/FDR2

Research in security of ad hoc networks consists mainly of classifications and new protocol propositions. But formal verification should also be used in order to be able to prove the properties intended for the protocols. In this paper we present our work in formally verifying the group password-based authenticated key exchange protocol proposed in 2000 by Asokan and Ginzboorg. The proposition is rather old, but in the last years the research community focused only on two-party PAKE protocols, giving very little attention to group PAKE protocols. With the help of Casper and FDR2 we prove that G-PAKE does not accomplish the specifications given by the authors. Based on our results we proposed an improved version that we validated through model checking.