Advances in quantum computing have shown a serious challenge for widely used current cryptographic techniques because a su cient large-scale quantum computer can e ciently solve hard mathematical problems on which the current public-key cryptography is relying. That is the reason why recently many researchers and industrial companies have spent lots of e ort on constructing post-quantum cryptosystems, which are resistant to quantum attackers. Large numbers of post-quantum key encapsulation mechanisms (KEMs) have been proposed to provide secure key establishment - one of the most important building blocks in asymmetric cryptography. This paper presents a formal security analysis of three lattice-based KEMs: Kyber, Saber, and SK-MLWR. We rst formally specify each of them in Maude, a rewriting logic-based speci cation and programming language equipped with many functionalities, such as a reachability analyzer (or the search command) that can be used as an invariant model checker, and then conduct invariant model checking with the Maude search command, nding an attack.
In recent years, advanced research in the eld of quantum computing and quantum information
theory has brought a credible threat to cryptosystems currently in use. The most popular
asymmetric (or public-key) primitives used today will become insecure against su ciently
strong quantum computers because they can be e ciently broken by Shor’s algorithm [
As a response to the quantum attack threat, there is extensive research to nd new schemes which are secure even in the presence of quantum adversaries. In the past few years, many post-quantum asymmetric primitives have been proposed as replacements for those traditional ones currently in use. The National Institute of Standards and Technology of USA (NIST) also started the Post-Quantum Cryptography Project in 2017, calling for proposals of post-quantum cryptographic protocols that are secure against both conventional and quantum computers1. There were 82 submissions to this standardization project, implying the importance of this problem. Among these submissions, a large number of proposals are for post-quantum key encapsulation mechanisms (KEMs), which aim to securely establish a symmetric key between two parties. This is understandable because key exchange algorithms are considered the most important building block of asymmetric cryptography.
Security analysis of cryptographic primitives and/or protocols can be fundamentally divided into two approaches: computational security and symbolic security. Proof in the computational model requires a de nition of secure cryptographic construction (primitive, protocol), and some assumptions about the computationally infeasible problem. The proof can be regarded as a mathematical reduction to the situation where the only chance to violate the security of such a construction is to solve the infeasible problem. The authors of the three KEMs considered in this paper have already presented their security proofs in the computational model. However, such proofs are often not easy to understand for non-experts in cryptography. On the other hand, symbolic analysis is easier to understand, computer-veri ed and suitable for automation. Our approach presented in this paper belongs to the latter. Note that our approach can be applied to not only the three KEMs but also other KEMs and other kinds of primitives as well.
We formally specify and model check three KEMs: Kyber [
Related work. In 2012, Blanchet [
Scyther [
Yadav et al. [
In the computational security approach, game-based model is known as a standard model for
proving security. Security for cryptographic primitives or protocols is de ned as an attack game
played between an adversary and some benign entity, which is called the challenger. The main
idea of the game-based security model is simulation of interaction among these two parties.
Eventually, the security proof typically leads to a proof that any supposed adversary can get
an advantage over the challenger if and only if he/she is able to solve some computationally
infeasible problem (e.g., discrete logarithm, integer factorization). When a proof becomes too
complicated, the proof normally employs the sequence of games technique [
Roadmap. The remaining of this paper is organized as follows: Section 2 gives some preliminaries, such as KEM and state machine. Section 3 describes Kyber KEM, brie y explains the underlying learning with error problem. The speci cation of Kyber in Maude is presented in Section 4. The model checking result and the attack found are presented in Section 5. Finally, Section 6 summarizes the paper.
A key encapsulation mechanism is a tuple of algorithms (KeyGen, Encaps, Decaps) along with a nite keyspace K: • KeyGen() ! (pk, sk): A probabilistic key generation algorithm that outputs a public key pk and a secret key sk. • Encaps(pk) ! (c, k): A probabilistic encapsulation algorithm that takes as input a public key pk, and outputs a ciphertext (or encapsulation) c and a key k 2 K . • Decaps(c, sk) ! k: A (usually deterministic) decapsulation algorithm that takes as input a ciphertext c and a secret key sk, and outputs a key k 2 K .
A state machine M , hS, I, T i consists of a set S of states, a set I ✓ S of initial states and a binary relation T ✓ S ⇥ S over states. The set R of reachable states with respect to M is inductively de ned as follows: (1) for each s 2 I , s 2 R and (2) for each (s, s0) 2 T , if s 2 R , then s0 2 R . A state predicate p is an invariant property with respect to M if and only if p(s) holds for all s 2 R .
In this paper, to express a state of S, we use a braced associative-commutative collection
of name-value pairs. Associative-commutative collections are called soups, and name-value
pairs are called observable components. That is, a state is expressed as a soup of observable
components. The juxtaposition operator is used as the constructor of soups. Let oc1, oc2, oc3 be
observable components, and then oc1 oc2 oc3 is the soup of those three observable components.
A state is of the form {oc1 oc2 oc3}. There are multiple possible ways to specify state transitions.
In this paper, we use Maude [
Maude provides the search command that can nd a state reachable from t such that the state matches p and satis es the condition(s) c:
search [n,m] in MOD : t =>* p such that c . where MOD is the name of the module specifying the state machine, and n and m are optional arguments denoting a bound on the number of desired solutions and the maximum depth of the search. n typically is 1 and t typically represents an initial state of the state machine.
Let B denote the set {0, . . . , 255}, i.e., the set of 8-bit unsigned integers (bytes). Consequently, Bk denotes the set of byte arrays of length k and B⇤ denotes the set of byte arrays of arbitrary length. For two byte arrays a and b, (a||b) denotes the concatenation of a and b.
The ring of integers modulo q is denoted by Zq. We denote by R the polynomial ring Z[X]/(Xn + 1) and by Rq the quotient polynomial ring Zq[X]/(Xn + 1). Thus polynomials in Rq are of n coe cients where each coe cient is in [0, q). In Kyber, the values of n and q are always xed to n = 256 and q = 7681 in all levels of security. Regular font letters denote elements in R or Rq (which includes elements in Z and Zq) and bold lower-case letters represent vectors with coe cients in R or Rq. By default, all vectors are column vectors. Bold upper-case letters are matrices. For a vector v (or matrix A), we denote by vT (or AT ) its transpose. For a vector v we write v[i] to denote its i-th entry (with indexing starting at zero); for a matrix A we write A[i][j] to denote the entry in row i and column j (again, with indexing starting at zero).
Let H and G be two hash functions, where H : B⇤ ! B32 and G : B⇤ ! B32 ⇥ B 32. Let KDF denote the key derivation function, where KDF : B⇤ ! B32. Let x 2 Q, where Q denotes the rational numbers set, then bxe denotes rounding of x to the closest integer. Let x 2 Zq and d < blog2 qe, functions Compress and Decompress are de ned by the following equations: Let x0 = Decompressq(Compressq(x, d), d), then we have:
Compressq(x, d) = b(2d/q) · xe mod 2d, Decompressq(x, d) = b(q/2d) · xe |x0 x mod q| b
q 2d+1 e (1) (2) (3) When Compressq and Decompressq are used with x 2 Rq or x 2 Rqk, they are applied to each coe cient individually. KEM.KeyGen() z B 32 (pk, sk0) = CPAPKE.KeyGen() sk = (sk0||pk||H(pk)||z) return (pk, sk) KEM.Dec(c, sk) (s||pk||H(pk)||z) = sk m0 = CPAPKE.Dec(c, s) (K¯ 0, r0) = G(m0||H(pk)) c0 = CPAPKE.Enc(pk, m0, r0) if c = c0 then return K = KDF(K¯ 0, H(c)) else return K = KDF(z, H(c))
! 3.2. Kyber Fig. 1 describes the three algorithms (KeyGen, Encaps, Decaps) of Kyber KEM. It employs the three algorithms (KeyGen, Enc, Dec) of Kyber.CPAPKE, which are shown in Fig. 2. Let us suppose that there are two parties Alice and Bob. The interactions depicted in Fig. 1 are as follows. Alice performs the KEM.KeyGen step, starting by choosing a random seed d, and hashing it to get the pair (⇢, ). From , she generates vector s serving as the secret key sk and vector e acting as an error component. t is then computed from s, e, and matrix A, which is generated from ⇢ . The pair of t and ⇢ serves as the public key pk, which is sent to Bob. Upon receiving pk, Bob executes the KEM.Enc step (i.e., Encaps step) in Fig. 1. He randomly chooses an m0, hashes it, and passes the outputs to the CPAPKE.Enc procedure (depicted in Fig. 2). The obtained ciphertext c, which is a pair of c1 and c2, is sent back to Alice. Upon receiving c, Alice performs the KEM.Dec step (i.e., Decaps step). She computes c0 by employing the CPAPKE.Dec and CPAPKE.Enc procedures. With a very high probability c0 is equal to c, implying that m0 on Alice’s side is equal to m on Bob’s side with an overwhelming probability. After that, they can derive the same key K. Note that all multiplications and additions in the two gures are computed over Zq[X]/(Xn + 1).
Note that in [
The procedure to generate matrix A, which is denoted by generate(⇢ ) in Fig. 2, taking as input a random seed ⇢ , is deterministic. Informally, if Alice and Bob share the same random seed ⇢ , then they can agreeingly derive the same matrix A, whose coe cients of each entry are close to a uniformly random distribution. In contrast, the procedure to sample noise (or error)
(c1||c2) = c u0 = Decompressq(c1, du) v0 = Decompressq(c2, dv) m0 = Compressq(v0 sT u0, 1) return m0 Figure 2: Kyber.CPAPKE
(t||⇢ ) = pk Rqk⇥ k 3 A = generate(⇢ ) Rqk 3 r, e1 sampleCBD(r) Rq 3 e2 sampleCBD(r) u = AT r + e1 v = tT r + e2 + Decompressq(m, 1) c1 = Compressq(u, du) c2 = Compressq(v, dv) return c = (c1||c2) components (e.g., e, e1, and e2), namely sampleCBD, is probabilistic. It takes as input a random seed (e.g., ⇢ and r) and returns a polynomial whose coe cients are close to a centered binomial distribution (to sample a vector, e.g., s and e, the procedure is called k times). Informally, coe cients of an output of sampleCBD are mostly close to 0, and their absolute value is never greater than a speci c small number (which is 5, or 4, or 3, depending on the level of security).
We rst introduce sort Poly that represents polynomials as follows: sort Poly . subsort Int < Poly . op _p+_ : Poly Poly -> Poly [ctor assoc comm prec 33] . op _p*_ : Poly Poly -> Poly [ctor assoc comm prec 31] . op _p-_ : Poly Poly -> Poly [prec 33] . op neg_ : Poly -> Poly [ctor] . where Int is the sort of integers. The notation subsort Int < Poly indicates that any integer is also a polynomial. p+, p*, and p- denote the addition, multiplication, and subtraction, respectively, between two polynomials. neg denotes the negation of a polynomial. assoc comm indicates that _p+_ and _p*_ are declared to be associative and commutative. prec 33 attached with _p+_ and _p-_ indicates that these operators have the same precedence 33, which is lower precedence than that of _p*_ (i.e., 31). Note that, we only consider polynomials in Zq[X]/(Xn + 1) (or Rq), where n = 256 and q = 7681. Let P1, P2, and P3 be variables of Poly. We declare some properties of the operators as follows: eq P1 p+ 0 = P1 . eq P1 p* 0 = 0 . eq P1 p* (P2 p+ P3) = (P1 p* P2) p+ (P1 p* P3) .
eq P1 p* 1 = P1 .
eq P1 p+ neg(P1) = 0 .
eq neg(P1 p+ P2) = neg(P1) p+ neg(P2) .
In a similar way, we introduce sorts Vector and Matrix representing polynomial vectors and matrices, respectively; operators v+, dot, and m* representing the addition & inner product of two polynomial vectors, and multiplication of a polynomial matrix and a vector, respectively. Let V1, V2, and V3 be variables of Vector. The declarations of the three operators and the distributive property of vectors are speci ed as follows: op _v+_ : Vector Vector -> Vector [assoc comm prec 33] . op _dot_ : Vector Vector -> Poly [prec 31] . op _m*_ : Matrix Vector -> Vector [prec 31] . eq (V1 v+ V2) dot V3 = (V1 dot V3) p+ (V2 dot V3) . eq V3 dot (V1 v+ V2) = (V3 dot V1) p+ (V3 dot V2) .
Two constructors for the two kinds of messages used in Kyber are as follows: op msg1 : Prin Prin Prin Vector Poly MsgState -> Msg [ctor] . op msg2 : Prin Prin Prin Vector Poly MsgState -> Msg [ctor] . where Prin is the sort representing principals, and Msg is the sort denoting messages. MsgState is the sort representing message states, receiving one of the following three values: sent the message was sent, replied - the message was sent and the receiver replied with another message, and intercepted - the message was intercepted by the intruder. The rst, second, and third arguments of each operator are the actual creator, the seeming sender, and the receiver of the corresponding message. The rst and last arguments are meta-information that is only available to the outside observer, while the remaining arguments can be seen by every principal. The fourth and fth arguments of msg1 carry the vector t and the random seed ⇢ , respectively, of the public key pk (pk is (t||⇢ ) as explained in Section 3.2). Similarly, the fourth and fth arguments of msg2 carry c1 and c2, respectively, of CPAPKE.
We model the network as a multiset of messages, in which the intruder can use as his/her storage. Consequently, the empty network (i.e., the empty multiset) means that no messages have been sent. The intruder can fully control the network, that is he/she can intercept any message, glean information from it, and fake a new message to any honest party. To formally specify Kyber in Maude, we use the following observable components: • (nw : msgs) - msgs is the soup of messages in the network; • (keys[p] : keys) - keys is a soup of the computed shared keys of principal p. Each entry of keys is in form of key(K,q), where K is the shared key and q is the principal whom p believes that he/she has communicated with; • (prins : ps) - ps is the collection of all principals participating in the protocol; • (d[p] : d0) - d0 is the random seed d (used in Fig. 2) of principal p; • (m[p] : m0) - m0 is the random seed m0 (shown in Fig. 1)) of principal p; • (rd-d : rdds) - rdds is a list of available values as the random seed d (we use list, but not set, to reduce the state space for searching). Each time when a principal makes a query for a random value of d, the top value in rdds is removed and returned to the principal; • (rd-m : rdms) - rdms is a list of the available values as random seed m0; • (glean-keys : gkeys) - gkeys is the soup of shared keys gleaned by the intruder; • (ds : ds) - ds is the collection of the random seeds d used by the intruder. Note that every entry in ds is di erent from any random value used by honest parties; • (ms : ms) - ms is the collection of random seeds m used by the intruder. Similarly to ds, every entry in ms is di erent from any random value used by honest parties.
Each state in SKyber is expressed as {obs}, where obs is a soup of those observable components. We suppose that there are two honest principals alice and bob together with a malicious one, namely eve, participating in Kyber KEM. The initial state init of IKyber is de ned as follows: {(nw: empty) (prins: (alice bob eve)) (rd-d: (d1 , d2)) (rd-m: (m1 , m2)) (keys[alice]: empty) (keys[bob]: empty) (glean-keys: empty) (d[alice]: 0) (d[bob]: 0) (m[alice]: 0) (m[bob]: 0) (ds: empty) (ms: empty)} .
With the honest parties, we specify three transitions: keygen, encaps, and decaps, which correspond to the three steps of the mechanism. Let OCs be a variable of observable component soups, A, B, and C be variables of principals (possibly intruder), and PS be a variable of principal collections. Let D, M, M2, M’, Rho, RhoA, V, V’, CV, and P1 be variables of polynomials, and PoL be a variable of polynomial lists. Let G and H denote the hash functions G and H, respectively. Let MS be a variable of networks (i.e., message soups). The rewrite rule keygen is de ned as follows: crl [keygen] : {(rd-d: (D, PoL)) (d[A]: P1) (prins: (A B PS)) (nw: MS) OCs} => {(rd-d: PoL) (d[A]: D) (prins: (A B PS)) (nw: (MS msg1(A,A,B, sample-A(1st(RhoSig)) m* sample-s(2nd(RhoSig)) v+ sample-e(2nd(RhoSig)), 1st(RhoSig), sent))) OCs} if RhoSig := G(D) . where RhoSig is a variable denoting a pair of polynomials, 1st and 2nd are its projection operators. sample-A, sample-e, and sample-s represent the sampling procedures, outputting the matrix A, the vectors e, and s, respectively. The rewrite rule says that when there exists a polynomial D in rd-d, A picks it as a random seed d, builds a message msg1 exactly following the KeyGen() step of the mechanism, and sends it to B. d[A] is set to D, and D is removed from rd-d.
The rewrite rule encap is de ned as follows: crl [encap] : {(rd-m: (M, PoL)) (m[B]: P1) (keys[B]: KS)
(nw: (msg1(C,A,B,T,Rho,sent) MS)) OCs} => {(rd-m: PoL) (m[B]: M) (keys[B]: (KS key(KDF(1st(Kr), H’(CU,CV)), A))) (nw: (msg1(C,A,B,T,Rho,replied) msg2(B,B,A, CU, CV, sent) MS)) OCs} if M’ := H(M) /\ Kr := G(pair(M’, H’(T, Rho))) /\
CU := enc-u(T, Rho, M’, 2nd(Kr)) /\ CV := enc-v(T, Rho, M’, 2nd(Kr)) . where T and CU are variables of polynomial vectors, Kr is a variable denoting a pair of polynomials, and KS is a variable representing a soup of shared keys. Let Rseed be a variable of polynomials. Let sample-r, sample-e1, and sample-e2 represent the procedures sampling r, e1, and e2, respectively. Following the CPAPKE.Enc(pk, m, r) in Fig. 2, enc-u and enc-v are de ned as follows: eq enc-u(T,Rho,M,Rseed) =
compr(tp(sample-A(Rho)) m* sample-r(Rseed) v+ sample-e1(Rseed),du) . eq enc-v(T,Rho,M,Rseed) =
compr(tpV(T) dot sample-r(Rseed) p+ sample-e2(Rseed) p+ decompr(M,1),dv) . where tp(A) denotes the transpose matrix of A and tpV(T) denotes the transpose vector of T. du and dv are constants of natural numbers, denoting du and dv, respectively. decompr(M,1) and compr(M,1) denote Decompressq(M, 1) and Compressq(M, 1), respectively. enc-u(T,Rho,M ,Rseed) and enc-v(T,Rho,M,Rseed) compute c1 and c2, respectively, in Fig. 2 given as inputs T||Rho, M, Rseed. The rewrite rule encaps says that when there exists a message msg1 sent from A to B in the network, B builds a message msg2 exactly following the Encaps() step of Kyber, sends it back to A. B also computes the shared key with A, and the state of the message msg1 is updated to replied.
The rewrite rule decaps is de ned as follows: crl [decaps] : {(d[A]: D) (keys[A]: KS)
(nw: (msg1(A,A,B,T,Rho,MsgStat) msg2(C,B,A, CU, CV, sent) MS)) OCs} => {(d[A]: D) (keys[A]: (KS key(KDF(1st(Kr2), H’(CU,CV)), B)))
(nw: (msg1(A,A,B,T,Rho,MsgStat) msg2(C,B,A, CU, CV, replied) MS)) OCs} if RhoSig := G(D) /\ Rho == 1st(RhoSig) /\
T == sample-A(Rho) m* sample-s(2nd(RhoSig)) v+ sample-e(2nd(RhoSig)) /\ U’ := decompr(CU, du) /\ V’ := decompr(CV, dv) /\ M2 := compr(V’ p- tpV(sample-s(2nd(RhoSig))) dot U’, 1) /\ Kr2 := G(pair(M2, H’(T, Rho))) /\ enc-u(T,Rho,M2,2nd(Kr2)) == CU /\ enc-v(T,Rho,M2,2nd(Kr2)) == CV . where MsgStat is a variable representing an arbitrary message state. The rewrite rule says that when A has sent a message msg1 to B and there exists a message msg2 replied from B to A in the network, A follows the Decaps() step of Kyber, computes the shared key with B. We only consider the overwhelming case, i.e., Alice successfully recovers m. We assume that the error tolerance gaps made by error components always be silent, making m0 equals to m. This is done by the following equation: ceq compr(E0 p+ decompr(M,1),1) = M if isSmall?(E0) . where E0 is a variable of sort Poly, and isSmall?(E0) is a predicate, returning true if all coe cients of E0 are small in comparison with q. Sampling procedures for s, e, r, e1, and e2 return vectors or polynomials whose coe cients are small. These properties are speci ed by the following equations: eq isSmall?(sample-s(P)) = true . eq isSmall?(sample-e1(P)) = true . eq isSmall?(sample-r(P)) = true .
eq isSmall?(sample-e(P)) = true . eq isSmall?(sample-e2(P)) = true . Using Eq. 3, we rewrite Decompressq(Compressq(v, dv), dv) and Decompressq( Compressq(u, du), du) by v + ✏1 and u + ✏2, respectively, where all coe cients of ✏1 and ✏2 are small in comparison with those of v and u. In the speci cation, we specify ✏1 as epsilon1(v), ✏2 as epsilon2(u), and both epsilon1(v) & epsilon2(u) are “small”. This is done by the following equations: eq decompr(compr(V,dv),dv) = V p+ epsilon1(V) . eq decompr(compr(U,du),du) = U v+ epsilon2(U) . eq isSmall?(epsilon1(V)) = true . eq isSmall?(epsilon2(U)) = true .
We suppose that there is one intruder, namely eve, participating in the mechanism. When there exists a message msg1 sent from A to B in the network, the intruder can intercept that message, fake a new message, and send it to the receiver. This behavior is speci ed by the following rewrite rule: crl [keygen-eve] : {(ds: (D PoC1)) (nw: (msg1(A,A,B,TA,RhoA,sent) MS)) OCs} => {(ds: (D PoC1)) (nw: (msg1(A,A,B,TA,RhoA,intercepted) msg1(eve,A,B,sample-A(1st(RhoSig)) m* sample-s(2nd(RhoSig)) v+ sample-e(2nd(RhoSig)),1st(RhoSig),sent) MS)) OCs} if RhoSig := G(D) . where PoC1 and PoC3 are variables representing arbitrary soups of polynomials. The intercepted message must have state sent at the beginning, which means that the message has not reached the receiver. eve then constructs a new faking message from an available value D for the random seed d. This kind of random value cannot be gleaned from the network, but eve can only construct it by randomly choosing a new value as the rewrite rule build-ds as follows: rl [build-ds] : {(rd-d: (D, PoL)) (ds: PoC1) OCs} => {(rd-d: PoL) (ds: (PoC1 D)) OCs} .
Similarly, the only way in which eve can construct values for the random seed m is by randomly choosing a new value. This is speci ed by the following rewrite rule build-ms: rl [build-ms] : {(rd-m: (M, PoL)) (ms: PoC3) OCs} => {(rd-m: PoL) (ms: (PoC3 M)) OCs} .
Two more rewrite rules are introduced as follows: crl [encaps-eve] : {(ms: (M PoC3)) (glean-keys: KS)
(nw: (msg1(A,A,B,TA,RhoA,intercepted) MS)) OCs} => {(ms: (M PoC3)) (glean-keys: (key(KDF(1st(Kr),H’(CU,CV)),A) KS)) (nw: (msg1(A,A,B,TA,RhoA,intercepted) msg2(eve,B,A,CU,CV,sent) MS)) OCs} if M’ := H(M) /\ Kr := G(pair(M’,H’(TA,RhoA))) /\
CU := enc-u(TA,RhoA,M’,2nd(Kr)) /\ CV := enc-v(TA,RhoA,M’,2nd(Kr)) /\ msg2(eve,B,A,CU,CV,sent) \in MS = false /\ msg2(eve,B,A,CU,CV,replied) \in MS = false . crl [decaps-eve] : {(ds: (D PoC1)) (glean-keys: KS) (nw: (msg1(eve,A,B,T,Rho,replied) msg2(B,B,A,CUB,CVB,sent) MS)) OCs} encaps-eve says that when eve has intercepted a message msg1 sent from A to B, eve fakes a new message msg2, sends it to A, and computes a shared secret key with A. decaps-eve says that when eve has faked a new message msg1, sent it to B, and B on his/her belief that the message truly comes from A has replied to A a message msg2, eve intercepts the message msg2, and computes a shared secret key with B.
We introduce the following search command:
search [
(glean-keys: (key(K1,alice) key(K2,bob) KS)) OCs} . where K1 and K2 are variables that denote arbitrary shared keys. K1 may or may not be equal to K2. The command tries to nd a state reachable from init such that: alice in her belief obtains the shared key K1 with bob, bob in his belief obtains the shared key K2 with alice, and eve owns both K1 and K2. Maude found a counterexample, and this kind of vulnerability belongs to MITM attacks. Fig. 3 shows how this attack happens on Kyber, which is visualized from the path leading to the counterexample Maude returned. There are mainly ve steps as follows: Step 1. Alice wants to construct a shared key with Bob, she starts by performing KEM.KeyGen(), generating a public key pk and a secret key sk. She keeps sk, and sends pk to Bob. Step 2. Eve intercepts the rst message sent from Alice to Bob. She takes a random de, follows the KEM.KeyGen() step to generate a pair (pke, ske), and sends pke to Bob.
Step 3. Bob receives pke thinking it is from Alice. As a response, he takes a random m0, performs KEM.Enc(pke), and obtains a ciphertext c and a shared key Kb. He sends the ciphertext c back to Alice, and keeps the key Kb, which he believes that it is the shared key obtained by him and Alice.
Step 4. Eve intercepts the replied message which contains ciphertext c sent from Bob to Alice. She rst performs KEM.Dec(c, ske) to obtain the shared key Kb. She then takes a random me0, performs KEM.Enc(pk), and obtains a ciphertext ce and a shared key Ka. She sends the ciphertext ce back to Alice as a response for the rst message.
Step 5. Alice receives the ciphertext ce thinking it is from Bob. She performs KEM.Dec(ce, sk) to obtain the shared key Ka. She believes that Ka is the shared key obtained by her and Bob.
The reachable state space in the experiment is nite. Indeed, if we try to run the following command: search in KYBER : init =>* {OCs} ., the number of returned solutions is nite,
Alice z B 32 (pk, sk0) = PKE.KeyGen() sk = (sk0||pk||H(pk)||z) return (pk, sk) !
pk m0 = PKE.Dec(ce, s) (K¯ 0, r0) = G(m0||H(pk)) c0 = PKE.Enc(pk, m0, r0) if ce = c0 then return Ka = KDF(K¯ 0, H(ce)) ce de B 32 (⇢ e, e) = G(de) Rqk⇥ k 3 Ae = generate(⇢ e) Rqk 3 se, ee sampleCBD( e) te = Aese + ee pke = (te||⇢ e) ske = se return (pke, ske) !
pke m0b = PKE.Dec(c, se) (K¯ 0b, rb0) = G(m0b||H(pke)) c0b = PKE.Enc(pke, m0e, re0) if c = c0b then return Kb = KDF(K¯ 0b, H(c)) me0 B 32 me = H(me0) (K¯ e, re) = G(me||H(pk)) ce = PKE.Enc(pk, me, re) Ka = KDF(K¯ e, H(ce)) return (ce, Ka) c m0 B 32 m = H(m0) (K¯ , r) = G(m||H(pke)) c = PKE.Enc(pke, m, r) Kb = KDF(K¯ , H(c)) return (c, Kb) implying that the state space is nite. We give a brief explanation of this fact. Each state is denoted as a braced associative-commutative soup of the ten observable components as shown in Section 4. The key point is that the numbers of possible values that each observable component (i.e., a name-value pair) can receive is nite. Indeed, ps in (prins : ps) is always (alice bob eve) because there is no rewrite rule that changes it. rdds and rdms in (rd-d : rdds) and (rd-m : rdms) never consist of more than (d1,d2) and (m1,m2), respectively, because there is no rewrite rule that inserts element(s) into them. d0 and m0 in (d[p] : d0) and (m[p] : m0) can only be in the sets {d1, d2} and {m1, m2}, respectively. Similarly, the numbers of possible values for ds and ms in (ds : ds) and (ms : ms) are nite. msgs in (nw : msgs) consists of nite messages because (1) each of the two rewrite rules keygen and encaps adds a new message into the network, but simultaneously it also removes one element from rdds and rdms (note that rdds and rdms never consist of more than (d1,d2) and (m1,m2) as shown above); (2) the rewrite rule keygen-eve adds a new message msg2 into the network, but simultaneously it also changes the status of an existing message msg1 from sent to intercepted, thus, keygen-eve can only be applied nitely many times; and (3) the rewrite rule encaps-eve only adds a new message msg2 into the network if that message does not exist before (note that the other rewrite rules does not change the network or only update the status of messages). Similarly, keys in (keys[p] : keys) consists of nite entries because: the rewrite rule encaps removes one element from rdms; and the rewrite rule decaps changes the status of an existing message msg2 from sent to replied. In the same manner, we can show gkeys in (glean-keys : gkeys) is nite. In summary, we can conclude that the state space in our experiment is nite. Consequently, with a search command to nd a state satisfying some conditions, in nite time Maude will either nd no solutions or will nd a state satisfying the conditions.
Remark. Readers may argue that this kind of attack is not a novel attack since Kyber is not equipped with any feature for dealing with authentication. We agree on it. The paper instead illustrates one symbolic approach for reasoning about KEMs rather than focusing on this kind of attack. Our ultimate goal is to come up with a new security analysis/veri cation technique for post-quantum cryptographic protocols, such as post-quantum TLS. Such protocols use post-quantum cryptographic primitives, such as KEMs. Formally specifying such primitives is necessary to analyze the security. What is described in the paper is our initial step toward the goal.
Saber and SK-MLWR. In the same manner, we formalize the two other KEMs, i.e., Saber [
We have presented an approach to security analysis of some lattice-based KEMs in the symbolic model. We rst used Maude as a speci cation language to formally specify the KEMs. After that, by employing Maude search command, an MITM attack was found for each KEM. The occurrence of the attack is basically because a KEM alone does not come with an authentication solution.
Researchers have proposed a post-quantum TLS protocol [