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

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.