ﻻ يوجد ملخص باللغة العربية
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 Entrusts 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.
The B method has facilitated the development of software by specifying the design of software as abstract machines and formally verifying the correctness of the abstract machines. The quality of B abstract machines can significantly impact the qualit
Recent attacks exploiting errors in smart contract code had devastating consequences thereby questioning the benefits of this technology. It is currently highly challenging to fix errors and deploy a patched contract in time. Instant patching is espe
The various types of communication technologies and mobility features in Internet of Things (IoT) on the one hand enable fruitful and attractive applications, but on the other hand facilitates malware propagation, thereby raising new challenges on ha
Agent-technologies have been used for higher-level decision making in addition to carrying out lower-level automation and control functions in industrial systems. Recent research has identified a number of architectural patterns for the use of agents
Increasing automation and external connectivity in industrial control systems (ICS) demand a greater emphasis on software-level communication security. In this article, we propose a secure-by-design development method for building ICS applications, w