Modelling and verification of post-quantum key encapsulation mechanisms using Maude

Kyber

Kyber (Avanzi et al., 2019) is an IND-CCA2-secure key encapsulation mechanism whose security is based on the hardness of solving the learning-with-errors (LWE) problem over module lattices. Kyber works with vectors and matrices of polynomials with various operations, such as concatenation, transposition, product or other more complex ones, such as hash and key derivation functions. These operations are present in the main functions KeyGen, Enc and Dec, depicted in Figs. 13 and 14. It is important to clarify that the algorithms in both figures represent an instance of the algorithms previously explained with Fig. 12 in ‘Behaviour’. Specifically, Figure 13 shows three algorithms that encapsulate the ones present in Fig. 14. The encapsulation is done to provide further security measures as stated by Avanzi et al. (2019). The algorithms on the left, KeyGen and Dec, are executed by the initiator of the protocol. Meanwhile, the algorithm on the right, Enc, is run by the other participant.

Furthermore, In Fig. 13 it should be noted that in algorithm CCAKEM.Dec, when the sub-function CPAPKE.Dec(s,(u,v)) takes place, the computed text m′ could not be the same as the one generated by the other participant in CCAKEM.Enc. This different message m′ is a value close to m given the property isSmall(p) over a polynomial p. We say that a polynomial p is small when its degree is lower than a given number established by the protocol. This approximately equal value m′ is then used to compute a new, but also close, value c′, which is compared to the received c in a message. Depending on their equality, the construction of the shared key will be different from the key derivation function (KDF). This differentiation of values arises with low probability (Avanzi et al., 2019), but it states that the encryption and decryption phases are not error-prone.

Nevertheless, why are they different in the end? To answer this question is to understand the strength of the scheme against a quantum adversary. If we check the most internal functions, that is, the CPAPKE ones shown in Fig. 14, we can see in algorithm CPAPKE.Enc that there are vector values such as e₁ and e₂ that have been sampled with a random seed r using function sampleCBD from a centred binomial distribution. These values add randomness to the computations, thus making the computations harder to replicate or break. (1)${\displaystyle Decompres{s}_q\left(Compres{s}_q\left(X,1\right),1\right)=X^{\prime }}$

Function Decompress_q processes the error when extracting from the pair of vectors c₁ and c₂ the vectors u and v respectively, at the middle of step CPAPKE.Dec. This function has a property in combination with function Compress_q, which states in Eq. (1) that decompressing the compress of a given value X with the same second parameters, gives a new value X′ which is similar to the original compressed value. This property takes place while computing the original message m as it is shown in Eq. (2), present at the end of the Dec algorithm in Fig. 14. (2)${\displaystyle m=Compress\left(v^{\prime }-s^T{\mathbf{u}}^{\prime },1\right)}$

It is important to mention that other operations take place, such as generate, sampleCBD, Compress, Decompress, encode and decode. These are necessary for the main three operations we have described before but are not explained in detail in this article because they are not necessary for the understanding of the protocol. Full descriptions of these specific functions are available at Avanzi et al. (2019).

BIKE

BIKE (Aragon et al., 2017), which stands for BIt-flipping Key Encapsulation, is a code-based key encapsulation mechanism. Figure 15 shows BIKE’s specific algorithms. Although the previous KEM Kyber is lattice-based and this KEM BIKE is code-based, they follow a similar structure, and BIKE’s algorithms are an instance of the functionalities of ‘Behaviour’.

The key part of this KEM is how the decapsulation algorithm, to process the received ciphertext, manages to recover the original tuple of errors computed during the encapsulation step. To better understand the process, we first need to know where the errors are added. Looking at Fig. 15 we can see in step Encaps, line 3, that C is computed as a tuple of values (c₀, c₁). The first element, c₀, is defined as e₀ + e₁h, being $h=h_1{h}_0^{-1}$ the public key previously received and (e₀, e₁) the tuple of error values we are looking for. The second element, c₁, encapsulates the value m performing the exclusive or operation with a hash function $L:{\mathcal{R}}^2\to \mathcal{M}$ on the two same error values. This value m holds significant importance since it is used to compute, through other hash function $H:\mathcal{M}\to {ϵ}_t$, the pair of error values, (e₀, e₁), specifically in line 2.

Now, on the Decaps step line 1, present also in Fig. 15, e′ will be the result of applying the decoder function on c₀ with the components of the public key h, that is, the tuple h₀ and h₁. This decoding algorithm will ideally return a pair of errors equal to those of e from the Encaps step such that e₀h₀ + e₁h₁ = s, where s represents the first parameter of decoder. Since we managed to extract the original errors with high probability, we are able to compute m′ on line 2 applying exclusive or over c₁ = m⊕L(e₀, e₁) and L(e₀, e₁). It is important to note that similar to the previous KEM, m′ here is named to denote that the computed value may not be the same since the decoder function might fail with low probability. Thanks to two properties of exclusive or, we will get the original m. The first property is where X⊕X = 0, and the second property has to do with X⊕0 = X. The combination of these two properties allows us to compute in line 3 the same shared key using another hash function K.

Another operation also takes place and is fully defined by Aragon et al. (2017). The concrete algorithm is Black-Gray-Flip, and it implements the decoder. It is necessary for the decoding of a ciphertext, but we do not explain it in detail because it is not necessary for the understanding of the protocol.

Classic McEliece

Classic McEliece (Chou et al., 2022) is a code-based key encapsulation mechanism designed to achieve IND-CCA2 security. Even though it is code-based, like BIKE, and follows the same steps all KEMs do, it is a new instance, providing new algorithms for each of the three main functions for key generation, encapsulation and decapsulation.

The key part for this specific instance of a KEM resides at the ENCODE and DECODE functions, and the role they play in the encapsulation and decapsulation algorithms, respectively. Figure 16 shows, in algorithm Enc line 2, the application of function ENCODE over some error e with the public key T to get the ciphertext C. A careful reader can see the resemblance between BIKE’s encapsulation and this one because some sampled or generated error is being “encapsulated” with the public key previously received. Then the shared key is computed using a hash function $H:{\left\{0,1\right\}}^8\times {\mathbb{F}}_2^n\times {\mathbb{F}}_2^{mt}\to {\mathbb{F}}_2^l$.

In algorithm Dec, values s and Γ′ are extracted from the private key computed with SeededKeyGen, that is, KeyGen. With these values, the application of function DECODE manages to decapsulate the original error e. This is done thanks to the idea represented in Eq. (3). Furthermore, notice that even if the decoding process can fail, i.e., returning e as ⊥, there is a way in which the shared key can be computed thanks to the existence of some error correction mechanisms. (3)${\displaystyle DECODE\left(ENCODE\left(E,T\right),{\Gamma }^{\prime }\right)=E}$

It is important to note that although the second argument of DECODE and ENCODE are different, they share a common value. If we expand the values with their specific construction definitions, i.e., the specific functions used in their computations, we get that T is the first component from the output of MATGEN(Γ) while Γ′ is the last component from the same output. With this discovery, we get a relation between the two, in principle, distinct values, so when the same matrix generation function has been used to compute the two values, the property defined in Eq. (3) holds.

As with previous KEMs, other operations take place. For Classic McEliece it is MatGen, Encode, Decode, Irreducible, FieldOrdering and FixedWeight. These are necessary for the main three operations we have described before but are not explained in detail here because only a high-level representation is needed for the specification. Full descriptions of these specific functions are available at Chou et al. (2022).

Dolev-Yao

The Dolev-Yao adversary model was first introduced by Dolev & Yao (1983). In that article, the authors explained that public-key schemes are secure against adversaries that cannot modify the environment, which is unrealistic. That is why they presented different examples of protocols whose security properties could be compromised if an intruder can take action over the messages of a network. An intruder can be either passive or active over a network where other participants send and receive messages during, for example, a handshake protocol or a key exchange scheme. The passive intruder can only read the message and extract raw content from it, meaning they cannot derive any information from messages without the proper private key. The active intruder can read messages, modify them, and send them through the network. It is essential to clarify that the intruder is considered a polynomial-time Turing machine.

In their seminal work, the authors proposed the Dolev-Yao intruder model. This model states the capabilities an intruder has over a network. Such capabilities are:

• Intruder can obtain any message that is passing through the network.

• He is a legitimate user of the network. That is, he can do any actions an honest participant can.

• The intruder has the opportunity to be a receiver to any participant. That is, he can receive messages from other participants.

It must be noted that the network participants, the intruder included, must comply with the following assumptions:

• One-way functions are unbreakable. In other words, the basic primitives of the protocol are considered to be non-reversible.

• The protocol definition cannot be changed and must be followed by any participant. A user cannot do undefined steps during the protocol execution.

• Public keys can be used for encryption by everyone.

• Private keys can decrypt messages encrypted by the corresponding public key.

Kyber

In the case of the KEM known as Kyber, we make some assumptions on the mathematical aspects of the data types we try to represent. We also assume certain qualities of some operations. In the case of basic data types, we assume that all matrices are square matrices and that vectors are column vectors, considering transposed vectors as row vectors. Vectors, representing polynomials, are considered to be of the necessary degree to be considered small, thus fulfilling the property isSmall(p) explained in ‘Kyber’. Related to the qualities of some operations, we only consider for the decompression function the ideal case where there is no error in obtaining m. Thus, m′ will be equal to m. Furthermore, we assume that the deciphered message is the shared key between the participants, so no additional functions, such as KDF, need to be specified and applied. Finally, our sampling procedures are deterministic, but we will assume that the operators sampled are from a CBD whenever it is the case.

BIKE

Regarding the assumptions made over the symbolic model of BIKE, we have some inherited from the specification provided by Aragon et al. (2017) and the rest are made over operation decoder. From the specification, we inherit the assumption for Hardness of Quasi Cyclic Syndrome Decoding (QCSD) and Hardness of Quasi Cyclic Codeword Finding (QCCF), needed for code-based KEM. We also assume indistinguishability in two aspects. First, we assume it for the public key, i.e., $h_1{h}_0^{-1}$ from random $\left(h_o,h_1\right)\stackrel{\$}{\leftarrow }{\mathcal{H}}_w$. Second, assume indistinguishability of the first half of the ciphertext c, i.e., (e₀ + e₁h) where $h=h_1{h}_0^{-1}$, from random $\left(\left(e_0,e_1\right),h\right)\stackrel{\$}{\leftarrow }{\varepsilon }_t\times \mathcal{R}$. We assume the decoder function is correct and always returns the correct pair of errors, so we assume no decoding failure, i.e., σ = 0.

Classic McEliece

With Classic McEliece, we focus on operational assumptions regarding its decoding algorithm DECODE. As per the specification given by Chou et al. (2022), algorithm DECODE has two possible outputs. On the first one, the original errors are recovered given some conditions, i.e., there exists a weight-t vector $e\in {\mathbb{F}}_2^n$ such that C = He with H = (I_mt|T), then DECODE (C, Γ′) = e. The second condition is when the ciphertext does not have the form He, so DECODE returns DECODE (C, Γ′) = $\perp$. For this reason, we assume that all applications of DECODE always return the original errors; thus, C always has the form He for any weight-t vector $e\in {\mathbb{F}}_2^n$.

Functional modules

MODEL-CONFIGURATION.

Module that sets the basic structure of the system upon which the KEM will work on. We first define the participants, explaining their structure and components. Also, related to their components, we define some notation so participants can store and identify different types of keys and encrypted texts, linking those to a participant. Then the message syntax is set. Finally, we define the global state, where participants send and receive messages. All these element definitions are the same for the three KEMs we have defined following the framework.

Participants in our model follow the operational definition shown in Fig. 18. Here three identifiers are declared for our corresponding participants. Then the structure of a participant is declared. A participant consists of an Identifier, like the ones that have been defined, a group of keys the participant know, and a group of elements that represent its elements that are not keys and the participant has in its possession, that is, in its memory.

Shared between all KEMs, these operators have the purpose of storing a relation between a cryptography component and a participant. Examples of such cryptography components are the notion of types of keys such as public, secret and shared keys, or a ciphertext. Figure 19 shows the definition of the former, where sorts PKey and SKey represent the publicly available keys and secret keys, only known to the creator and or corresponding peer, respectively.

Messages are defined by the operator msg shown in Fig. 20. A message contains information about two participant identifiers, the status of the message and the content it carries. The first identifier indicates the source of the message, and the second is the identifier of the participant to whom the message is delivered throw the network. Then, the status of a message can take the values sentX and receivedX, where X can either be PK or C for public key or ciphertext, respectively, depicting in part the current step over the network. At last, the content of the message is assumed to be secure, meaning a participant can not infer any additional contents from it without the required information.

Figure 21 shows the definition of the structure representing our system. Here, and from left to right, the elements our rules will handle are specified. At the right corner, we assigned a field between symbols { and } for all the available sample values. These samples are modelled as constant values representing symbolic values, to use in any of the Keygen, Enc or Dec steps. Next, we have an associative and commutative set of participants between symbols < and >, following the structure explained at the beginning of this section. Then, at the left end, we have the network, with a collection of associative messages representing a kind of record that lets participants work over the sent messages. All this together gives us a proper term structure that can represent any network with any participants and messages being sent and received.

System module

With the system module identified as the name of the corresponding KEM, we try to model the behaviour of honest participants and the intruder’s capabilities over the network, that is, the global state we defined. The first thing to do in this module is to declare the sampling sets of values needed to perform a session of the key exchange. Once the samples are defined, we can start defining the honest participant behaviour, following the explanation in ‘Behaviour’. These rules specify the transitions of our formal system regarding the three main functions known as KeyGen, Enc and Dec, and also model the sending and receiving of both the public key and the ciphered text over the network. Lastly, we check the specific intruder behaviour following the Dolev-Yao intruder model assumptions and represent such capabilities over the network messages.

Initial set up: Before modelling the behaviour, we need to declare the sampling groups and the initial states upon which the symbolic model would start to run the simulation. Sampling groups are represented as operators that can store sampling values of some type. Such operators are placed at the sample set of the global state. The population in these operators should be minimal, that is, the minimal set of values required to carry on a protocol session of a KEM. In this way, and since our approach is symbolic, with many different symbolic values, we would be representing the same thing, so by keeping it minimal, we are avoiding redundancy. We can now declare the initial global states with the specific sampling sets, participants and the network channel. Such initial states can be seen as snapshots of the network. An example is shown in Fig. 22 following the required samples for KYBER, where sampling sets ds, ms and rs contain one corresponding sampling value, participants Alice, Bob and Eve have empty key sets and no peer assigned, and the network is empty.

Participant behaviour: Following the different KEMs’ specifications and the Dolev-Yao assumptions, we specify the following rules in Maude to model how the different KEMs operate. All these rules have been written to be as general as possible, making the model and the constructed execution tree more realistic and compelling for model checking. It is important to note that the main differences between each rule related to the three main functions are the conditions, which help to model how the sample values and other functions are used to construct the cryptography elements like keys and ciphered texts between others. To properly explain the participant behaviour rules, we will first show a more general rule without the conditionals, which is almost the same for all the KEMs. Then, we will show the conditionals of each KEM and link it to the original algorithm we showed in ‘Security Fundamentals’.

The first rule is KeyGen as seen in Fig. 23. This rule is the one that starts the protocol for a given participant. Specifically, the rule states that given a participant with identifier ID1 whose set of keys is empty and has no peer associated, he can generate a publicKey(ID1, PK) and a secretKey(ID1, SK) in the group of keys, linked to the identifier ID1 of the participant. Specifically, for each protocol, the necessary samples should be present in CONT4, the pool of available sampled sets.

We also defined two rules available in Fig. 24 .The first rule, SendPK, models the behaviour of a participant with his public key, sending it to any other participant in the network different from him. The message is sent if it has not been sent previously, so we avoid infinite execution. Then, to complement the first rule, we defined rule ReceivePK to process an incoming message if it contains a public key and has not been received yet.

Rule Enc, as it is shown in Fig. 25, models the function with its same name. In order to apply the encryption step, a participant first has to receive the public key from the other peer, which is why the left-hand side of the rule has a component publicKey(ID1, PK). The participant also needs to be able to sample the necessary values from the set of samples CONT4, just like in rule KeyGen. After applying the rule, the participant possesses in the pool of keys a new shared key SK related to his current peer ID1. In the content pool, the ciphertext C is stored as the value to be transmitted securely to the other participant.

The counterpart of SendPK but for a ciphered text c obtained through Enc is the conditional rule SendCiph. As Fig. 26 shows, it checks similar conditions when sending the public key, so no infinite execution happens. Then, the rule to receive a ciphertext behaves similarly to its counterpart, that is, ReceivePk. The rule is applied when there is a sent message in the network for a given participant with ID1. The content of the message is stored by the participant in its pool of content, acting as memory.

Finally, the rule to decipher the received ciphertext is Dec. Figure 27 depicts the behaviour of a participant ID1 with his own secret key SK and an assigned peer ID2. Once the shared key K1 for participant ID2, that is the peer, has been computed and placed in the pool of keys, the peer can be removed since the protocol session has ended between them.

Intruder behaviour: When specifying the intruder’s capabilities over our module, we decided to specify two rules, Intercept1 and Intercept2, both identical between all the KEMs’ symbolic models. The former can be seen in Fig. 28, and it binds the intruder with the ability to intercept a sent message containing a public key. The intercepted message is modified by extracting the body, that is the public key It is carrying, and replacing it with its own public key. This modification makes the receiver think the public key received is from the sender when it is not, thus beginning the man-in-the-middle attack. The latter is available in Fig. 29 and makes the intruder intercept a message sent with a ciphertext. This intercepted message is sent by the receiver from the previous fake message and makes Eve send a new message but with his own ciphertext. In this way, Eve has in store two ciphertexts, her own and the one intercepted.

KeyGen.

Regarding the construction of public and secret keys, this is done through the matching equations in the rule’s conditions available in Fig. 30. The structure is the one present at the specification and previously depicted in Fig. 14, where public key PK is the matrix A, obtained through function generateA, multiplied by the secret key s plus a sampled error e. For the secret key SK, we assumed it to be the output value from a CBD using the function sampleS, so no further operations are needed for its computation.

Enc.

As in the KeyGen rule, the conditions of Enc are used to construct the needed cryptography elements. In this case, a ciphered text c consisting of a pair of ciphered texts, denoted as c₁ and c₂. Both elements are specified following the operations in Fig. 14. The conditions constructing the two elements of C are available in Fig. 31. Before them, we also had to define variables U and V that represent the vectors u and v, respectively. Constant values du and dv symbolically represent the corresponding constants from the parameters of the protocol.

Dec.

Figure 32 shows the multiple conditions necessary to compute the shared key, denoted with variable K1. The matching equations for U’ and V’ allow us to extract the original U and V, presented in Fig. 31, thanks to the equational theory regarding functions Compress and Decompress. Furthermore, the definition of the shared key K1 matches the equational theory for error cancellation represented by Eq. (2).

KeyGen.

On the specific conditions related to the conditional rule KeyGen, we can notice in Fig. 33 that we only symbolically represent the computation of the public key. The reason to omit the representation of any possible secret key is that it can be recovered later in terms of the components used to compute the public key. Remember, from Fig. 15 that the KeyGen algorithm is defined to first sample two values $\left(h_0,h_1\right)\leftarrow \mathcal{D}{\mathcal{H}}_w$, and uses them in the computation of the public key $h=h_1{h}_0^{-1}$. Finally, it samples a value $\sigma \stackrel{\$}{\leftarrow }\mathcal{M}$ which is stored alongside values (h₀, h₁) as a private key. We decided not to model the last sampling since it is for later use in the Dec step if the decoder fails. Since such a path is not possible because we assume zero decoding failure rate, as stated in the assumptions of ‘BIKE’, we simplify the model.

Enc.

The conditions of Enc are built to model all the steps of the encapsulation without exception. Figure 34 shows, between others, the computation of the errors as E0 and E1, the definition of the ciphertext as a tuple stored in Cs and the computation of the shared key through the hashing function K using the sampled value SAM1 and the ciphertext Cs.

Dec.

With a similar structure, the conditions of the rewrite rule for Dec are defined to represent all aspects present in the specification. Figure 35 depicts such a representation. It is important to note that since we didn’t store the full secret key, we can, in a very elegant way, prepare the decoder to extract the errors from the first component of the ciphertext, as we explained before in this section with the property related to the decoder. Furthermore, the equational theory regarding the exclusive or operation helps to obtain the value m. It is now that the equational theory plays an important role, both for the decoder and for the exclusive or operation xorD.

KeyGen.

The adaptation from the specification code provided by Chou et al. (2022) to our symbolic model regarding the key generation step represented by rule KeyGen is done directly over function SeededKeyGen from Fig. 16. This function is essentially the key generation algorithm. It comprises many other functions we use to obtain certain values to construct the public and secret keys. For the public key PK, we can see in Fig. 36 that it is the resulting value at the head from the matrix generation function known as MATGEN. In the case of the secret key SK, it is not a specific value but a set of values. The set of values for the secret key comprises a sample SAM1 and some elements from the output of MATGEN and other elements that derive from them.

Enc.

The encapsulation algorithm is straightforward. Figure 37 shows that we only need to model three values. First, the error is represented with variable ER through the result of the function FIXEDWEIGHT. Then we set variable C, which represents the ciphertext, as the encoding of the error with the public key. Finally, as with all KEMs, the shared key computation comes from one of the encapsulation step sides. To this end, we modelled the hash function H with a preset value one along the error and ciphertext as subsequent parameters.

Dec.

The algorithm for the decapsulation is portrayed in Fig. 38. Two elements from the secret key SK are extracted to construct what is then stored in variable GAMMA’. This variable represents Γ′ from line 2 at step Dec in Fig. 16. With this newly constructed value and the application of DECODE over C with GAMMA’, we get the original error thanks to our equational theory. Finally, similar to the previous step, the shared key is computed with the same inputs, thus obtaining the same key.

There are some capabilities an intruder might want to perform in BIKE. These capabilities take advantage of possible design vulnerabilities, allowing an intruder to subtract certain information from another participant that might later come as valuable knowledge. The new capabilities imply two rules depicted in Fig. 39. The first rule implies that an intruder might modify or send a message where the public key sent to Bob is equal to one. This public key was not generated by the intruder using the key generation function and thus has certain implications. One implication is that upon its construction, h₀ =  = h₁, so when computing pk = h₁∗(h₀)⁻¹ = 1. Also, with this public key, the encapsulation function becomes the identity function. The second rule represents the capabilities of the intruder to differentiate from a message the two components of the ciphertext, i.e., c₀ and c₁. Also, the conditions of the second rule represent the intruder taking advantage of the design vulnerability regarding the implementation of hash function L to obtain the generated value m_B, which is the basis for the shared key, depicted in the rule as SK, computation.

Correctness

The search for states where the protocol terminates is successful for both initial states in any of the three symbolic models. This means honest participants, Alice and Bob, share the same key after following the specified rules. This demonstrates that our model works regarding the respective specifications of Kyber (Avanzi et al., 2019), Bike (Aragon et al., 2017) and Classic McEliece (Chou et al., 2022).

Man-in-the-middle

Regarding the second search, it returns solutions only for the case of the second initial state init2 over the three symbolic models. This implies some trace of state transitions, also known in the security area as an attack vector, are present during the simulations, leading to insecure states. We analyze the first solution because all other solutions fit this view.

The attack vector is depicted in Fig. 43 as a pseudo-network diagram. Here, the participants in our model are displayed, with the steps of the protocol represented as boxes and the messages as directed arrows. The black dots in the malicious participant, known as EVE, are the intercept capabilities at work. As we see depicted by the diagram, when this malicious agent Eve modifies the messages sent by Alice, it supplants the identity since the public key of the new message is from Eve. This also takes place the other way around, when the message sent by Bob is intercepted, and the ciphertext is modified to the one generated by Eve using Alice’s public key. In both cases, Eve uses the gleaned contents to its advantage. First, the gleaned public key is used in the Enc step to generate a shared key without Alice being aware. Second, after intercepting the second message, Eve can perform the Dec step with the gleaned ciphertext since it was encapsulated using her own public key. In this way, Eve possesses the necessary information in certain moments to carry out a man-in-the-middle attack between Alice and Bob, the two honest participants of the network.

Design vulnerability

Some of the states that the second search command finds for the symbolic model of BIKE are due to a vulnerability in the KEM’s design. As stated in ‘BIKE Specification’, some properties might arise due to poor implementation decisions. The combination of these new properties with an intruder taking advantage of the possible design flaws leads to cases where the intruder can learn sampling values that can later be reused due to implementation decisions.

A trace of the vulnerability can be found in Fig. 44. Here an intruder, let us refer to it as Eve, might choose to start a communication with some honest participant, Bob. Since the intruder could not follow the cryptography primitive KeyGen, Eve decides to use a public key h = h₁∗(h₀)⁻¹ such that h₀ = h₁ so h = 1. Once Bob receives the public key, thinking it is from Alice, he applies the encapsulation function with it and sends back a message with the resulting ciphertext. Eve then intercepts the message, and if Bob’s implementation satisfies the property L(e₀, e₁) = L(e₀ + e₁), then she is able to compute the shared key without the need for a decapsulation function. Eve was able to learn critical information using a weak key and a vulnerability of the exclusive or function. The specific application of the exclusive or operation can be seen at the end of the timeline of Eve in Fig. 44. Basically, Eve extracts c₀ from the sent ciphertext by Bob and uses it in the hash function L to apply the exclusive or operation over the second part of the sent ciphertext, c₁.

Although this design vulnerability may not seem very relevant, it requires some extra checks by future implementations to ensure that (i) weak keys are not accepted and (ii) a proper implementation must not satisfy the L(e₀, e₁) = L(e₀ + e₁) algebraic property. An extra possible solution is the use of authentication or integrity checks on the messages in the network. This makes Bob avoid any message that is not from a trusted participant or that has been altered.

Predicates

In order to use model checking in Maude, one needs two things: a system module representing the system to check and some predicates to define properties through formulas. The system module has already been defined and tested, and now we dive into the three specified predicates for model checking.

Predicate wantsToShareKey, depicted in Fig. 45, is defined so it holds in a global state where a participant with identifier ID1 has his own public key, meaning he has performed the KeyGen step, and there is a message to another participant, with identifier ID2, different than him. This predicate represents a participant wanting to share a key with another. In other words, it is the start of any of the specified KEMs.

Predicate sharedAKeyWith, depicted in Fig. 46, is defined so it is true when two participants, ID1 and ID2, hold the same shared key K1. This predicate would then represent the end of the KEM execution, fulfilling the previous predicate in which the KEM was started.

Finally, predicate stolenSharedKey is depicted in Fig. 47. The predicate holds in any state where the shared key a participant has with another one is present in the pool of keys of a different participant. It is important to notice that we do not require that the third participant has or does not have the shared key.

Properties

With the predicates defined, we now specify three properties. One security property stating something bad never happens. One liveness property to state something good eventually happens. One property to check the fairness of our system. We write these properties as LTL formulas, allowing us to explore the execution tree in search of counterexamples. If no counterexample is found, we can say with assurance that the property holds in our symbolic model.

KEY SHARING.

This liveness property checks that whenever Alice wants to share a key with Bob, they eventually do so. This natural language description can be expressed in LTL notation as ${\displaystyle \square \left(P\to ◊Q\right)}$ where P = wantsToShareKey(Alice, Bob) and Q = sharedAKeyWith(Alice, Bob). Even though Eve is not specified in the formula it is present in the analyzed execution paths.

Results

About the execution of our LTL formulas, we have applied the three of them over our two initial states, init1 and init2, for the three protocols. The results are that both initial states accomplish the liveness (KEY SHARING) and fairness property when Alice and Bob want to share a key, in any of the three KEMs symbolic models. We get different results per the security property concerning SECRECY. For the KEM’s symbolic models of Classic McEliece and Kyber, the property holds in the initial state init1. In the case of the initial state init2, it does not hold due to the MITM attack that was reported with the reachability analysis. In the case of the symbolic model of BIKE, the only case where the property holds is in the initial state init1 when the participant is Alice and the thief is Eve. The property does not hold when the participant is Bob, due to the design’s vulnerability, and when the initial state is init2, because of the MITM attack.

To replicate these experiments, in the GitHub repository, there is a text file named as each of the KEMs. These documents present the commands one needs to execute to replicate the search and model checking we have presented.