Analyzing and Patching SPEKE in ISO/IEC

Feng Hao*, Roberto Metere, Siamak F. Shahandashti, Changyu Dong

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

Abstract

Simple password exponential key exchange (SPEKE) is a well-known password authenticated key exchange protocol that has been used in Blackberry phones for secure messaging and Entrust's TruePass end-to-end web products. It has also been included into international standards such as ISO/IEC 11770-4 and IEEE P1363.2. In this paper, we analyze the SPEKE protocol as specified in the ISO/IEC and IEEE standards. We identify that the protocol is vulnerable to two new attacks: an impersonation attack that allows an attacker to impersonate a user without knowing the password by launching two parallel sessions with the victim, and a key-malleability attack that allows a man-in-the-middle to manipulate the session key without being detected by the end users. Both attacks have been acknowledged by the technical committee of ISO/IEC SC 27 and ISO/IEC 11770-4 revised as a result. We propose a patched SPEKE called P-SPEKE and present a formal analysis in the Applied Pi Calculus using ProVerif to show that the proposed patch prevents both attacks. The proposed patch has been included into the latest revision of ISO/IEC 11770-4 published in 2017.

Original languageEnglish
Pages (from-to)2844-2855
Number of pages12
JournalInformation Forensics and Security, IEEE Transactions on
Volume13
Issue number11
Early online date3 May 2018
DOIs
Publication statusPublished - Nov 2018

Bibliographical note

This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details

Keywords

  • key exchange
  • SPEKE
  • ISO standards
  • IEC standards
  • Pi Calculus
  • ProVerif
  • Security
  • Impersonation attack
  • key agreement
  • formal methods
  • Password-based authenticated key exchange

Cite this