Analysing and Patching SPEKE in ISO/IEC
This work addresses security vulnerabilities in a widely used password-authenticated key exchange protocol, impacting standards and products like Blackberry and Entrust TruePass, with the patch being adopted into international standards.
The paper identified two new attacks on the SPEKE protocol as standardized in ISO/IEC and IEEE, including an impersonation attack and a key-malleability attack, and proposed a patched version called P-SPEKE that was formally verified to prevent these attacks and included in the 2017 revision of ISO/IEC 11770-4.
Simple Password Exponential Key Exchange (SPEKE) is a well-known Password Authenticated Key Exchange (PAKE) 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 analyse 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 (MITM) 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.