FORMAL VERIFICATION OF G-PAKE USING CASPER/FDR2 - Securing a Group PAKE Protocol Using Casper/FDR2

Mihai-Lica Pura, Victor Valeriu Patriciu, Ion Bica

2010

Abstract

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.

Download


Paper Citation


in Harvard Style

Pura M., Valeriu Patriciu V. and Bica I. (2010). FORMAL VERIFICATION OF G-PAKE USING CASPER/FDR2 - Securing a Group PAKE Protocol Using Casper/FDR2 . In Proceedings of the International Conference on Security and Cryptography - Volume 1: SECRYPT, (ICETE 2010) ISBN 978-989-8425-18-8, pages 299-303. DOI: 10.5220/0002980702990303

in Bibtex Style

@conference{secrypt10,
author={Mihai-Lica Pura and Victor Valeriu Patriciu and Ion Bica},
title={FORMAL VERIFICATION OF G-PAKE USING CASPER/FDR2 - Securing a Group PAKE Protocol Using Casper/FDR2},
booktitle={Proceedings of the International Conference on Security and Cryptography - Volume 1: SECRYPT, (ICETE 2010)},
year={2010},
pages={299-303},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0002980702990303},
isbn={978-989-8425-18-8},
}


in EndNote Style

TY - CONF
JO - Proceedings of the International Conference on Security and Cryptography - Volume 1: SECRYPT, (ICETE 2010)
TI - FORMAL VERIFICATION OF G-PAKE USING CASPER/FDR2 - Securing a Group PAKE Protocol Using Casper/FDR2
SN - 978-989-8425-18-8
AU - Pura M.
AU - Valeriu Patriciu V.
AU - Bica I.
PY - 2010
SP - 299
EP - 303
DO - 10.5220/0002980702990303