On the detection of desynchronisation attacks against security protocols that use dynamic shared secrets

Many peer-to-peer security protocols in mobile communications utilise shared secrets. Synchronous storage of shared secrets is imperative for the successful operation of security protocols, as asynchronous storage of shared secrets may lead to service unavailability. Hence, update mechanisms must not only guarantee the secrecy of shared secrets, but also their synchrony. This paper addresses synchronisation weaknesses in security protocols for wireless communications. It is demonstrated that a wide range of protocols contain such weaknesses. A new class of attack, called suppress-and-desynchronise attack, is introduced that exploit these weaknesses. These new attacks desynchronise the shared secrets of principals by suppressing messages, resulting in a permanent denial of service condition. A verification system to model update mechanisms for shared secrets is introduced. Based on this verification system detection rules are developed that are able to detect synchronisation weaknesses that can be exploited by suppress-and-desynchronise attacks. Application of the detection rules to three security protocols results in the detection of hitherto unknown weaknesses. Consequently, these security protocols are susceptible to suppress-and-desynchronise attacks and details of mounting the attacks are presented. Finally, amendments to one of these protocols are proposed and application of the introduced formal system establishes the immunity of the amended protocol against suppress-and-desynchronise attacks.