# Formal Analysis of Random Nonce Misuses in Cryptographic Protocols

Gildas Avoine, Tristan Claverie, Stéphanie Delaune

► To cite this version:

Gildas Avoine, Tristan Claverie, Stéphanie Delaune. Formal Analysis of Random Nonce Misuses in Cryptographic Protocols. 38th IEEE Computer Security Foundations Symposium (CSF 2025), Jun 2025, Santa Cruz, CA, United States. 10.1109/CSF64896.2025.00037. hal-05066621

HAL Id: hal-05066621

https://hal.science/hal-05066621v1

Submitted on 18 May 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Formal Analysis of Random Nonce Misuses in
Cryptographic Protocols

Gildas Avoine

INSA Rennes, Univ Rennes, CNRS, IRISA, IUF

Rennes, France

gildas.avoine@irisa.fr

Tristan Claverie

ANSSI, INSA Rennes, IRISA

Rennes, France

tristan.claverie@ssi.gouv.fr

Stéphanie Delaune

Univ Rennes, CNRS, IRISA

Rennes, France

stephanie.delaune@irisa.fr

*Abstract*—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.

# I. INTRODUCTION

In this section, we first review the concept of nonces and discuss common implementation issues, before presenting related work and outlining our contributions.

## A. Concept of nonce in the protocol-related literature

Cryptographic protocols commonly use (random) nonces to guarantee security properties. The word *nonce* dates back to Middle English for something only used once or temporarily [47]. The word has been used in the cryptography domain since the 1970s [48]. Although cryptographers usually believe that *nonce* is a blend word built upon *number used once* [7], which is not the correct etymology, the basic understanding of the word remains correct.

In the narrow sense, a nonce used in a cryptographic protocol can be, for example, a counter value or a time-varying value because they both guarantee the *freshness* property, i.e., they are used once and only once. This approach is used by the NIST in [8] to define a nonce as “a time-varying value that has, at most, a negligible chance of repeating”. In the same vein, the BSI defines in [20] a nonce as being “an arbitrary number to be used only once in a cryptographic communication”.

In the scientific body of literature related to protocols, nonce-based protocols are usually introduced without clearly stating which properties the considered nonces should ensure. As noticed in [46], protocol specifications usually state that nonces are random values. A random value can obviously play the role of a nonce according to its narrow definition, but a random value guarantees an additional property, which is the *unpredictability* property of the nonce, so-called random nonce [1]. Even the NIST states that a nonce is a “randomly generated value” in some standards [60], which is much more constraining than the definition it provides in [8]. This common confusion was already pointed out by Abadi and Needham in 1994 [1], without any strong impact on the protocols that followed.

The lack of universal definition is misleading for cryptographers and developers, and leads to error-prone cryptographic implementations. For example, a cryptographer may prove a protocol assuming that the nonces are random values, while the developer may implement them with time-varying values. While the symmetric-key cryptography community has refined the distinction between nonces and random numbers [53], this distinction is less established in the protocol community, despite several foundational works [1], [21], [48].

This work concerns the freshness and unpredictability properties of random nonces. For the sake of brevity, such random nonces will sometimes simply be called nonces in the sequel. Apart from nonces, protocols frequently need additional random values, such as secret keys, random masks, or initialization vectors, which are consequently addressed as well in this work.

## B. Nonce implementation

With the lack of universal definition and clear recommendations, nonces may end up in practice being weakly generated, especially random nonces. For example, a frequent implementation mistake is using a common Pseudo-Random Number Generator (PRNG), rather than a Cryptographically-Secure Pseudo-Random Number Generator (CSPRNG). There are multiple possible PRNG implementations that do not guarantee the *freshness* or the *unpredictability* of the generated nonces. For example, PRNGs based on Linear Congruential Generators (LCG). Another example is a PRNG based on a hash chain $n_i = h(n_{i-1})$ with $n_i$ the nonce output at round i.

This work received funding from the France 2030 program managed by the French National Research Agency under grant agreement No. ANR-22-PECY-0006.
This type of implementation also trivially allows predicting all future nonces from a single one.

With regard to *freshness*, some PRNGs have short periods and may repeat themselves in practice. For example, Linear-Feedback Shift Registers (LFSR) are sometimes used as PRNG and their period depends on the length of the LFSR internal state.

Also, reusing a seed when initializing a PRNG may repeat the sequence of nonces if the system does not collect entropy from external sources. This problem is particularly important at boot time or in virtualized systems because the system may not have enough entropy when generating random values and ends up reusing some [14]. Sometimes the seed is simply a hardcoded constant to avoid implementing a hardware random number generator, for example on low-cost smartcards [50].

In [19], it was shown that some implementations use LCG for their nonce generation, making them completely predictable. An implementation was even found to rely on constant nonces, hence obviously known to anyone. Finally, when nonces are too short, collisions can quickly arise due to the birthday paradox.

Therefore, *freshness* and *unpredictability* are not always guaranteed in practice, which may affect protocol implementations. Analyzing the consequences of a nonce reuse (i.e., when the freshness property is not ensured) is of paramount importance, and it is as important to analyze a nonce leakage (i.e., when the unpredictability is not ensured).

### C. Related works

In his 2004 seminal paper about nonce-based cryptography [53], Rogaway formalized the use of nonces in symmetric encryption primitives. After it was identified that reusing a nonce with a key in GCM leaks the authentication key [39], the concept of nonce-misuse resistance has been defined in [54]. Informally, this property states AEAD construction should not fail completely when a nonce is reused. Several constructions for nonce-misuse resistant symmetric primitives have been defined and studied over the years [25], [34], [38]. The NIST CAESAR competition for Authenticated Encryption even included a *defense in depth* category, for AEAD modes that are nonce-misuse resistant. The winners Deoxys-II [38] and COLM [3] both provide this property.

In signature primitives, misused nonces also prove to be a source of problems with algorithms that leak their private key if a nonce is misused [12], [16], [49]. To counter that, alternative schemes relying on deterministic nonces are studied [13], [49], [51]. Basically, the idea of these schemes is to compute the nonce to use from a secret element (e.g., the private key) and the message to process, such that there cannot be two executions of the algorithm with the same key and nonce, but a different message.

It should be noted that designing CSPRNGs is an active research topic. Recently, a construction has been proposed to wrap an untrusted randomness source into a CSPRNG to output only quality random numbers [2]. This proposal

has been standardized by IETF under RFC 8937 [27]. Other CSPRNG constructions also exist in the literature [40].

When it comes to the security of nonce-based cryptographic protocols, since the 90s, several researchers have made the observation that nonce properties in protocols should be explicit [1], [41], [56]. However, event recent studies show that there exist weaknesses in random number generators widely deployed in practice, leading to practical attacks on protocols [14], [19], [30], [59].

From a formal point of view, there are a number of automated tools dedicated to cryptographic protocol proof in the symbolic model, like TAMARIN [45], PROVERIF [17] or AVISPA [4]. While symbolic models assume perfect cryptographic implementation by default, there are a growing number of studies to represent some cryptographic imperfections in these tools [22], [24], [26], [28], [29].

In 2020, the WPA2 key agreement has been formalized to study a key reinstallation attack that forces the generation of the same sequence of nonces with AES-CCM [29], [61]. Then, in 2023, this concept was taken one step further to propose symbolic models of AEAD algorithms [26] that formalize the known problems of these primitives, including their vulnerability to nonce reuse.

Closer to the problem studied in this paper, in [64], a detailed formal security analysis with TAMARIN of LoRaWAN 1.1 has been conducted, and the authors have also proposed a way to represent nonces used in the protocol by drawing them from a small predetermined pool of constants. Their aim was to recover a known attack on LoRaWAN 1.0 in their model. Our approach is in the same vein, but the way we model nonce misuses is different and better suited to the systematic analysis we want to carry out. The simplicity of our modeling also allows us to analyze more complex scenarios.

### D. Contributions

This paper introduces a method to identify with a systematic approach the properties an implementation should guarantee, w.r.t. random nonces, to ensure the security of a cryptographic protocol. As a corollary, the method determines the security impact of a nonce misuse. The proposed modeling is also applied to other types of random values, like ephemeral keys, masks, and nonces used in randomized primitives. In the latter case, we consider, when appropriate, the method used in [26], [29] for AEAD primitives, which illustrates that both methods are complementary. Overall, the proposed method could be used prior to standardizing protocols, in order to select protocols that are resilient against such misuses.

The contribution of this paper is twofold, as it provides:

* a method based on the formal symbolic verification tool TAMARIN to account for failure of implementations to generate correct nonces, and

* an analysis of existing standardized and deployed protocols, based on this method, which leads to newly discovered vulnerabilities in Dragonfly, WPA3, and Bluetooth.
The complete support material (implementations, models, and analyses) is available at [5], and also here:

https://github.com/ANSSI-FR/tamarin-parser.

## II. MOTIVATIONS THROUGH EXAMPLES

Many protocol implementations have proven to mishandle random values, opening the door to practical attacks. To motivate the importance of introducing a formal approach to detect such kinds of nonce misuses, this section presents two real-life cases: LoRaWAN 1.0 [57] and Bluetooth Numeric Comparison [18]. A nonce *reuse* is considered in the former case, while the vulnerability relies on the nonce *predictability* in the latter one.

### A. LoRaWAN 1.0

LoRaWAN is a technology dedicated to low-energy smart devices. A device joins a network using a cryptographic exchange, then sends and receives encrypted data from the network. The Over-the-Air Activation (OTAA) procedure of LoRaWAN 1.0, depicted in Figure 1, relies on a shared symmetric key *AppKey* known by the network and the device. The identity of the device is the public value DevEUI and the responder on the network side is identified by JoinEUI. The network knows the mapping between DevEUI, JoinEUI and *AppKey*, so it can verify the validity of the received message and craft an answer. In the response, the network sends devaddr, an address that the device uses to identify itself during the session.

<figure><img src="image_2.png" /><figcaption>Fig. 1. LoRaWAN 1.0 Over-the-Air Activation</figcaption></figure>

This protocol is vulnerable to multiple attacks [6], [64], the first one being on the authentication granted. Indeed, as there is no common data between the first and second message, any request can be paired with any response, so a Machine-in-the-Middle (MitM) attacker can break some forms of authentication. More interestingly, with respect to nonces, LoRaWAN 1.0 specification mentions that *DevNonce* and *JoinNonce* are respectively 16-bit and 24-bit values randomly chosen. Using short nonces aims to keep the messages as short as possible to

save battery life. However, a device that initiates $2^8$ sessions reuses a *DevNonce* value twice with a probability close to 0.5. When that happens, the attacker can replay the corresponding network response, which will be accepted by the device, and more importantly will force the device to reuse the same set of session keys. Therefore, in LoraWAN 1.0, the nonce reuse leads to a form of key reinstallation attack. Doing so, the attacker is then able to replay previous messages towards the device and, even worse, gain information on the plaintext transmitted because AES is used in counter mode.

To prevent this nonce reuse attack, LoRaWAN 1.1 [58] uses counters instead of nonces during the over-the-air activation, according to the recommendations provided in [6]. Note that using counters instead of nonces to mitigate security issues is not new. This kind of patch, which comes with its own drawbacks, was already used in the 2000s to mitigate the initialization vector reuse issue in the WEP protocol [32].

### B. Bluetooth Numeric Comparison

Bluetooth Numeric Comparison is a pairing protocol standardized for both Bluetooth Classic (BC) and Bluetooth Low Energy (BLE) technologies. It is one of the authentication and key agreement protocols defined in Bluetooth's specification. In this protocol, Initiator and Responder establish a shared session key *LTK* that is authenticated through user verification.

<figure><img src="image_3.png" /><figcaption>Fig. 2. Bluetooth Numeric Comparison (BLE version)</figcaption></figure>

The Bluetooth Numeric Comparison protocol is displayed in Figure 2, using the Bluetooth Low Energy (BLE) terminology. The same protocol is also used in Bluetooth Classic (BC). For the sake of simplicity, we assume here that *I* (i.e., the Initiator) and *R* (i.e., the Responder) have already exchanged their respective identities $ID_i$, $ID_r$ and input-output capabilities.
The protocol starts with a Diffie-Hellman exchange using the P-256 curve. *R* selects a nonce *N*<sub>*r*</sub> and commits to it with the value *C*<sub>*r*</sub>. Then, both *I* and *R* send their nonce *N*<sub>*i*</sub> and *N*<sub>*r*</sub>, and *I* verifies that the value *N*<sub>*r*</sub> received matches the commitment *C*<sub>*r*</sub>.

If correct, both devices display a 6-digit verification number, computed using the public values exchanged in the protocol. The user must verify that both codes are equal, then accept to continue the protocol with both devices. Key derivation is used to create a confirmation key *MacKey* and the session key *LTK*. Finally, a key confirmation is performed, using previously exchanged data and *MacKey*.

This protocol has been widely studied over time [15], [24], [28], [42], [59], [63], [65] and proven secure if implemented correctly. It is mentioned in the specification that if a user fails to verify that both codes match, an attack is possible. It was also shown that implementations that fail to validate the received public key are vulnerable to impersonation [15], [28]. More recently, pairing confusion attacks that trick devices to use two distinct protocols were identified [24], [63], [65]. In this work, we reuse the model provided in [28].

More relevant for our work, researchers have reverse engineered in [59] the PRNG implementation of widely deployed Broadcom chipsets and they identified that some of them generate nonces using a predictable PRNG. They also identified an attack on the Bluetooth Numeric Comparison protocol that requires the nonce $N_r$ to be predicted by the attacker. By predicting $N_r$, an attacker can send its own public key to each participant, then find a value $N'_i$ to send to $R$, such that both devices display the same code. If successful, the user cannot notice that there is an ongoing attack on the protocol, and the attacker successfully completes a MitM on the communication. Beyond the predictable nonce, the attack is possible because the code is a 6-digit hash of the parameters, so the attacker only has to brute force about a million values to find a correct nonce, which can be done in real time.

### III. TAMARIN PROVER

This section provides a brief description of the TAMARIN prover, which is the verification tool used in this paper.

#### A. Overview

TAMARIN [45] is a tool for verifying security protocols that supports both falsification and unbounded verification within the symbolic model. In this framework, messages are represented as terms, and it is assumed that cryptography is perfect. For instance, unless some explicit rules representing a cryptographic weakness are added into the model, nonces are supposed to be unguessable, and retrieving the content of a ciphertext is only possible when the key is known.

TAMARIN is a mature, state-of-the-art tool for cryptographic protocol verification that has already been successfully used to analyze large-scale, real-world cryptographic protocols [9]. Compared to similar tools like PROVERIF [17], AVISPA [4], or the recent verification platform SAPIC⁺ [23], TAMARIN comes with a better user interface and representation for some

primitives (e.g., Diffie-Hellman). For these reasons, we have chosen to implement our approach within TAMARIN, although nothing prevents our approach from being implemented in, e.g., PROVERIF or SAPIC⁺. This would, however, require adaptations as the input language of those tools are different from the one used in TAMARIN.

#### B. Modeling protocols

TAMARIN relies on multiset rewriting, a formalism frequently employed to model concurrent systems due to its inherent support for independent transitions. The system's state – comprising the contents of each agent's memory, the network, and the attacker's knowledge – is globally represented as a multiset of facts.

For instance, in our models, the facts `!Ltk($idA, ~k)` and `!Ltk($idB, ~k)` represent a key $\tilde{k}$ shared between the two agents whose identities are `$idA` and `$idB`. A fact of the form `StartI(idA, idB, m)` is typically used to indicate that the agent with identity `idA`, playing the role of the initiator, has started a session with the agent with identity `idB`. The parameter `m` can be used to store additional information.

Some facts are built-in in TAMARIN. This is the case of the fact `Fr` that produces fresh values, `!K(m)` used to represent that the attacker knows `m`, and the two built-in facts `In(m)` and `Out(m)` for modeling inputs and outputs of a message `m`.

A rewrite rule in TAMARIN has a name, e.g., `Reveal`, and three components, each of which is a multiset of facts: the rule's left-hand side, the rule's right-hand side, and its labels. The rule below allows one to reveal the key $\tilde{k}$ of an agent and a label `RevLtk(id)` is added in the execution trace to indicate that the agent `id` is corrupted.

$$ \texttt{rule Reveal: [!Ltk(id, \tilde{k})] -[RevLtk(id)] \rightarrow [Out(\tilde{k})]} $$

Executing a rule consumes the facts on the left. This means that the facts are removed from the global multiset of facts representing the current state of the system. Then, the rule produces the facts on the right, and adds the labels to the execution trace. Facts prefixed with `!` are persistent, i.e., they are not consumed, and can thus never be deleted or changed.

TAMARIN analyzes protocols in the so-called Dolev-Yao model, where the attacker is able to receive, intercept, modify, and forge messages. In order to represent cryptographic operations, TAMARIN relies on function symbols, and relations between them are defined through equations. Some cryptographic operations such as symmetric encryption and Diffie-Hellman, are built-in. This attacker is encoded using rewrite rules following the same format as the ones modeling protocols. For example:

$$ \texttt{rule Listen: [Out(x)] -[K(x)] \rightarrow [!K(x)]} $$

$$ \texttt{rule Enc: [!K(x);!K(y)] -[K(senc(x,y))]} \rightarrow [!K(senc(x,y))] $$

TAMARIN integrates a preprocessor that we used to include or exclude some parts of our file modeling protocols. Concretely, this is done by putting the relevant part of our code within a block of the form:
```c
#ifdef XXX code1 #else code2 #endif.
```

When running TAMARIN with the option `-DXXX`, `code1` will be considered, and otherwise `code2`. We rely on this feature to enable different behaviors in the modeling, e.g., in `code1` we include the rewrite rule modeling the normal behavior, and in `code2` we represent a patch version of the same rule. This feature is useful to avoid duplicating our models and keep them more readable.

### C. Modeling security properties

Security properties in TAMARIN are expressed using lemmas. These are first-order formulas written using the facts that label the rewrite rules, and indices `#i` used to identify execution steps. The language is rich enough to express various forms of authentication, e.g., injective or non-injective agreement, secrecy properties; or freshness properties ensuring that the value derived at some point has never been used before.

For instance, the lemma below states that for all traces where the fact `EndI` has been generated at step `#i`, then exists a time point `#j` that has occured before in the trace where the fact `EndR` has been generated, unless one of the agents is corrupted and has revealed their key at some time point `#r`.

lemma agreement:
"∀ ida idb m #i. EndI(ida, idb, m)@#i ⇒
(∃ #j . EndR(ida, idb, m)@#j & j < i)
| (∃ #r . RevLtk(ida)@#r)
| (∃ #r . RevLtk(idb)@#r)"

Restrictions are another useful feature of TAMARIN. They are formulas similar to lemmas, except that instead of proof obligations, they are assumptions, i.e., they tell TAMARIN to restrict its analysis to traces where they hold. For instance, to model that some equality holds at some point, we can label a rule with the fact `Eq(m,m')` and add a restriction expressing that we will only consider executions in which both messages are actually equal.

restriction Rstr: "∀ a b #i. Eq(a, b)@#i ⇒ a = b"

### D. Outcomes

When provided with a lemma, TAMARIN attempts to prove it, or to find a trace that contradicts it. This trace contains the sequence of rules that are applied and the actions the attacker took to violate the property. As the proof search is undecidable, TAMARIN may also not terminate. In that case, it is possible to use an interactive mode and to prove the property manually by guiding TAMARIN regarding the states to explore. Most of our proofs/attacks are obtained automatically by launching TAMARIN with its autoprove mode without further guidance. A few results required guidance through additional tactics [52] and intermediary lemmas to help TAMARIN to conclude.

## IV. MODELING RANDOMNESS FAILURE

This section explains how randomness can be represented in symbolic tools, with a focus on TAMARIN. The method developed for representing misused random numbers is applicable to any type of random value. This step can be automated, regardless of the role of the generated value. In Section VII-B, it is shown how this method can be used to analyze the consequences of misusing a random value in established randomized cryptographic primitives.

The basic approach consists in identifying all the random values of a given protocol, then generating a suitable symbolic model for every meaningful scenario, whether it belongs to the predictability case, to the reuse case, or even to the genuine case without any nonce misuse.

For illustrative purposes, we rely on a toy protocol depicted in Figure 3. This is a 2-party protocol in which 3 nonces are generated and exchanged.

<figure><img src="image_4.png" /><figcaption>Fig. 3. A toy 3-random protocol to illustrate randomness failure</figcaption></figure>

In practice, a lot of scenarios are necessary to study even this simple protocol. In order to simplify the study, the user only has to provide a protocol template for the TAMARIN model where random values are clearly identified. Instead of relying on `Fr` to generate random values, the user simply denotes them with a special fact that we have chosen to call `Random`.

Considering our toy protocol, and assuming that all three nonces may be misused, the TAMARIN template provided by the user will be as follows:

rule A1: [Random(n1)] → [Out(n1), A1Done()]

rule B1: [In(n1), Random(n2)] → [Out(n2)]

rule A2: [A1Done(), In(n2), Random(n3)] → [Out(n3)]

Note that such a TAMARIN template is not executable, and so TAMARIN must not be run on this file, as no rewrite rule producing facts `Random` is available. Moreover, this protocol is oversimplified to focus on the important aspect: the use of the `Random` fact.

### A. Genuine case

The genuine case is the one where nonces are supposed to be correctly generated. It is obtained from the template provided by the user by numbering the different `Random` facts in the protocol specification, and adding rewrite rules to generate the values. All the nonces are generated correctly relying on the built-in TAMARIN fact `Fr`. The additional rewrite rule regarding the first nonce is as follows, and we have similar
rules for the two other nonces. Rule A1 is also rewritten to use the correct value through the Random1 fact.

rule GenRandom1: [ Fr(~n1)] -> [ Random1(~n1) ]

rule A1: [ Random1(n1)] -> [ Out(n1), A1Done() ]

## B. Predictability

Predicting a random value means that the attacker guesses the value that will be used in a forthcoming session of the protocol. Typically, the attacker predicts a value from previous ones, for example, because it has recovered the internal state of a random number generator; or the attacker predicts it because its entropy is too low, possibly a hardcoded constant.

Predictability is represented in TAMARIN as a value leakage that occurs when the value is generated. Note that considering a leakage once the protocol session is over is out of the scope of this paper, although such an attack is relevant in cases where the secrecy of the values is required. Leaking the value at the beginning of the protocol is a stronger attacker model than leaking at the end, and actually catches all possible attacks relying on predictability.

Although any value might be considered to be predictable, a reasonable approach consists of assuming that if it is predictable in a given session, then it is predictable in any session. Moreover, to make the analysis closer to more realistic cases, we only consider the predictability of one value at a time. Of course, modulo a combinatorial explosion, other scenarios involving several random values are conceivable. With this assumption, for a protocol with N random values, there are N scenarios to be considered. Those scenarios are generated automatically from the TAMARIN template provided by the user.

We illustrate this scenario considering predictability of nonce $N_1$. The rule GenRandom1 from the genuine rewrite case is modified to model the leakage of $~n1$ as follows:

rule GenRandom1:[Fr(~n1)] -> [Out(~n1), Random1(~n1)]

Note that the value $~n1$ is given to the attacker (using the fact Out) each time such a value in generated, i.e., in all sessions. Regarding the two other random values, the rewrite rules will be the same as those used in the genuine case.

## C. Reuse

In our toy protocol given in Figure 3, there are four possible reuse scenarios if a single protocol session is considered: $N_1=N_2$, $N_1=N_3$, $N_2=N_3$, and $N_1=N_2=N_3$. Clearly, the combinatorics explodes when considering several protocol sessions. Not all these scenarios are meaningful in practice, though. The number of considered scenarios can consequently be restricted to a few cases:

(A) A given nonce is constant in all protocol sessions. This typically represents a poorly initialized random generator or a hardcoded nonce. For a N-random protocol, this case leads to N scenarios.

(B) Two (and only two) different nonces are equal whether they belong to the same protocol session or not. For a N-random protocol, this case leads to:

$$N + \frac{N(N-1)}{2} = \frac{N(N+1)}{2} \text{ scenarios.}$$

Considering the two cases (A) and (B) mentioned above, the total number of reuse scenarios to be considered is:

$$1 + \frac{N(N+1)}{2} = \frac{N(N+3)}{2}.$$

For example, the analysis of LoRaWAN 1.0 OTAA ($N=2$) leads to 5 reuse scenarios, while it leads to 27 reuse scenarios for WPA3 ($N=6$).

**Scenario A (reuse always):** In the case where a value is reused over all sessions, it is possible to model this by generating once and for all the misbehaving value using a persistent fact, and selecting the value from this fact in all protocol runs. The encoding in TAMARIN of such a scenario is illustrated below.

In order to illustrate this scenario, we consider the reuse of nonce $N_1$. Note that the original rule A1 is also modified to make use of the persistent fact created.

rule MisgenerateRandom1: [Fr(~n1)] -[OnlyOnce()]-> [!Random1(~n1)]

restriction RestOnlyOnce: "∀ #i #j. OnlyOnce()@#i & OnlyOnce()@#j ⇒ #i = #j"

rule A1: [!Random1(n1)] -> [Out(n1), A1Done() ]

The rewrite rules B1 and A2 remain unchanged up to the numbering of the fact Random. The rewrite rule modeling the random generation for values $N_2$ and $N_3$ are as in the genuine case. The restriction RestOnlyOnce ensures that the label fact OnlyOnce occurs at most once in a trace, and thus only one nonce $~n1$ will ever be generated.

**Scenario B (reuse once):** In this scenario, a given random value is used twice. For example, the nonce $N_1$ is used twice necessarily means that $N_1$ appears with the same value in two different sessions. However, when we consider a reuse between two different nonces, e.g., $N_1$ and $N_3$, then the reuse can happen in the same session, or in two different sessions. In TAMARIN, we decided to write one model for each pair of values, but the fact that the reuse happens in the same session, or in two different sessions (when this makes sense) is captured within the same TAMARIN model.

Below, we illustrate the case where the nonce $~n$ is reused to play both the roles of $N_1$ and $N_3$. As for scenario A, a restriction is used to ensure that the misgeneration occurs at most once.

rule MisgenerateRandom1: [Fr(~n)] -[OnlyOnce()]-> [Random1(~n); Random3(~n)]

restriction RestOnlyOnce: "∀ #i #j. OnlyOnce()@#i & OnlyOnce()@#j ⇒ #i = #j"

In this model, the rewrite rules modeling the genuine generation of nonces for $N_1$, $N_2$, and $N_3$ are still present
as they are useful for modeling the generation of nonces for the other sessions.

## D. Implementation

Considering the reuse scenarios, the predictability scenarios, and the genuine scenario, and assuming that reuse and predictability are exclusive, the total number of scenarios to be considered for a N-random protocol is:

$$1 + N + \frac{N(N+3)}{2} = 1 + \frac{N(N+5)}{2}.$$

Each scenario leads to a TAMARIN model that is automatically generated from the TAMARIN template provided by the user. This template represents the protocol, and the random values on which the misuse analysis has to be performed are indicated through the use of the special fact Random.

Regarding implementation details, this approach relies on TamarinParser, a Python tool developed and published along with this study. It is based upon the Python Lex-Yacc (PLY) package [11], which allows for defining and parsing custom grammars. It parses the Abstract Syntax Tree (AST) of a TAMARIN model, following the grammar implemented by TAMARIN. Once the AST is recovered, there are predefined transformations of the AST to implement the patterns detailed in this section. Therefore, this tool transforms TAMARIN template containing Random facts into valid TAMARIN models with additional rules and restrictions. This is used to generate all misuse cases, that are then written to new .spthy files to be processed by TAMARIN.

# V. CASE STUDIES

To analyze the impact of nonce misuse on protocols, our method is applied to various case studies. This section begins by describing the protocols and the considered security properties. We then clarify which random values are the focus of our analysis in each case study (see Table I).

## A. Analyzed protocols

The approach provided in this paper is first applied to several authentication protocols:

* Needham-Schroeder-Lowe Public Key (NSLPK); and

* four protocols from the ISO 9798 standard.

It is then applied to more complex authentication and key agreement protocols from industrial standards:

* LoRaWAN 1.0 OTAA;

* Bluetooth Numeric Comparison (NC);

* Four-Way Handshake;

* RFC 7664 - Dragonfly Key Exchange; and

* Wi-Fi Protected Access 3 (WPA3).

LoRaWAN and Bluetooth NC have already been presented in Section II. The other protocols are briefly described below with message sequence charts available in the appendix.

1) NSLPK and ISO 9798: The Needham-Schroeder-Lowe Public Key protocol is a well-known mutual authentication protocol studied in the scientific literature [43]. It has been developed to fix an attack identified by Lowe in the original Needham-Schroeder protocol. It is a two-party protocol, and each agent has a private-public key pair. This protocol explicitly involves two random nonces, one being generated by each party. For our analysis, we reuse the already existing model provided in the TAMARIN repository.

ISO standards define security protocols for different purposes and initial setups. The ISO 9798 specification defines many authentication protocols. They differ by the cryptographic primitives they use, and the presence or not of a trusted third party. In this work, we consider:

* ISO 9798-2-4 [36]: authenticated encryption, 3-pass mutual authentication;

* ISO 9798-2-6 [36]: authenticated encryption, 5-pass mutual authentication with trusted third party;

* ISO 9798-3-4 [37]: digital signature, 3-pass mutual authentication; and

* ISO 9798-4-4 [35]: message authentication code, 3-pass mutual authentication.

In ISO protocols, the specification mentions the use of random nonces (2 or 3 in each protocol), which are therefore considered in this work. It should be noted that parts of the ISO 9798 standard have already been subject to formal analyses [10], [66]. However, the protocols have since been improved and the standards have been updated accordingly. It is also worth noting that these seminal analyses did not include nonce misuse.

2) Four-Way Handshake: The Wi-Fi ecosystem defines several methods to authenticate a client to an Access Point (AP). The Four-Way Handshake is core to the authentication in Wi-Fi networks as it is used in both WPA2 and WPA3 authentication. The Four-Way Handshake relies on a Pre-Shared Key (PSK), shared between the AP and the client. The protocol eventually allows AP and clients to share a Pairwise Transient Key (PTK) that is used to exchange encrypted packets. This protocol benefits from extensive formal analyses (with a broader approach than ours, e.g., [29]), and its security properties are thus well understood.

3) Dragonfly: The Dragonfly key exchange, depicted in Figure 4, is defined in IETF RFC 7664 [33]. Dragonfly is a 2-agent authentication and key agreement protocol. Both parties initially share a password and agree on parameters, namely the group to be used. They first derive a group element $pe$ from the password and their respective identities. The agent A generates a random key $s_A$ and a random mask $m_A$, then sends the scalar $s_A + m_A$ and the group element $pe^{-m_A}$. The agent B sends a similar message, using two other random values and $pe$. The agent A computes a shared secret from B's scalar and group element as follows:

$$ss = (pe^{s_B+m_B} \times pe^{-m_B})^{s_A} = pe^{s_B \times s_A}.$$
Then, agent B does an analogous calculation. They both exchange confirmation values to verify they have the same shared secret. At the end of the exchange, they share a key mk that they use in further protocols.

Although the shared secret derived from the first message is a usual Diffie-Hellman secret, representing the use of masking and its derivation is challenging in a symbolic model. The naive approach would be to define an addition function that is distributive with regard to the multiplication:

$$g^{m+s} = g^m \times g^s.$$

Doing so, TAMARIN can accurately simplify $g^m \times g^{-m} = DH_{neutral}$, with $DH_{neutral}$ being the neutral element of the group. However, TAMARIN forbids a user to write such equations, as it would break its correctness [31], [55]. The representation chosen here is to model the addition with a function add, and to provide rules that deliver the Diffie-Hellman secret to the legitimate agent when it is needed. The function inv is the builtin inverse function in TAMARIN that is used to implement group operations.

rule ADeriveSS:
[ AKey($B, $A, psk, pe, ^ska, inv(pe^~mb), add(^mb, ^skb)) ]
→ [ AGetKey($B, $A, psk, ^ska, (pe^~skb)^~ska) ]

The attacker also has a specific derivation rule to derive the public key of a participant under the knowledge of $pe, pe^{-m}$ and $m+s$.

rule AttDerive:
let pe = h($AP, $Client, psk) in
[ !PskUsed(psk),
  In(pe), In inv(pe^~m), In add(^m, ^s))
→ [ Out(pe^~s) ]

TAMARIN faces challenges in handling the exchange of Dragonfly keys. The proposed model remains an oversimplification, considering that all values received are well-formed terms from fresh values. Nevertheless, this simplified model still produces meaningful results.

4) WPA3: WPA3 is another method for joining a Wi-Fi network. It relies on the combination of the Dragonfly key exchange to derive a key mk, and then uses this key as an input for the Four-Way Handshake. WPA3 restricts the role that the client and the AP have in the Dragonfly key exchange and specifies the cryptographic groups that can be used.

## B. Security properties

In order to perform a systematic study, there are two sets of security properties considered, depending on whether the protocol is an authentication protocol or an authentication and key agreement protocol. For NSLPK and protocols from ISO 9798, the non-injective agreement (NIA) and injective agreement (IA) properties from the perspective of each party are studied, following the definition from Lowe's hierarchy of authentication properties [44]. For all the other protocols, we consider additional properties, namely NIAK, IAK, S, and KF. All these security properties are briefly explained below:

* Non-injective agreement on role and nonces (NIA): Whenever an agent a playing role A has completed the protocol with another agent b and exchanged some nonces, b has indeed played role B with a, and the two agents agree on the nonces that have been exchanged during the session, unless a and/or b is compromised. A similar property can be expressed from the perspective of role B.

* Injective agreement on role and nonces (IA): This property is NIA where, additionally, each run of agent a in role A corresponds to a unique run of agent b in role B.

* Non-injective and injective agreements on keys (NIAK & IAK) are defined in a similar way, considering the keys instead of nonces.

* Weak secrecy of keys (S): Whenever a secret key is established by an agent playing role A (resp. B), then the attacker does not know the key, unless one of the agents who established that key has been compromised.

* Freshness of keys (KF): Whenever an agent a playing role A has completed the protocol and computed a key, then this key is fresh in the sense that the same key has not been derived in another session of role A. Again, a similar property can be expressed from the point of view of role B.

All properties are analyzed under the assumption of an unlimited number of sessions and the possibility of an agent to be compromised. To illustrate how these properties are modeled in TAMARIN, we consider below the freshness of the ptk from the perspective of the AP in WPA3. This is expressed in TAMARIN as follows:

lemma keyFreshnessAP:
"∀ ap client ptk #i .
  APEndedKeys(ap, client, ptk)@#i
  ↪ (∃ ap2 client2 #j .
      APEndedKeys(ap2, client2, ptk)@#j
      & ↪ (#i = #j))
  | (∃ #r . RevLtk()@#r)"

Informally, this property states that an attacker must not be able to force the AP to reuse a previous ptk. If it happens, then this is typically a case of key-reinstallation attack, similar to the problem that affects LoRaWAN 1.0 OTAA [64] and some WPA2 implementations [29], [61].

## C. Random values under analysis

In this work, we consider the misuse of any random value represented in our TAMARIN models. Nonces are commonly used in protocols and are usually left poorly specified. Hence, they are considered to be possibly misused. This helps to gain a deeper understanding of nonce properties critical to protocol security.

In addition, several protocols rely on the generation of ephemeral keys during the execution. These keys are also considered to be possibly misused in our models. The misuse of ephemeral keys is briefly discussed at the beginning of Section VII. Table I summarizes the different random values considered for each protocol studied. A distinction is made between protocol nonces and ephemeral keys, to better interpret the security consequences of the results. In particular,
<figure><img src="image_5.png" /><figcaption>Fig. 4. Dragonfly protocol</figcaption></figure>

<table><caption>TABLE I
RANDOM VALUES INVOLVED IN THE CONSIDERED PROTOCOLS</caption><thead><tr><td>Protocol</td><td>Protocol nonce</td><td>Ephemeral key</td></tr></thead><tbody><tr><td>NSLPK</td><td>N<sub>A</sub>, N<sub>B</sub></td><td>-</td></tr><tr><td>9798-2-4</td><td>R<sub>A</sub>, R<sub>B</sub></td><td>-</td></tr><tr><td>9798-2-6</td><td>R<sub>A</sub>, R<sub>B</sub>, R<sub>A2</sub></td><td>k<sub>AB</sub></td></tr><tr><td>9798-3-4</td><td>R<sub>A</sub>, R<sub>B</sub></td><td>-</td></tr><tr><td>9798-4-4</td><td>R<sub>A</sub>, R<sub>B</sub></td><td>-</td></tr><tr><td>LoRaWAN 1.0</td><td>DevNonce, JoinNonce</td><td>-</td></tr><tr><td>Bluetooth NC</td><td>N<sub>i</sub>, N<sub>r</sub></td><td>ski, skr</td></tr><tr><td>Four-Way Handshake</td><td>N<sub>A</sub>, N<sub>S</sub></td><td>-</td></tr><tr><td>Dragonfly</td><td>m<sub>A</sub>, m<sub>B</sub></td><td>s<sub>A</sub>, s<sub>B</sub></td></tr><tr><td>WPA3</td><td>N<sub>A</sub>, N<sub>S</sub>, m<sub>A</sub>, m<sub>B</sub></td><td>s<sub>A</sub>, s<sub>B</sub></td></tr></tbody></table>

the protocols that rely on ephemeral keys are ISO 9798-2-6, Bluetooth NC, Dragonfly, and WPA3.

Some of the protocols also rely on long-term keys. In the considered protocols, long-term keys are roots of trust, hence it is expected that the security properties studied would fail in case of misuse. However, we highlight that our approach could be extended to also tackle long-term key misuse. Such cases may be relevant for protocols that intend to provide forward secrecy or post-compromise security.

## VI. RESULTS

In this section, we first provide an overview of the results obtained from the case studies, and then we discuss in depth the cases Dragonfly, WPA3, and ISO 9798-2-6. As already said, we focus here on protocol nonce misuse. Additional results involving ephemeral keys and randomized primitives are detailed in Section VII. Most results were obtained using the automatic mode of TAMARIN, except for WPA3 and ISO 9798-2-6 that required manual guidance with tactics to conclude on some cases [52]. Running all the models required several days. A standard laptop was primarily used, and a server was employed for cases demanding additional RAM.

All details are available at: https://github.com/ANSSI-FR/tamarin-parser.

### A. Summary of the results regarding protocol nonces

Several protocols considered in this paper have multiple versions that deserve to be analyzed. For example, the basic implementation of Dragonfly is considered, but also one that is patched against a well-known reflection attack [33], [62]. In total, 166 models are studied, covering all possible cases of misuse and relevant configurations for the studied protocols.

Table II provides a summary of the results regarding protocol nonces. The approach has been performed systematically, but we acknowledge that the leak misuse case is not relevant in protocols that send the generated nonces in cleartext (e.g., Four-Way Handshake) right after being generated.

The first block *No misuse* represents the results of the analysis when nonces are considered to be perfectly generated.

LoRaWAN 1.0 OTAA and Dragonfly fail some properties even when no misuse is assumed, which is consistent with the existing literature [6], [64].

The original paper, which presented the attack on Bluetooth Numeric Comparison [59], correctly identified that the predictability of nonce $N_r$ breaks the protocol. The model studied here confirms this attack, but also shows that the protocol is broken when the nonce $N_i$ is predictable.

One can also see that attacks are found when a nonce is reused. In fact, the analysis of the attack trace shows that this happens when a device has completed a session with a nonce $N_i$ or $N_r$, then reuses it in a second session. Because the nonce was revealed in the first session, the attacker can predict the value that will be used in the second one. Therefore, these attacks also highlight the critical importance of unpredictability for the nonces, rather than their freshness. It is important to note that, since TAMARIN halts upon finding the first attack trace, additional issues related to nonce freshness may remain undetected.

We also observed that in many of the studied protocols, reusing a nonce leads to a loss of injectivity of the agreement
<table><caption>TABLE II
SUMMARY OF THE RESULTS</caption><thead><tr><th rowspan="2">Protocol</th><th colspan="6">No misuse</th><th colspan="6">Reuse once</th><th colspan="6">Reuse always</th><th colspan="6">Leak always</th></tr><tr><th>IA</th><th>NIA</th><th>IAK</th><th>NIAK</th><th>S</th><th>KF</th><th>IA</th><th>NIA</th><th>IAK</th><th>NIAK</th><th>S</th><th>KF</th><th>IA</th><th>NIA</th><th>IAK</th><th>NIAK</th><th>S</th><th>KF</th><th>IA</th><th>NIA</th><th>IAK</th><th>NIAK</th><th>S</th><th>KF</th></tr></thead><tbody><tr><td>NSLPK</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>-</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>-</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>-</td><td>-</td></tr><tr><td>ISO 9798-2-4</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>-</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>-</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>-</td><td>-</td></tr><tr><td>ISO 9798-2-6</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>-</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>-</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>-</td><td>-</td></tr><tr><td>ISO 9798-3-4</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>-</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>-</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>-</td><td>-</td></tr><tr><td>ISO 9798-4-4</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>-</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>-</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>-</td><td>-</td></tr><tr><td>LoRaWAN 1.0 OTAA</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td>Bluetooth NC</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td>Four-Way Handshake (Static PSK)</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td>Four-Way Handshake (Fresh PSK)</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td>Dragonfly (No patch for reflection)</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td>Dragonfly (Patch for reflection)</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td>WPA3</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr></tbody></table>

●: None of the cases ends with the property falsified

●: Property is false for both sides of the protocol, though there may be two involved cases with an attack for one side each

● or ●: The property is false in at least one case for stated side of the protocol. The other side has no property contradicted in any case

<table><caption>TABLE III
DETAILED RESULTS ON THE DRAGONFLY KEY EXCHANGE</caption><thead><tr><th></th><th>Misuse</th><th>IA</th><th>NIA</th><th>IAK</th><th>NIAK</th><th>S</th><th>KF</th></tr></thead><tbody><tr><td rowspan="3">Dragonfly (no patch)</td><td>N/A</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td>Leak m<sub>A</sub></td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td>Leak m<sub>B</sub></td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td rowspan="3">Dragonfly (patched)</td><td>N/A</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td>Reuse (any)</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td>Leak m<sub>A</sub></td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td></td><td>Leak m<sub>B</sub></td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr></tbody></table>

for one side of the communication. A perhaps more interesting element is the key freshness property (KF), which may fail when a nonce is reused. This impacts the Four-Way Handshake, and shows that key reinstallation could still happen against devices patched for KRACK [61] in case their nonces are reused.

## B. Dragonfly

The detailed results on the Dragonfly key exchange are shown in Table III. To the best of our knowledge, this is the first formal study of Dragonfly using a symbolic tool. In particular, we discover that many security properties fail, even when no nonce misuse is considered. There exists indeed a reflection attack on the protocol, where an attacker, acting as the responder, reflects the two messages received from the initiator. With this scenario, most security properties fail, although the attacker has no knowledge of the key derived by the initiator. It should be noted that the specification mentions

that implementations should protect themselves against such a reflection attack. However it does not detail the security problems created when this mitigation is not applied. This reflection attack on Dragonfly is also mentioned in [62] as it affects some WPA3 implementations. They also identify a side-channel attack on the “hunting-and-pecking” algorithm used to derive *pe*, but such attacks are out of scope of our symbolic analysis.

More importantly, our study highlights that if the attacker knows one of the masks $m_A$ or $m_B$, it is always possible to passively recover the shared secret after the key exchange is completed. Because the attacker has the shared secret $ss$, it is able to derive the keys $kck$ and $mk$, hence complete the protocol with each of the honest agents. The attack works as follows when $A$ leaks $m_A$:

1) $A$ and $B$ have exchanged their public parameters;

2) Attacker knows $s_A+m_A$, $pe^{-m_A}$, $m_A$, $s_B+m_B$, $pe^{-m_B}$;

3) Attacker recovers $pe = (pe^{-m_A})^{(-m_A)^{-1}}$;

4) Attacker computes $pe^{s_B} = pe^{s_B+m_B} \times pe^{-m_B}$;

5) Attacker recovers $s_A = s_A + m_A - m_A$;

6) Attacker computes $ss = (pe^{s_B})^{s_A}$.

TAMARIN possesses a refined representation of exponents: therefore it is aware that by knowing $g^a$ and $a$, it is possible to recover $g$ (Step 3). Then, it is possible to recover $s_A$ from the knowledge of $s_A + m_A$ and $m_A$, which allows them to finally derive the shared secret. Although the symbolic analysis is limited by the security properties formalized in the model, this result enables us to make several other observations with respect to the security of the Dragonfly key exchange:

* If the nonce used by a participant leaks at any point in the
protocol, and an attacker has observed the key exchange, the attacker gains knowledge of *pe*, which allows for an offline brute force of the PSK.

* If the nonce used by a participant leaks after the protocol has ended, and an attacker has observed the key exchange, the attacker is able to recover the session key *mk* and to decrypt subsequent communications. Hence, forward secrecy fails if the nonce leaks.

Therefore, w.r.t. Dragonfly security, our study demonstrates that more than being *unpredictable*, the nonce must absolutely remain *secret*, even after the protocol has ended. Overall, on Dragonfly, the secrecy of the nonce for the security of the protocol is just as important as the secrecy of the private key of an agent. For reference, the Dragonfly specification mentions that the mask should be “irretrievably destroyed” after being used, but remains ambiguous with regards to expected security properties of this value. The specification also fails to describe the consequences, should the mask not be destroyed. The present study clarifies the specification and makes explicit why this requirement must be fulfilled.

### C. WPA3

WPA3 is the combination of Dragonfly and the Four-Way Handshake. First, it should be noted that the security of WPA3 is not affected by the reflection scenario. Moreover, the possible key reinstallation due to nonce reuse in the Four-Way Handshake does not affect WPA3. This comes from the fact that a fresh key is generated at the end of each Dragonfly run before being used for the Four-Way Handshake. This is similar as if the Four-Way Handshake was used with a fresh PSK at each run.

However, there is still a remaining issue when the possibility of *predictable* nonces is taken into account, as this leads to critical problems on the overall protocol. If any nonce used in Dragonfly leaks, then the attacker can recover the *mk* at the end of the exchange, as explained in Section VI-B. When this happens, the Four-Way Handshake is run between two honest agents, while the attacker knows the symmetric shared secret that is used for the key derivation. Therefore, the attacker is able to break most security properties, including the secrecy of the *ptk* that is derived at the end of the exchange.

Similarly, the observations made for Dragonfly also hold for WPA3, so an attacker who learns a mask can break future communications and attempt an offline brute force of the network passphrase. This shows that the *secrecy* of the masks generated during the key exchange is of critical importance for the security of WPA3-encrypted communications. As for the Dragonfly RFC, the IEEE 802.11 specification is explicit that the mask shall be “irretrievably destroyed” along with the key, but does not explain the reason for doing so.

### D. ISO 9798-2-6

The detailed results for protocol nonce misuse in ISO 9798-2-6 are provided in Table IV. Although there is a problem identified when the nonce $R_B$ is reused at least once, all other studied cases regarding protocol nonces misuse have no

<table><caption>TABLE IV
DETAILED RESULTS FOR ISO 9798-2-6</caption><thead><tr><th></th><th>Misuse</th><th>IA</th><th>NIA</th></tr></thead><tbody><tr><td rowspan="3">9798-2-6</td><td>N/A</td><td>●</td><td>●</td></tr><tr><td>Reuse once R<sub>B</sub> = R<sub>B</sub></td><td>●</td><td>●</td></tr><tr><td>Reuse always R<sub>B</sub></td><td>●</td><td>●</td></tr><tr><td></td><td>Other misuses</td><td>●</td><td>●</td></tr></tbody></table>

<table><caption>TABLE V
IMPORTANT PROPERTIES PER NONCE PER PROTOCOL</caption><thead><tr><th>Protocol</th><th>Nonce</th><th>Required property</th><th>Impact if property invalid</th></tr></thead><tbody><tr><td rowspan="3">NSLPK</td><td rowspan="2">N<sub>i</sub></td><td>unpredictability</td><td>IA, NIA</td></tr><tr><td>freshness</td><td>IA, NIA</td></tr><tr><td>N<sub>r</sub></td><td>unpredictability</td><td>IA, NIA</td></tr><tr><td rowspan="2">ISO 9798-2-4</td><td>R<sub>A</sub></td><td>freshness</td><td>IA, NIA</td></tr><tr><td>R<sub>B</sub></td><td>freshness</td><td>IA</td></tr><tr><td rowspan="3">ISO 9798-2-6</td><td>R<sub>A</sub></td><td>none</td><td>N/A</td></tr><tr><td>R<sub>B</sub></td><td>freshness</td><td>IA</td></tr><tr><td>R<sub>A2</sub></td><td>none</td><td>N/A</td></tr><tr><td rowspan="2">ISO 9798-3-4</td><td>R<sub>A</sub></td><td>freshness</td><td>IA</td></tr><tr><td>R<sub>B</sub></td><td>freshness</td><td>IA</td></tr><tr><td rowspan="2">ISO 9798-4-4</td><td>R<sub>A</sub></td><td>freshness</td><td>IA</td></tr><tr><td>R<sub>B</sub></td><td>freshness</td><td>IA</td></tr><tr><td rowspan="2">LoRaWAN</td><td>DevNonce</td><td>freshness</td><td>KF</td></tr><tr><td>JoinNonce</td><td>freshness</td><td>KF</td></tr><tr><td rowspan="2">Bluetooth NC</td><td>N<sub>i</sub></td><td>unpredictability</td><td>IA, NIA, IAK, NIAK, S</td></tr><tr><td>N<sub>r</sub></td><td>unpredictability</td><td>IA, NIA, IAK, NIAK, S</td></tr><tr><td rowspan="2">Four-Way Handshake</td><td>N<sub>A</sub></td><td>freshness</td><td>IA, IAK, KF</td></tr><tr><td>N<sub>S</sub></td><td>freshness</td><td>IA, IAK, KF</td></tr><tr><td rowspan="2">Dragonfly</td><td>m<sub>A</sub></td><td>unpredictability (*)</td><td>IA, NIA, IAK, NIAK, S, KF</td></tr><tr><td>m<sub>B</sub></td><td>unpredictability (*)</td><td>IA, NIA, IAK, NIAK, S</td></tr><tr><td rowspan="3">WPA3</td><td>m<sub>A</sub></td><td>unpredictability (*)</td><td>IA, NIA, IAK, NIAK, S</td></tr><tr><td>m<sub>B</sub></td><td>unpredictability (*)</td><td>IA, NIA, IAK, NIAK, S</td></tr><tr><td>N<sub>A</sub></td><td>none</td><td>N/A</td></tr><tr><td></td><td>N<sub>S</sub></td><td>none</td><td>N/A</td></tr></tbody></table>

impact on the security of the protocol. This protocol relies on a trusted third party that shares a key with honest agents from the beginning. A description is available in the appendix.

For this protocol, *A* generates two distinct nonces, while *B* generates one. The interesting point of the study is that *A* may reuse any of its two nonces, this has no impact on the security properties guaranteed by this protocol. However, if *B* reuses its nonce, the injective agreement of *B* with respect to *A* is no longer satisfied because an attacker can replay the fourth message to *B*, which will correctly end the protocol.

This peculiarity comes from the fact that *A* uses two nonces, one with the third party and one with *B* and verifies that these two values are associated with the value of $R_B$ for the considered session. Furthermore, the trusted party generates a fresh $k_{AB}$ at each session, therefore this adds another element of randomness in the overall protocol.

<footnote>(*) Unpredictability is a necessary property, but it is not enough to guarantee security: as stated in Section VI-B, the nonce secrecy is required, not only its unpredictability.</footnote>
<table><caption>TABLE VI
SUMMARY OF THE RESULTS FOR EPHEMERAL KEY MISGENERATION</caption><thead><tr><th>Misuse</th><th>Protocol</th><th>IA</th><th>NIA</th><th>IAK</th><th>NIAK</th><th>S</th><th>KF</th></tr></thead><tbody><tr><td rowspan="4">Leak</td><td>ISO 9798-2-6</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>-</td></tr><tr><td>Dragonfly (patch)</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td>WPA3</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td>Bluetooth NC</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td rowspan="4">Reuse (any)</td><td>ISO 9798-2-6</td><td>●</td><td>●</td><td>-</td><td>-</td><td>-</td><td>-</td></tr><tr><td>Dragonfly (patch)</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td>WPA3</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td>Bluetooth NC</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr></tbody></table>

### E. Important properties per protocol nonce

The results of the analysis of the different models and attack traces can be found in Table V. It synthesizes the relevant property to be fulfilled, for each nonce of each protocol studied, as well as the security properties that fail when the property is not true. When a leaking nonce creates a problem, this means that *unpredictability* is relevant for the nonce. When a reused nonce creates a problem, it usually indicates the requirement of *freshness*. However, when security issues are identified in both cases, further inspection of the attack traces is required to identify the root cause. In particular, for Bluetooth and WPA3 this inspection showed that the relevant property is indeed the *unpredictability*, the reuse cases that failed were simply cases where the nonce considered was leaked in a previous session, and reuse in place of another nonce. As TAMARIN halts when one attack trace is found, *freshness* may possibly still be required in these protocols.

## VII. ADDITIONAL RESULTS

This section details results regarding the misuse of ephemeral keys and nonces in randomized primitives.

### A. Ephemeral keys misuse

The results obtained for the misuse of ephemeral keys are displayed in Table VI. As expected, if an ephemeral key leaks the protocol loses its security properties. The reuse scenarios are more interesting, and differences can be identified between protocols in that regard. For ISO 9798-2-6, in case the key $k_{AB}$ is reused between sessions, then all authentication properties fail. For Dragonfly, TAMARIN identifies a problem with the key freshness if an ephemeral key is reused. Finally, for Bluetooth NC, there are no problems identified in the studied model if an ephemeral key is reused. The Bluetooth specification itself specifies that the same ephemeral key may be reused for several sessions<fnref n="1" />, so the present result confirms the security of the protocol in this context.

### B. Advanced models for randomized primitives

Certain protocols considered in this paper may depend on randomized cryptographic primitives, which can lead to subtle

vulnerabilities in scenarios where random values are misused. For instance, common AEAD primitives should not be used with the same key and nonce to encrypt distinct messages.

In [26], the authors present several potential failures of practical AEAD encryption schemes, including vulnerabilities arising from nonce reuse. They propose different ways of modeling this in TAMARIN. They consider the case where the key leaks if the attacker has access to two such ciphertexts (NR-A1 model), and they also consider a weaker attacker model in which the attacker only accesses the contents of the messages (NR-A2 model).

In the same vein, signature imperfections regarding nonce misuses can be modeled in TAMARIN to take into account weaknesses of signature algorithms when random values are incorrectly generated. Some well-known flaws concern (EC)DSA signatures. It has been demonstrated that if the (EC)DSA random value leaks or if there is a known linear relation between two of them, it is possible to recover the signing key [12]. Note that reusing a random value gives a trivial linear relation between two randoms, hence this case also allows for recovering the signing key. This attacker model that can be easily represented in TAMARIN is called NR-S.

In order to present comprehensive results, our systematic analysis of nonce misuse has also been conducted under these advanced attacker models. To do that, we first explicitly model randomness in primitives, and we add the corresponding TAMARIN rules sketched above, depending on whether the protocol relies on the AEAD or the signature primitive.

<table><caption>TABLE VII
SUMMARY OF THE RESULTS OF MISUSED NONCES IN PRIMITIVES</caption><thead><tr><th rowspan="2"></th><th rowspan="2">Attacker model</th><th colspan="2">Reuse once</th><th colspan="2">Reuse always</th><th colspan="2">Leak</th></tr><tr><th>IA</th><th>NIA</th><th>IA</th><th>NIA</th><th>IA</th><th>NIA</th></tr></thead><tbody><tr><td rowspan="3">9798-2-4</td><td>Standard</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td>NR-A1</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td>NR-A2</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td rowspan="3">9798-2-6</td><td>Standard</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td>NR-A1</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td>NR-A2</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td rowspan="2">9798-3-4</td><td>Standard</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr><tr><td>NR-S</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td><td>●</td></tr></tbody></table>

To study all possible misuses (i.e., random nonces, ephemeral keys, random values in primitives) with the different attacker models for protocols ISO 9798-2-4, 9798-2-6, and 9798-3-4, there are a total of 254 models to study. This systematic study has been performed, and confirms the results for the misuse of random nonces and ephemeral keys. With regards to the misuse of random values in randomized primitives, additional results are identified when they are leaked or reused across agents and/or protocol executions. These are displayed in Table VII.

As expected, the threat model (NR-A1) and (NR-S) yield some attacks when the nonce used in the primitive is reused. However, there is a difference between 9798-2-4 and 9798-

<footnote n="1">¹Bluetooth Core Spec., Vol. 3, Part H, §2.3.6; and Vol. 2, Part H, §5.1</footnote>
2-6. In the former protocol, considering (NR-A2), there is no additional security problem identified with respect to a perfect primitive. However, in 9798-2-6, there are still vulnerabilities identified in this model. Upon inspection of the attacks, this is because the server in this protocol generates a key $k_{AB}$ and sends it encrypted to A and B. Therefore, if the content of the encrypted message leaks to the attacker, it is able to recover $k_{AB}$ and finish the protocol with A and B, breaking authentication properties.

## VIII. CONCLUSION

Although it is known for a long time that nonces should have clear security properties, many modern standards do not meet this requirement. Even the standardization body NIST is sometimes ambiguous about the definition of nonce: a nonce being either a value used once or a random value, depending on the considered standard.

This paper introduces a method, based on the prover TAMARIN, to identify in a systematic way the consequences of nonce misuses. In order to illustrate the relevance of the approach, the method has been successfully applied to well-understood protocols. New corner cases on recent and widely deployed protocols such as Dragonfly, WPA3, and Bluetooth have been identified.

This approach could be used to provide additional insight when selecting a standardized protocol for a specific application, without control over all the implementations. A sane approach is to choose a protocol that is more robust when misimplemented. This has been the approach followed by the NIST (albeit on a different subject) when standardizing encryption algorithms resistant to nonce misuses.

From a pure design perspective, we observe that there exist other protocols that do not rely solely on random nonces. LoRaWAN 1.1 for example is explicit about the use of counters and the verifications an implementation must perform. Authentication protocols in mobile networks (e.g., EPS-AKA, 5G-AKA, etc.) mix both a nonce and a time-based SQN value to prevent replay attacks. A final example is the recently standardized SPAKE2+ in RFC 9383. This is a password-authenticated key exchange whose objectives are similar to those of Dragonfly. It does rely on ephemeral keys, but not on random nonces or counters of any kind. These alternative protocol designs may prove fruitful and could gradually be extended to other protocols, ensuring that future standardized protocols are less vulnerable to nonce misuse.

Although this work focuses on the misuse of random numbers due to incorrect implementations, it would be useful to formally analyze other classes of implementation-related vulnerabilities. For instance, there are real-world protocols whose implementations miss to perform checks, especially when a given piece of information appears more than once in the exchanges (and are thus expected to be equal). Following a similar method as the one developed in this paper, future work could focus on the impact of missed checks in protocol implementations.

## REFERENCES

[1] Martín Abadi and Roger M. Needham. Prudent engineering practice for cryptographic protocols. In *IEEE Symposium on Research in Security and Privacy*, pages 122–136. IEEE Computer Society, 1994.

[2] Liliya Akhmetzyanova, Cas Cremers, Luke Garratt, Stanislav Smyshlyaev, and Nick Sullivan. Limiting the impact of unreliable randomness in deployed security protocols. In *IEEE 33rd Computer Security Foundations Symposium*, pages 277–287. IEEE Computer Society, 2020.

[3] Elena Andreeva, Andrey Bogdanov, Nilanjan Datta, Atul Luykx, Bart Mennink, Mridul Nandi, Elmar Tischhauser, and Kan Yasuda. The COLM Authenticated Encryption Scheme. *Journal of Cryptology*, 37:15, 2024.

[4] Alessandro Armando, David A. Basin, Yohan Boichut, Yannick Chevalier, Luca Compagna, Jorge Cuéllar, Paul Hankes Drielsma, Pierre-Cyrille Héam, Olga Kouchnarenko, Jacopo Mantovani, Sebastian Mödersheim, David von Oheimb, Michaël Rusinowitch, Judson Santiago, Mathieu Turuani, Luca Viganò, and Laurent Vigneron. The AVISPA tool for the automated validation of internet security protocols and applications. In *17th International Conference on Computer Aided Verification*, volume 3576 of *Lecture Notes in Computer Science*, pages 281–285. Springer, 2005.

[5] Gildas Avoine, Tristan Claverie, and Stéphanie Delaune. Formal Analysis of Random Nonce Misuses in Cryptographic Protocols. Technical report, May 2025. https://hal.science/hal-05066621.

[6] Gildas Avoine and Loïc Ferreira. Rescuing LoRaWAN 1.0. In *22nd International Conference on Financial Cryptography and Data Security*, volume 10957 of *Lecture Notes in Computer Science*, pages 253–271. Springer, 2018.

[7] Wenbo Bao. *Modern Cryptography – Theory and Practice*. Prentice Hall, Upper Saddle River, NJ, 2004.

[8] Elaine Barker. NIST Special Publication 800-102 – Recommendation for Digital Signature Timeliness, September 2009.

[9] David Basin, Cas Cremers, Jannik Dreier, and Ralf Sasse. Tamarin: Verification of large-scale, real-world, cryptographic protocols. *IEEE Security & Privacy*, 20(3):24–32, 2022.

[10] David Basin, Cas Cremers, and Simon Meier. Provably Repairing the ISO/IEC 9798 Standard for Entity Authentication. In *Principles of Security and Trust*, pages 129–148. Springer, 2012.

[11] David Beazley. PLY - Python Lex-Yacc. https://github.com/dabeaz/ply.

[12] Mihir Bellare, Shafi Goldwasser, and Daniele Micciancio. “Pseudo-random” number generation within cryptographic algorithms: The DSS case. In *Advances in Cryptology – CRYPTO '97*, pages 277–291. Springer, 1997.

[13] Mihir Bellare and Björn Tackmann. Nonce-Based Cryptography: Retaining Security When Randomness Fails. In *Advances in Cryptology – EUROCRYPT 2016*, pages 729–757. Springer, 2016.

[14] Ryad Benadjila and Arnaud Ébalard. Randomness of random in Cisco ASA. In *Symposium sur la Sécurité des Technologies de l'Information et de la Communication, SSTIC 2023*, pages 39–86. SSTC, 2023.

[15] Eli Biham and Lior Neumann. Breaking the Bluetooth Pairing - The Fixed Coordinate Invalid Curve Attack. In *26th International Conference on Selected Areas in Cryptography*, volume 11959 of *Lecture Notes in Computer Science*, pages 250–273. Springer, 2019.

[16] Ian Blake and Theodoulos Garefalakis. On the Security of the Digital Signature Algorithm. *Designs, Codes and Cryptography*, 26:87–96, 2002.

[17] Bruno Blanchet. Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. *Foundations and Trends in Privacy and Security*, 1(1-2):1–135, 2016.

[18] Bluetooth SIG. *Bluetooth Core Specification*, 2024. 6.0.

[19] Dominique Bongard. Offline bruteforce attack on WiFi Protected Setup. http://archive.hack.lu/2014/Hacklu2014_offline_bruteforceattack_on_wps.pdf, October 2014. Hack.LU.

[20] BSI. Cryptographic Mechanisms: Recommendations and Key Lengths – BSI TR-02102-1, February 2024.

[21] Michael Burrows, Martín Abadi, and Roger M. Needham. A logic of authentication. *ACM Transactions on Computer Systems*, 8(1):18–36, 1990.

[22] Vincent Cheval, Cas Cremers, Alexander Dax, Lucca Hirschi, Charlie Jacomme, and Steve Kremer. Hash gone bad: Automated discovery of protocol attacks that exploit hash function weaknesses. In *32nd USENIX Security Symposium*, pages 5899–5916. USENIX Association, 2023.
[23] Vincent Cheval, Charlie Jacomme, Steve Kremer, and Robert Künnemann. SAPIC+: protocol verifiers of the world, unite! In *31st USENIX Security Symposium*, pages 3935–3952. USENIX Association, 2022.

[24] Tristan Claverie, Gildas Avoine, Stéphanie Delaune, and José Lopes-Esteves. Tamarin-Based Analysis of Bluetooth Uncovers Two Practical Pairing Confusion Attacks. In *28th European Symposium on Research in Computer Security*, volume 14346 of *Lecture Notes in Computer Science*, pages 100–119. Springer, 2023.

[25] Benoît Cogliati and Yannick Seurin. EWCDM: An Efficient, Beyond-Birthday Secure, Nonce-Misuse Resistant MAC. In *Advances in Cryptology – CRYPTO 2016*, pages 121–149. Springer, 2016.

[26] Cas Cremers, Alexander Dax, Charlie Jacomme, and Mang Zhao. Automated analysis of protocols that use authenticated encryption: How subtle AEAD differences can impact protocol security. In *32nd USENIX Security Symposium*, pages 5935–5952. USENIX Association, 2023.

[27] Cas Cremers, Luke Garratt, Stanislav V. Smyshlyaev, Nick Sullivan, and Christopher A. Wood. RFC 8937: Randomness Improvements for Security Protocols. Internet Requests for Comments, October 2020.

[28] Cas Cremers and Dennis Jackson. Prime, Order Please! Revisiting Small Subgroup and Invalid Curve Attacks on Protocols using Diffie-Hellman. In *IEEE 32nd Computer Security Foundations Symposium*, pages 78–93. IEEE Computer Society, 2019.

[29] Cas Cremers, Benjamin Kiesel, and Niklas Medinger. A Formal Analysis of IEEE 802.11's WPA2: Countering the Kracks Caused by Cracking the Counters. In *29th USENIX Security Symposium*, pages 1–17. USENIX Association, 2020.

[30] Braden L. Crimmins, Dhanya Y. Narayanan, Drew Springall, and J. Alex Halderman. DVSorder: Ballot Randomization Flaws Threaten Voter Privacy. In *33rd USENIX Security Symposium*, pages 6525–6541. USENIX Association, 2024.

[31] Jannik Dreier, Charles Duménil, Steve Kremer, and Ralf Sasse. Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols. In *Principles of Security and Trust*, pages 117–140. Springer, 2017.

[32] Scott R. Fluhrer, Itsik Mantin, and Adi Shamir. Weaknesses in the Key Scheduling Algorithm of RC4. In *8th Annual International Workshop on Selected Areas in Cryptography*, volume 2259 of *Lecture Notes in Computer Science*, pages 1–24. Springer, 2001.

[33] Dan Harkins. RFC 7664: Dragonfly Key Exchange. Internet Requests for Comments, November 2015.

[34] Viet Tung Hoang, Reza Reyhanitabar, Phillip Rogaway, and Damian Vizár. Online Authenticated-Encryption and its Nonce-Reuse Misuse-Resistance. In *Advances in Cryptology – CRYPTO 2015*, pages 493–517. Springer, 2015.

[35] ISO Central Secretary. IT Security techniques — Entity authentication — Part 4: Mechanisms using a cryptographic check function. Standard ISO/IEC 9798-4:1999, International Organization for Standardization, Geneva, CH, 1999.

[36] ISO Central Secretary. IT Security techniques — Entity authentication — Part 2: Mechanisms using authenticated encryption. Standard ISO/IEC 9798-2:2019, International Organization for Standardization, Geneva, CH, 2019.

[37] ISO Central Secretary. IT Security techniques — Entity authentication — Part 3: Mechanisms using digital signature techniques. Standard ISO/IEC 9798-3:2019, International Organization for Standardization, Geneva, CH, 2019.

[38] Jérémy Jean, Ivica Nikolić, Thomas Peyrin, and Yannick Seurin. The Deoxys AEAD Family. *Journal of Cryptology*, 34, 2021.

[39] Antoine Joux. Authentication Failures in NIST version of GCM. Technical report, DGA, 2006.

[40] Ronald T. Kneusel. *Cryptographically Secure Pseudorandom Number Generators*, pages 189–207. Springer International Publishing, 2018.

[41] Kwok-yan Lam and Dieter Gollmann. Freshness assurance of authentication protocols. In *2nd European Symposium on Research in Computer Security*, pages 261–271. Springer, 1992.

[42] Andrew Y. Lindell. Comparison-Based Key Exchange and the Security of the Numeric Comparison Mode in Bluetooth v2.1. In *Topics in Cryptology – CT-RSA 2009*, volume 5473, pages 66–83. Springer, 2009.

[43] Gavin Lowe. An attack on the Needham-Schroeder public-key authentication protocol. *Information Processing Letters*, 56(3):131–133, 1995.

[44] Gavin Lowe. A Hierarchy of Authentication Specifications. In *10th IEEE Workshop on Computer Security Foundations*. IEEE Computer Society, 1997.

[45] Simon Meier, Benedikt Schmidt, Cas Cremers, and David A. Basin. The TAMARIN prover for the symbolic analysis of security protocols. In *25th Internation Conference on Computer Aided Verification*, volume 8044 of *Lecture Notes in Computer Science*, pages 696–701. Springer, 2013.

[46] Alfred Menezes, Paul C. van Oorschot, and Scott A. Vanstone. *Handbook of Applied Cryptography*. CRC Press, 1996.

[47] James Murray. *A New English Dictionary on Historical Principles*. Clarendon Press, Volume VI, Part II: M-N edition, 1908.

[48] Roger M. Needham and Michael D. Schroeder. Using Encryption for Authentication in Large Networks of Computers. *Communications of the ACM*, 21(12):993–999, 1978.

[49] Jonas Nick, Tim Ruffing, Yannick Seurin, and Pieter Wuille. MuSigDN: Schnorr Multi-Signatures with Verifiably Deterministic Nonces. In *2020 ACM Conference on Computer and Communications Security*, page 1717–1731. ACM, 2020.

[50] Karsten Nohl, David Evans, Starbug, and Henryk Plötz. Reverse-Engineering a Cryptographic RFID Tag. In *17th USENIX Security Symposium*, pages 185–194. USENIX Association, 2008.

[51] Thomas Pornin. RFC 6979: Deterministic Usage of the Digital Signature Algorithm (DSA) and Elliptic Curve Digital Signature Algorithm (ECDSA). Internet Request for Comments, 2013.

[52] Maïwenn Racouchot. *Formal analysis of security protocols: real-world case-studies and automated proof strategies*. PhD thesis, University of Lorraine, Nancy, France, 2024.

[53] Phillip Rogaway. Nonce-Based Symmetric Encryption. In *11th International Workshop on Fast Software Encryption*, volume 3017 of *Lecture Notes in Computer Science*, pages 348–359. Springer, 2004.

[54] Phillip Rogaway and Thomas Shrimpton. A Provable-Security Treatment of the Key-Wrap Problem. In *Advances in Cryptology - EUROCRYPT 2006*, pages 373–390. Springer, 2006.

[55] Benedikt Schmidt, Simon Meier, Cas Cremers, and David Basin. Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties. In *IEEE 25th Computer Security Foundations Symposium*, pages 78–94. IEEE Computer Society, 2012.

[56] Gustavus J. Simmons. Cryptanalysis and protocol failures. *Communications of the ACM*, 37(11):56–65, November 1994.

[57] Sornin, N. and Luis, M. and Eirich, T. and Kramp, T. and Hersent, O. LoRaWAN Specification, July 2016. LoRa Alliance, version 1.0.2.

[58] Sornin, N. and Yegin A. LoRaWAN 1.1 Specification, October 2017. LoRa Alliance, version 1.1.

[59] Jörn Tillmanns, Jiska Classen, Felix Rohrbach, and Matthias Hollick. Firmware Insider: Bluetooth Randomness is Mostly Random. In *14th USENIX Workshop on Offensive Technologies*. USENIX Association, 2020.

[60] Miles Tracy, Wayne Jansen, Karen Scarfone, and Theodore Winograd. NIST Special Publication 800-44 version 2 – Guidelines on Securing Public Web Servers, September 2007.

[61] Mathy Vanhoef and Frank Piessens. Key Reinstallation Attacks: Forcing Nonce Reuse in WPA2. In *ACM Conference on Computer and Communications Security*, pages 1313–1328. ACM, 2017.

[62] Mathy Vanhoef and Eyal Ronen. Dragonblood: Analyzing the Dragonfly Handshake of WPA3 and EAP-pwd. In *IEEE Symposium on Security and Privacy*, pages 517–533. IEEE Computer Society, 2020.

[63] Maximilian von Tschirschnitz, Ludwig Peuckert, Fabian Franzen, and Jens Grossklags. Method Confusion Attack on Bluetooth Pairing. In *42nd IEEE Symposium on Security and Privacy*, pages 1332–1347. IEEE Computer Society, 2021.

[64] Stephan Wesemeyer, Ioana Boureanu, Zach Smith, and Helen Treharne. Extensive Security Verification of the LoRaWAN Key-Establishment: Insecurities & Patches. In *IEEE European Symposium on Security and Privacy*, pages 425–444. IEEE Computer Society, 2020.

[65] Jiangliang Wu, Ruoyu Wu, Dongyan Xu, Dave (Jing) Tian, and Antonio Bianchi. Formal Model-Driven Discovery of Bluetooth Protocol Design Vulnerabilities. In *43rd IEEE Symposium on Security and Privacy*, pages 879–897. IEEE Computer Society, 2022.

[66] Sheikh Ziauddin and Bruno Martin. Formal Analysis of ISO/IEC 9798-2 Authentication Standard using AVISPA. In *8th Asia Joint Conference on Information Security*, pages 108–114, 2013.
<figure><img src="image_6.png" /><figcaption>Fig. 5. Protocol NSLPK</figcaption></figure>

with $m_1 = \langle 1, R_A, R_B, B, Text_2 \rangle$,
and $m_2 = \langle 2, R_B, R_A, A, Text_4 \rangle$.

<figure><img src="image_7.png" /><figcaption>Fig. 6. Protocol 9798-2-4</figcaption></figure>

with $m_1 = \langle 1, R_A, R_B, B, Text_2 \rangle$.

<caption>Fig. 8. Protocol 9798-4-4</caption>
<figure><img src="image_8.png" /></figure>

with $m_1 = \langle 1, R_A, k_{AB}, B, Text_4 \rangle$, $m_2 = \langle 2, R_B, k_{AB}, A, Text_3 \rangle$, and $m_3 = \langle 3, R_{A2}, R_B, Text_6 \rangle$.

<figure><img src="image_9.png" /><figcaption>Fig. 10. Four-Way Handshake</figcaption></figure>