Formal Analysis of Random Nonce Misuses in Cryptographic Protocols

Cryptographic protocols commonly use (random) nonces to guarantee security properties. Although it is known for a long time that nonces should benefit from clear security properties, modern standards regularly miss this fundamental requirement. The lack of clear recommendations leads to error-prone cryptographic implementations, especially vulnerabilities due to nonce reuse and nonce leakage. This paper introduces a method based on TAMARIN to identify with a systematic approach the nonce-related properties an implementation should guarantee to ensure the security of a cryptographic protocol. As a corollary, the method also determines the security impact of a nonce misuse. Our method also applies to other types of random values used in protocols, namely ephemeral keys, masks, and nonces used in randomized primitives. This approach is then extended to take into account the well-known weaknesses of some randomized primitives when nonces are reused. The paper finally applies the method to real-life cryptographic protocols, discovering so new vulnerabilities related to nonce misuses in Dragonfly, WPA3, and Bluetooth.