Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel version

View article
PeerJ Computer Science

Main article text

 

Introduction

  1. The secrecy property of the ECDH shared secret key established between two honest principals. Par-Maude-NPA found a counterexample of this property at depth 12 in the time T = 1722 h (72 days), while Maude-NPA did not find it in T.

  2. The secrecy property of the PQ KEM shared secret key established between two honest principals. As the same time T, Par-Maude-NPA did not find any counterexample of this property up to depth 12, and neither did Maude-NPA up to depth 10.

  3. The authentication property, which states that if client A has completed the handshake, apparently with server B, then B is the actual principal who has communicated with A. As the same time T, Par-Maude-NPA did not find any counterexample up to depth 18, and neither did Maude-NPA up to depth 17.

Preliminaries

Functional modules

 
fmod    
M
 
is 
(Σ, E)
 
endfm 
. Σ is an order-sorted signature, which may contain a set of the following declarations:
  • importations of previously defined modules (

     
    protecting    
    … or
     
    extending 
    … or
     
    including 
    …)

  • sorts and subsorts (

     
    sort    
    s
     
    . 
    or
     
    sorts 
    s s
     
    . 
    or
     
    subsort 
    s
     
    < 
    s
     
    . 
    )

  • function symbols (

     
    op    
    f
     
    : 
    s1 … sn  →  s [att1 …  attk]
     
    . 
    )

  • variables (

     
    vars    
    v v
     
    . 
    )

 
assoc    
for associativity and
 
comm 
for commutativity.
 
eq    
t
 
= 
t
 
. 
) or conditional (
 
ceq 
t
 
= 
t
 
if 
cond
 
. 
), where t and t′ are terms and cond is a conjunction of equations (e.g., t
  
= 
t′). Equations are used as equational rules to perform the simplification in which instances of the left-hand side pattern that match subterms of a subject term are replaced by the corresponding instances of the right-hand side. The process is called term rewriting and the result of simplifying a term is called its normal form.

System modules

 
mod    
R
 
is 
(Σ, ER)
 
endm 
. Σ and E are the same as those in an equational theory. R may contain a collection of rewrite rules, which may be either unconditional (
 
rl [ 
label
 
] 
 
: 
u
 
=> 
v
  
. 
) or conditional (
 
crl [ 
label
 
] 
 
: 
u
 
=> 
v
 
if 
cond
 
. 
), where label is a name; u and v are terms; and cond is a conjunction of equations and/or rewrites (e.g., t 
 
=>  
  t′). Rewrite rules are also computed by rewriting from left to right modulo the equations in the system module and regarded as local transition rules, making many possible state transitions from a given state in a concurrent system.

Narrowing

 
c    
) and apples (
 
a 
) with dollars ($) and quarters (
 
q 
). A cake costs a dollar while an apple costs three quarters (specified by the rewrite rules
 
buy-c 
and
 
buy-a 
, respectively). Only dollars are allowed to buy cakes and apples. However, the machine can change four quarters into a dollar (the equation
 
change 
). The complete specification of the machine is as follows:
 
 
mod NARROWING-VENDING-MACHINE is 
  sorts Coin Item Marking Money State . 
  subsort Coin < Money . 
  op empty : -> Money . 
  op __ : Money Money -> Money [assoc comm id: empty] . 
  subsort Money Item < Marking . 
  op __ : Marking Marking -> Marking [assoc comm id: empty] . 
  op <_> : Marking -> State . 
  ops $ q : -> Coin . 
  ops c a : -> Item . 
  var M : Marking . 
  rl [buy-a] : < M $ > => < M a q > [narrowing] . 
  rl [buy-c] : < M $ > => < M c > [narrowing] . 
  eq [change] : q q q q M = $ M [variant] . 
endm    
 
<_>    
specifies the machine state. The attributes in the
 
__ 
operators state that they are associative and commutative and have the identity element
 
empty 
. The attributes
 
narrowing 
and
 
variant 
are specially used for narrowing and variant-based equational unification algorithms (Escobar, Sasse & Meseguer, 2010), i.e., only rewrite rules and equations with these attributes are used to perform the algorithms. Let us consider a term
 
< M1 > 
as an initial state that only contains a variable of the sort
 
Money 
. There would be several traces from the initial state by using narrowing. At each narrowing step, we must choose which subterm of the subject term, which rewrite rule of the specification, and which instantiation on the variables of the subterm and the left-hand side of the rewrite rule (or which unifier (or substitution) of the subterm and the left-hand side of the rewrite rule) are going to be considered. Each narrowing step applied to a given state produces a new branch in the reachability tree. For example, for each rewrite rule of the machine, there is only one unifier that makes the initial state
  
< M1 > 
equal the left-hand side of the rewrite rule. Therefore, with one narrowing step, there are only two possible cases, producing two successor states from the initial state as follows:
 
 
< M1 > ⇝σ1,  buy-a  < a q M2 > 
< M1 > ⇝σ′ 
1,  buy-c  < c M2’ >    
 
M2 
and
 
M2’ 
are variables of the sort
 
Money 
and the substitutions are σ1 =
 
M1 
 
M2, M ↦→ M2 and σ′1   = M1 ↦→ M2’ 
,
 
M 
 
M2’ 
with the rewrite rules
  
buy-a 
and
 
buy-c 
, respectively. Note that
 
M 
in the substitutions is the variable used in the left-hand side of the rewrite rules. From the successor state
 
< a q M2 > 
, two more consecutive narrowing steps may be performed as follows:
 
 
< M1 > ⇝σ1,  buy-a  < a q M2 > ⇝σ2,  buy-c  < a c q M3 > ⇝σ3,  buy-a  < a a c q M4 >    
 
M3 
and
 
M4 
are variables of the sort
 
Money 
and the substitutions are σ2 =
 
 
   {M2 ↦→ M3, M ↦→ a q M3} and σ3  =  { M3 ↦→ q q q M4, M ↦→ a c M4} with 
the rewrite rules buy-c and buy-a, respectively.  In the third nar- 
rowing step, when we apply the substitution σ3, the two obtained in- 
stances of < a c q M3 > and the left-hand side of the rewrite rule buy-a 
are < a c q q q q M4 > and < a c M4 > 
, respectively. The two instances are actually equal, thanks to the commutative property and the equation
 
change 
. Therefore, the rewrite rule
 
buy-a 
modulo the equational theory is used to obtain the state
 
< a a c q M4 >  
. From what has been described, it follows that by using narrowing, we can solve the reachability problem where St and St′ are patterns (terms that may have variables in common) of the sort
 
State 
such that some conditions are satisfied, and RE are the rewrite rules and equations in the specification.

Par-Maude-NPA

Hybrid Post-Quantum TLS 1.2

 
Encaps    
, see the “Protocol Formal Specification in Maude-NPA” section). Before that, however, if S has previously sent a CertificateRequest message, meaning that client authentication was requested, C must send their certificate (a Certificate message) first. Furthermore, if client authentication was requested, following the ClientKeyExchange message, C will then send a CertificateV erify message, that is a signature over all handshake messages exchanged so far signed by C’s long-term private key. Finally, C sends a ClientFinished message, whose content is a hash of all handshake messages exchanged so far encrypted by the negotiated handshake key.

Protocol formal specification in Maude-NPA

Formal specification by strands

  1. P → Q:pk(QPNP)

  2. Q → P:pk(PNPNQQ)

  3. P → Q:pk(QNQ)

 
Msg    
that represents messages and the sort
 
Fresh 
that is used to identify terms that must be unique. To model the protocol in Maude-NPA, we first introduce some new sorts, such as
 
Name 
and
 
Nonce 
to distinguish principal names and nonces, respectively. The two sorts are subsorts of the sort
 
Msg 
, which are declared as follows:
 
 
sorts Name Nonce . 
subsort Name Nonce < Msg .    
 
 
op n : Name Fresh -> Nonce [frozen] .    
 
frozen 
attribute is attached following the Maude-NPA convention, which is necessary to tell Maude not to attempt to apply rewriting/narrowing at the arguments of this operator. Suppose that
 
P 
and
 
r 
respectively are variables of the sorts
 
Name 
and
 
Fresh 
, then
 
n(P,r) 
denotes the nonce generated by
 
P 
, where
 
r 
guarantees its uniqueness. We also declare the public encryption operator as follows:
 
 
op pk : Name Msg -> Msg [frozen] .    
 
Q 
and
 
N 
be variables of the sorts
 
Name 
and
 
Nonce 
, respectively. The strand specifying the protocol execution from the P side is then defined as follows:
 
 
:: r :: 
[ nil | +(pk(Q, P ; n(P,r))), -(pk(P, n(P,r) ; N ; Q)), +(pk(Q, N)), nil ]    
 
r 
,
 
P 
consumes it to generate the nonce
 
n(P,r) 
and sends the nonce to
 
Q 
together with
 
P 
’s identifiers encrypted by
 
Q 
’s public key. When
 
P 
receives another message whose content is
 
n(P,r) 
, another nonce
  
N 
, and
 
Q 
’s identifiers encrypted under
 
P 
’s public key (which can be checked by using their secret key to decrypt the received ciphertext),
 
P 
replies to
 
Q 
the new nonce
 
N 
encrypted under
 
Q 
’s public key. Recall that
 
:: r:: 
denotes the unique fresh
 
r 
which is consumed by the first output message of the strand and all messages are put after the vertical bar following the Maude-NPA convention because the vertical bar is irrelevant when specifying the protocol execution. Note also that
  
; 
is the infix operator of message concatenation, which has signature declaration as follows:
 
 
op _;_ : Msg Msg -> Msg [frozen] .    
 
 
:: r :: 
[ nil | -(pk(Q, P ; N)), +(pk(P, N ; n(Q,r) ; Q)), -(pk(Q, n(Q,r))), nil ]    
 
 
:: nil :: [ nil | -(M), +pk(P,M), nil ]    
 
M 
is a variable of the sort
 
Msg 
. Precisely, the strand says that if the intruder has learned the message
 
M 
, then the intruder can encrypt it by the public key of any principal (
 
P 
).

Protocol formal specification

KEM specification

 
KeyGen    
,
 
Encaps 
,
 
Decaps 
) along with a finite key space K:
  •  
    KeyGen    
    () →(pksk): A probabilistic key generation algorithm, which generates a public & secret key pair pk & sk.

  •  
    Encaps    
    (pk) →(ck): A probabilistic encapsulation algorithm, which takes as input a public key pk and generates an encapsulation (or ciphertext) c and a shared key kK.

  •  
    Decaps    
    (csk) →k: A deterministic decapsulation algorithm, which takes as inputs a ciphertext c and a secret key sk, and returns as output a shared key kK.

 
KeyGen    
() and (ck)←
 
Encaps 
(pk), it holds that:
 
Decaps    
([csk ≠ k] ≤ ϵ
 
Decaps    
cannot recover the correct shared key k. In most cases, ϵ would be negligible, and when ϵ = 0, we say the KEM is correct. In this article, we only consider the case that all KEMs are correct, which means that
 
Encaps 
and
 
Decaps 
always correctly return the same shared key k. Idealizing assumptions like that are typically necessary when conducting security analysis in the symbolic model. Furthermore, because a
 
Decaps 
-failure probability is really small, typically almost 0, we are not over-idealizing when omitting such
 
Decaps 
-failure cases. For example, with Kyber, that failure probability is below 2−140 (Bos et al., 2018), i.e., Kyber is ϵ- correct with ϵ < 2−140.
 
PqSk    
,
 
PqPk 
,
 
Cipher 
, and
 
PqKey 
to represent secret keys, public keys, encapsulations, and shared keys, respectively. The constructor of a secret key is specified by the following operator:
 
 
op pqSk : Name Fresh -> PqSk [frozen] .    
 
Fresh 
provides the uniqueness of secret keys, while the argument of the sort
 
Name 
is not strictly necessary, but it is convenient for identifying who is the owner of a given key.
 
Decaps    
algorithm is straightforwardly declared as follows:
 
 
op decap : Cipher PqSk -> PqKey [frozen] .    
 
Decaps 
, it is a bit tricky to specify the
 
KeyGen 
and
 
Encaps 
procedures because they are probabilistic algorithms. For each of the two procedures, we add an argument of the sort
 
PqSk 
to make them become deterministic procedures. With the
 
Encaps 
procedures, we declare two separate Maude operators:
 
encapCipher 
and
 
encapKey 
that return the ciphertext c and the key k, respectively. We declare the following operators:
 
 
op pqPk         : PqSk       -> PqPk    [frozen] . 
op encapCipher : PqPk PqSk -> Cipher [frozen] . 
op encapKey     : PqPk PqSk -> PqKey  [frozen] .    
 
KeyGen 
procedure, while the two others model the
 
Encaps 
procedure. The algebraic properties of KEMs are then specified by means of equations as follows:
 
 
op $pqKey : PqSk PqSk -> PqKey [frozen] . 
eq encapKey(pqPk(S:PqSk), S2:PqSk) = $pqKey(S:PqSk, S2:PqSk) [variant] . 
eq decap(encapCipher(pqPk(S:PqSk),S2:PqSk), S:PqSk) 
    = $pqKey(S:PqSk, S2:PqSk) [variant] .    
 
variant 
attribute denotes that the two equations are not regular Maude equations used for simplification, but are equations used for variant-based equational unification (Escobar, Sasse & Meseguer, 2010). Here we introduce one more operator, namely
 
$pqKey 
, which is necessary for specifying that the rewritings of
 
encapKey 
and
 
decap 
(
 
Encaps 
and
 
Decaps 
steps) on proper arguments will result in the same key. The first equation can be straightforwardly comprehended. The second equation states that given an encapsulation en and a secret key sk, a principal can perform
  
Decaps 
(ensk) to get the proper shared key only if en is the result of
 
Encaps 
when taking as input the public key associated with the secret key sk.

ECDH and key calculation specification

 
 
sort Scalar Point ECKey . 
subsort Point < ECKey .    
 
Point    
represents points on the curve, which serve as ECDH public keys. The sort
 
Scalar 
and
 
ECKey 
represent the secret keys and shared keys, respectively. We then declare the following operators:
 
 
op p    : -> Point . 
op scl : Name Fresh     -> Scalar [frozen] . 
op gen : Point Scalar   -> Point  [frozen] . 
op _*_ : Scalar Scalar -> Scalar [frozen assoc comm] .    
 
p 
denotes a point generator on the curve, which is publicly known by all participants including the intruder. The operator
 
scl 
takes as inputs a principal name and a fresh, and outputs a scalar, which serves as a secret key. The operator
 
gen 
takes as inputs a point and a (secret) scalar and outputs another point. Concretely, when the first argument is a point generator, the result is a public key, which is used to send to the other peer; and when the first argument is a public key received from the opposite peer, the result is a shared key. The last operator is the associative-commutative multiplication operation on scalars, thanks to the Maude attributes
 
assoc 
and
 
comm 
. The algebraic property of ECDH is then specified by the following equation:
 
 
eq gen(gen(P:Point, S:Scalar), S2:Scalar) 
  = gen(P:Point, S:Scalar * S2:Scalar) [variant] .    
 
PreMasterSecret 
and
 
MasterSecret 
are introduced to represent premaster secrets and master secrets, respectively, in the protocol key calculation. We then model their calculations with the following operators:
 
 
op pms : ECKey PqKey -> PreMasterSecret [frozen] . 
op ms  : PreMasterSecret Rand Rand Point Cipher -> MasterSecret [frozen] .    
 
Rand 
is the sort representing random numbers generated by clients and servers. A pre-master secret is the concatenation of an ECDH shared secret and a PQ KEM shared secret. Whereas, a master secret is computed by the pseudorandom function (PRF) taking as inputs a pre-master secret and a seed, which is the combination of the two random numbers previously exchanged in the two Hello messages and the ECDH public key & PQ encapsulation previously sent in the ClientKeyExchange message.

Honest principal specification

 
rd    
,
 
sess 
, and
 
cert 
that serve as functions to produce random numbers, session IDs, and digital certificates, respectively. We also define operators
 
sig 
and
 
enc 
reflecting the signature and symmetric encryption functions. All of them are as follows:
 
 
op rd    : Name Fresh -> Rand [frozen] . 
op sess : Name Fresh -> Session [frozen] . 
op cert : Name -> Cert [frozen] . 
op sig  : Name Msg -> Msg [frozen] . 
op enc  : MasterSecret Msg -> Msg [frozen] .    
 
S    
, a message
 
M 
, and a master-secret
 
MS 
,
 
enc(MS,M) 
denotes the ciphertext obtained by encrypting
 
M 
by
 
MS 
, while
 
sig(S,M) 
denotes the signature over message
 
M 
signed by the long-term private key of server
 
S 
. By using the principal name as an input argument for the signature sign function instead of the private key (for example,
  
sig(priKey(S),M) 
), we implicitly associate a long-term private key with its owner’s name. For the sake of simplicity and for reducing the size of the state space,
 
cert(S) 
is used to denote the digital certificate of the server
 
S 
, while in fact, the certificate must contain information about the trusted certificate authority and the public key of
 
S 
. By using that simplification form, we explicitly associate a certificate with its owner’s name and ignore the case when the intruder tries to fake a certificate.
 
r1    
,
 
r2 
, and
 
r3 
be variables of the sort
 
Fresh 
;
 
C 
and
 
S 
be variables of the sort
 
Name 
;
 
N 
and
 
SS 
be variables of the sorts
  
Rand 
and
 
Session 
, respectively;
 
PK1 
and
 
PK2 
be variables of the sorts
 
Point 
and
 
PqPk 
, respectively. The execution of the protocol of Fig. 1 up to the ClientFinished message from a client’s side is specified as follows:
 
 
:: r1,r2,r3 :: 
[ nil | 
 +(ch ; rd(C,r1)), 
 -(sh ; N ; SS), 
 -(sc ; cert(S)), 
 -(ske ; PK1 ; PK2 ; sig(S, PK1 ; PK2 ; rd(C,r1) ; N)), 
 +(cke ; gen(p,scl(C,r2)) ; encapCipher(PK2, pqSk(C,r3))), 
 +(cf ; enc(ms(pms(gen(PK1,scl(C,r2)), encapKey(PK2, pqSk(C,r3))), 
          rd(C,r1), N, gen(p,scl(C,r2)), encapCipher(PK2, pqSk(C,r3))), 
     (ch ; rd(C,r1)) ++ 
     (sh ; N ; SS) ++ 
     (sc ; cert(S)) ++ 
     (ske ; PK1 ; PK2 ; sig(S, PK1 ; PK2 ; rd(C,r1) ; N)) ++ 
     (cke ; gen(p,scl(C,r2)) ; encapCipher(PK2, pqSk(C,r3)))) 
  ), 
nil ]    
 
ch 
,
 
sh 
,
 
sc 
,
 
ske 
,
 
cke 
, and
  
cf 
are constants of the sort
 
Msg 
, which are acronyms of ClientHello, ServerHello, Server Certificate, ServerKeyExchange, ClientKeyExchange, and ClientFinished. The
 
++ 
operator denotes message concatenation. The strand says that the client
 
C 
starts a new connection with the server
 
S 
by sending a ClientHello message with a random number denoted by
 
rd(C,r1) 
. When the client receives a ServerHello message, a valid server Certificate message, and a valid ServerKeyExchange message with ECDH and PQ public keys, i.e.,
 
PK1 
and
 
PK2  
, the client will send a ClientKeyExchange message with the client’s ECDH public key exchange and the encapsulation computed with
 
PK2 
as one of the inputs. Then, the client also sends a ClientFinished message, that is the concatenation (denoted by
 
++ 
) of all messages exchanged so far encrypted under the master secret. Note that for the sake of simplicity and for reducing the size of the state space, we use master secrets as symmetric keys for encryption of Finished messages. However, the correct protocol design states such a symmetric key must be computed by the PRF function taking as inputs the master secret and the two random numbers in the two Hello messages sent in the same session. Moreover, the ServerHelloDone message and some components of the Hello messages, such as protocol versions, cipher suites, and lists of cipher suites, are excluded. We also suppose that client authentication is not requested. Note also that the use of the concatenation operator
 
++ 
is not strictly necessary. For example, from the definition of
 
++ 
, it follows that
 
(sh ; N ; SS) ++ (sc ; cert(S)) 
is rewritten to
 
(sh ; N ; SS ; sc ; cert(S)) 
. Therefore,
  
++ 
can be omitted without posing any technical problems. However, we define and keep on using it because we want to show each message separately for ease of understanding from readers.
 
 
:: r1,r2,r3,r4 :: 
[ nil | 
 -(ch ; N), 
 +(sh ; rd(S,r1) ; sess(S,r2)), 
 +(sc ; cert(S)), 
 +(ske ; gen(p,scl(S,r3)) ; pqPk(pqSk(S,r4)) ; 
      sig(S, gen(p,scl(S,r3)) ; pqPk(pqSk(S,r4)) ; N ; rd(S,r1))), 
 -(cke ; PK1 ; CP), 
 -(cf ; enc(ms(pms(gen(PK1,scl(S,r3)), decap(CP, pqSk(S,r4))), 
             N, rd(S,r1), PK1, CP), 
         (ch ; N) ++ 
         (sh ; rd(S,r1) ; sess(S,r2)) ++ 
         (sc ; cert(S)) ++ 
         (ske ; gen(p,scl(S,r3)) ; pqPk(pqSk(S,r4)) ; 
             sig(S, gen(p,scl(S,r3)) ; pqPk(pqSk(S,r4)) ; N ; rd(S,r1))) ++ 
         (cke ; PK1 ; CP)) 
  ), 
nil ]    
 
CP 
is a variable of the sort
 
Cipher 
. Note that in both strands, we omit the ServerFinished message because they are too long to show all. The complete specification is publicly available at https://doi.org/10.5281/zenodo.7919153.

Intruder capabilities

 
X    
and
 
Y 
be variables of the sort
 
Msg 
, we first specify the intruder’s capabilities in concatenating and de-concatenating messages by the following three strands:
 
 
:: nil :: [ nil | -(X), -(Y), +(X ; Y), nil ] & 
:: nil :: [ nil | -(X ; Y), +(X), nil ] & 
:: nil :: [ nil | -(X ; Y), +(Y), nil ] &    
 
 
:: r :: [ nil | +(rd(i,r)), nil ] & 
:: r :: [ nil | +(scl(i,r)), nil ] &    
 
i 
is a constant denoting the intruder.
 
PK2    
, secret key
 
SK 
, and encapsulation
 
CP 
, then the intruder can derive some appropriate encapsulations and keys as follows:
 
 
:: nil :: [ nil | -(PK2), -(SK), +(encapCipher(PK2,SK)), nil ] & 
:: nil :: [ nil | -(PK2), -(SK), +(encapKey(PK2,SK)), nil ] & 
:: nil :: [ nil | -(CP), -(SK), +(decap(CP,SK)), nil ] &    
 
 
:: nil :: [ nil | -(gen(p,S)), -(gen(p,S2)), +(gen(p,S * S2)), nil ]    
 
S 
and
 
S2 
are variables of
 
Scalar 
.

Checking the specification

 
c    
and
 
s 
be two constants of the sort
 
Name 
, denoting arbitrary principals (implicitly stand for a client and a server). The state pattern is defined as a Maude-NPA
 
ATTACK-STATE 
as follows:
 
 
eq ATTACK-STATE(10) = 
:: r1,r2,r3 :: 
[ nil, 
 +(ch ; rd(c,r1)), 
 -(sh ; N ; SS), 
 -(sc ; cert(s)), 
 -(ske ; PK1 ; PK2 ; sig(s, PK1 ; PK2 ; rd(c,r1) ; N)), 
 +(cke ; gen(p, scl(c,r2)) ; encapCipher(PK2, pqSk(c,r3))), 
 +(cf ; enc(ms(pms(gen(PK1, scl(c,r2)), encapKey(PK2, pqSk(c,r3))), 
     rd(c,r1), N, gen(p, scl(c,r2)), encapCipher(PK2, pqSk(c,r3))), 
    (ch ; rd(c,r1)) ++ 
    (sh ; N ; SS) ++ 
    (sc ; cert(s)) ++ 
    (ske ; PK1 ; PK2 ; sig(s, PK1 ; PK2 ; rd(c,r1) ; N)) ++ 
    (cke ; gen(p, scl(c,r2)) ; encapCipher(PK2, pqSk(c,r3))))), 
 -(sf ; ... ) 
 | nil ] 
|| empty 
|| nil    || nil    || nil 
[nonexec] .    
 
10    
in
 
ATTACK-STATE(10) 
denotes the attack pattern number in order to distinguish from other attacks and
 
... 
denotes that some terms of the sort
 
Msg 
, which are components of the ServerFinished message, are omitted for the sake of simplicity. The attack pattern consists of five sections separated by the symbol ——. The second section is the intruder knowledge, which is empty in this case. The last three sections are set to
 
nil 
denoting empty because they are irrelevant in this case. The first section is the set of strands expected to appear in the attack, which says that client
 
c 
has completed the protocol handshake with server
 
s 
. Maude-NPA returns a solution for the attack pattern, thereby confirming that it is possible to successfully complete the protocol handshake between two principals.

Analysis experiments

Secrecy property of ECDH shared secret key

 
ATTACK-STATE(0)    
, that is identical to the
 
ATTACK-STATE(10) 
shown above except for the intruder knowledge section, which is changed from
 
empty 
to the following:
 
 
  gen(PK1, scl(c,r2)) inI, empty    
 
PK1    
denotes the ECDH public key that client
 
c 
receives from server
 
s 
, while
 
scl(c,r2) 
denotes the ECDH secret key of the client. The symbol
 
_inI 
indicates what messages the intruder knows, while the symbol
 
_!inI 
indicates what messages the intruder does not yet know (but will know in the future). The attack pattern says that when a client has completed the handshake with a server in which the server sent their ECDH public key, i.e.,
 
PK1 
, to the client and the client sent their ECDH public key, i.e.,
 
gen(p, scl(c,r2)) 
to the server, then the intruder can learn the corresponding ECDH shared key denoted by
 
gen(PK1, scl(s,r2)) 
.
 
 
1  +(ch ; rd(c,#3:Fresh)), 
2  -(ch ; rd(c,#3:Fresh)), 
3  +(sh ; rd(s,#4:Fresh) ; sess(s,#6:Fresh)), 
4  +(sc ; cert(s)), 
5  +(ske ; gen(p, scl(s,#0:Fresh)) ; pqPk(pqSk(s,#2:Fresh)) ; 
sig(s, gen(p, scl(s,#0:Fresh)) ; pqPk(pqSk(s,#2:Fresh)) ; 
rd(c,#3:Fresh) ; rd(s,#4:Fresh))), 
6  -(ske ; ...), 
7  +(gen(p, scl(s,#0:Fresh)) ; pqPk(pqSk(s,#2:Fresh)) ; 
sig(s, gen(p, scl(s,#0:Fresh)) ; pqPk(pqSk(s,#2:Fresh)) ; 
rd(c,#3:Fresh) ; rd(s,#4:Fresh))), 
8  -(sh ; rd(s,#4:Fresh) ; sess(s,#6:Fresh)), 
9  -(sc ; cert(s)), 
10 -(ske ; ...), 
11 +(cke ; gen(p, scl(c,#1:Fresh)) ; 
encapCipher(pqPk(pqSk(s,#2:Fresh)), pqSk(c,#5:Fresh))), 
12 -(cke ; ...), 
13 +(gen(p, scl(c,#1:Fresh)) ; 
encapCipher(pqPk(pqSk(s,#2:Fresh)),pqSk(c,#5:Fresh))), 
14 -(gen(p, scl(c,#1:Fresh)) ; 
encapCipher(pqPk(pqSk(s,#2:Fresh)),pqSk(c,#5:Fresh))), 
15 +(gen(p, scl(c,#1:Fresh))), 
16 -(gen(p, scl(s,#0:Fresh)) ; 
pqPk(pqSk(s,#2:Fresh)) ; sig(s, gen(p, scl(s,#0:Fresh)) ; 
pqPk(pqSk(s,#2:Fresh)) ; rd(c,#3:Fresh) ; rd(s,#4:Fresh))), 
17 +(gen(p, scl(s,#0:Fresh))), 
18 -(gen(p, scl(s,#0:Fresh))), 
19 -(gen(p, scl(c,#1:Fresh))), 
20 +(gen(p, scl(s,#0:Fresh) * scl(c,#1:Fresh))), 
21 +(cf ; ...), 
22 -(cke ; gen(p, scl(c,#1:Fresh)) ; 
encapCipher(pqPk(pqSk(s,#2:Fresh)), pqSk(c,#5:Fresh))), 
23 -(cf ; ...), 
24 +(sf ; ...), 
25 -(sf ; ...)    
 
c 
starts sending a ClientHello message to server
  
s 
(at line 1), where
 
#3:Fresh 
denote a unique fresh. Server
 
s 
receives that message (at line 2), and then sends consecutively to
 
c 
a ServerHello message (at line 3), a Certificate message (at line 4), and a ServerKeyExchange message (at line 5). The intruder grasps the ServerKeyExchange message, and by applying the de-concatenation rules twice, they learn the ECDH public key (
 
gen(p, scl(s,#0:Fresh)) 
) sent in that message (at lines 6–7 and 16–17). We use
 
... 
to omit some components of a message, which is too long to show fully. When
 
c 
receives the three messages from
 
s 
(at lines 8–10),
  
c 
sends to
 
s 
a ClientKeyExchange message (at line 11). The intruder again grasps that message, and by applying the de-concatenation rules twice, they learn the ECDH public key (
 
gen(p, scl(s,#1:Fresh)) 
) sent in that message (at lines 12–15). From the two ECDH public keys learned (at lines 18–19), by applying the rule
 
 
:: nil :: [ nil | -(gen(p,S)), -(gen(p,S2)), +(gen(p,S * S2)), nil ]    
 
c 
and
 
s 
(at line 20).
 
c 
then sends a ClientFinished message to
 
s 
(at line 21). Upon receiving the ClientKeyExchange and ClientFinished messages (at lines 22–23),
 
s 
sends back to
 
c 
a ServerFinished message (at line 24). The last line 25 denotes the reception of that ServerFinished message on the client side. The handshake is now completed, in which the ECDH shared secret is learned by the intruder.

Secrecy property of PQ KEM shared secret key

 
ATTACK-STATE(1)    
is defined as the counterpart of
 
ATTACK-STATE(0) 
, checking whether the intruder can learn the PQ KEM shared secret key established between the client and the server. If it is possible, then they can indeed derive the pre-master secret and the master secret from both PQ KEM and ECDH shared secrets learned; otherwise, the secrecy of the master secret is guaranteed. Therefore, the secrecy property of handshake keys is checked through this attack pattern.
 
ATTACK-STATE(1) 
is identical to
 
ATTACK-STATE(10) 
except for the intruder knowledge section, which now becomes as follows:
 
 
  encapKey(PK2, pqSk(c,r3)) inI, empty    
 
ATTACK-STATE(1)    
says that when a client has completed the protocol handshake with a server in which the server sent the PQ KEM public key denoted by
 
PK2 
to the client and the client sent the PQ KEM ciphertext (or encapsulation) denoted by
 
encapCipher(PK2, pqSk(c,r3)) 
to the server, then the intruder cannot learn the PQ KEM shared key denoted by
 
encapKey(PK2, pqSk(c,r3)) 
.

Authentication property

 
ATTACK-STATE(2)    
:
 
 
eq ATTACK-STATE(2) = 
:: r1,r2,r3 :: 
[ nil, 
 +(ch ; rd(c,r1)), 
 -(sh ; N ; SS), 
 -(sc ; cert(s)), 
 -(ske ; PK1 ; PK2 ; sig(s, PK1 ; PK2 ; rd(c,r1) ; N)), 
 +(cke ; gen(p,pt(c,r2)) ; encapCipher(PK2, pqSk(c,r3))), 
 +(cf ; enc(ms(pms(gen(PK1, pt(c,r2)), encapKey(PK2, pqSk(c,r3))), 
     rd(c,r1),N,gen(p,pt(c,r2)),encapCipher(PK2, pqSk(c,r3))), 
    (ch ; rd(c,r1)) ++ 
    (sh ; N ; SS) ++ 
    (sc ; cert(s)) ++ 
    (ske ; PK1 ; PK2 ; sig(s, PK1 ; PK2 ; rd(c,r1) ; N)) ++ 
    (cke ; gen(p,pt(c,r2)) ; encapCipher(PK2, pqSk(c,r3))))), 
 -(sf ; ... ) 
 | nil ] 
|| empty 
|| nil 
|| nil 
|| never( 
  :: r’,r1’,r2’,r3’ :: 
  [ nil | 
    -(ch ; rd(c,r1)), 
    +(sh ; N ; SS), 
    +(sc ; cert(s)), 
    +(ske ; PK1 ; PK2 ; sig(s, PK1 ; PK2 ; rd(c,r1) ; N)), 
    -(cke ; gen(p,pt(c,r2)) ; encapCipher(PK2, pqSk(c,r3))), 
    -(cf ; enc(ms(pms(gen(PK1,pt(c,r2)), encapKey(PK2, pqSk(c,r3))), 
       rd(c,r1),N,gen(p,pt(c,r2)),encapCipher(PK2, pqSk(c,r3))), 
      (ch ; rd(c,r1)) ++ 
      (sh ; N ; SS) ++ 
      (sc ; cert(s)) ++ 
      (ske ; PK1 ; PK2 ; sig(s, PK1 ; PK2 ; rd(c,r1) ; N)) ++ 
      (cke ; gen(p,pt(c,r2)) ; encapCipher(PK2, pqSk(c,r3))))), 
    +(sf ; ... ), 
    nil ] 
  & STR:StrandSet 
  || IK:IntruderKnowledge) 
[nonexec] .    
 
...    
denotes the omission of some terms of sort
 
Msg 
, which are components of the ServerFinished message. The intruder knowledge section now becomes
 
empty 
, meaning that there is no constraint about the intruder knowledge, while the last section now is a
 
never 
pattern. This attack pattern defines a state in which client
 
c 
has completed the handshake, apparently with server
 
s 
, by sending a ClientFinished message to
 
s 
and
 
c 
has received back another valid ServerFinished message, but
  
s 
has actually not executed such a server instance with
 
c 
(denoted by the
 
never 
pattern in the last section of the attack). Maude-NPA and Par-Maude-NPA did not find any counterexample up to depths 17 and 18, respectively. Next, we report the detailed experimental results of the three analyses in the next subsection.

Experimental results

Conclusion

Additional Information and Declarations

Competing Interests

The authors declare that there are no competing interests.

Author Contributions

Duong Dinh Tran conceived and designed the experiments, performed the experiments, analyzed the data, performed the computation work, prepared figures and/or tables, authored or reviewed drafts of the article, and approved the final draft.

Canh Minh Do conceived and designed the experiments, performed the experiments, analyzed the data, performed the computation work, prepared figures and/or tables, authored or reviewed drafts of the article, and approved the final draft.

Santiago Escobar conceived and designed the experiments, analyzed the data, authored or reviewed drafts of the article, and approved the final draft.

Kazuhiro Ogata conceived and designed the experiments, analyzed the data, authored or reviewed drafts of the article, and approved the final draft.

Data Deposition

The following information was supplied regarding data availability:

The complete protocol specification and the attack patterns are available at Zenodo:

duongtd23. (2023). Hybrid Post-Quantum TLS formal analysis in Maude-NPA (v1.1). Zenodo. https://doi.org/10.5281/zenodo.7919153.

Funding

This work was supported by the JST SICORP (No. JPMJSC20C2), the European Regional Development Fund, the Generalitat Valenciana, and the European Union NextGenerationEU. There was no additional external funding received for this study. The funders had no role in study design, data collection and analysis, decision to publish, or preparation of the manuscript.

1 Citation 914 Views 30 Downloads

Your institution may have Open Access funds available for qualifying authors. See if you qualify

Publish for free

Comment on Articles or Preprints and we'll waive your author fee
Learn more

Five new journals in Chemistry

Free to publish • Peer-reviewed • From PeerJ
Find out more