Split keys for station-to-station (STS) protocols

Formal verification tools for security protocols

The application of formal methods for the analysis of cryptographic protocol means using automated formal analysis tools to determine whether an attacker can prevent the protocol from achieving its security objectives ^[14]. Formal methods have proven valuable when developing critical systems, such as protocols, where safety or security is important. In fact, various protocols were believed to be secure for years, and then formal verification showed later that it was not the case. One classic example is the Needham-Shroeder protocol ^[15], which was developed in 1978 and later proven to be insecure by Lowe^[16] in 1996.

ProVerif ^[13] and Tamarin-Prover ^[17] are state-of-the-art tools used for formally verifying and analyzing security protocols. The Dolev-Yao adversary model is utilized in both tools.

ProVerif uses applied pi-calculus as a formal language, translates the protocol into a set of Horn clauses, and considers an unbounded number of sessions and an unbounded message space for the protocol analysis. The tool can detect attacks. If a protocol property cannot be proven, ProVerif attempts to construct an execution trace that contradicts that property.

Tamarin-Prover offers comprehensive support for modeling and analyzing security protocols. The specification of protocols and adversaries employs an expressive language based on multiset rewriting rules. These rules define a labeled transition system, where the state includes a symbolic representation of the knowledge of the adversary, the messages on the network, freshly generated values, and the state of the protocol. The adversary and protocol interaction involves updating network messages and generating new ones.

Secret splitting for authentication

The internet standard IETF RFC 5026 ^[18] introduces a split scenario in a model where the entity that provides service is different from the entity that authenticates and authorizes the user, e.g., the network access provider differs from the mobility service authorizer.

Several authentication schemes exist, e.g., biometric verification, text passwords, public key infrastructure, and symmetric-key-based authentication techniques. Multi-tier authentication schemes are more secure than single sign-on, considering layered defense; however, multi-tier authentication schemes increase the complexity of user experience ^[19]. To reduce the computational overhead in a system with multiple sources of trust, Choi et al. present a new multi-source authentication scheme called Split-Join One-Way Key Chain (SOKC) that stores the parts of the keys in the source nodes ^[20].

Shah et al. ^[21] and Wang et al. ^[22] present a multi-factor authentication with the secret-splitting concept of biometrics, including exclusive-or operations, DH key exchange algorithms, and encryption algorithms. The proposed approaches split the biometric data into two, encrypt both parts, and store one on a smart card and another on a server. The proposed solutions are secure against authentication factor attacks, network attacks, and interior attacks from the card-issuing organization.

Choi et al. ^[23] suggest a solution for a certificate-based authentication system using a password and a secondary source, i.e., an honest-but-curious server or another mobile device. In this setup, the user has a secret key to authenticate himself to a controller (a website or an application). To prevent the danger of compromising the device of the user, some secret values are utilized, each of which is used to encrypt their secret key. The secret values are stored in the secondary sources. When the user wants to sign into the controller, he retrieves the secret value from the secondary sources to decrypt the secret key. Therefore, the user can authenticate himself to the controller only with the contribution of secondary sources.

Station-to-station protocol

The STS protocol was proposed by Diffie et al. ^[4] in 1992 to obtain mutual entity authentication and mutual explicit key authentication ^[24]. STS is an AKA based on the DH key exchange protocol and authenticated signatures. Diffie et al. provide variants of the STS protocol that have explicit key confirmation by using a symmetric-key encryption scheme and a message authentication code (MAC) ^[4]. Those variants are called STS-ENC and STS-MAC, respectively, in Blake-Wilson et al. ^[5].

Blake-Wilson et al. show that STS-ENC and STS-MAC are vulnerable to UKS attacks ^[5]. To prevent these attacks, the authors propose to apply the Key Derivation Function (KDF) on the shared DH key. This variant was later named as STS-KDF by Jackson et al. ^[6], who also provide formal verification of the variants of the STS protocol by using the Tamarin Prover. They show that STS-KDF is the only variant that satisfies all the following security requirements: key secrecy, identity agreement, and strong session agreement (injective agreement) while using signatures that are secure under the Existential Unforgeability under an Adaptive Chosen Message Attack (EUF-CMA) model.

Next, we describe the STS-KDF protocol. Let Alice and Bob be two parties that use the protocol to agree on a shared key. Each party has a public and a secret key for signature verification and signing, respectively: $$ (pk_a, sk_a) $$ is the public and secret key pair of Alice, and $$ (pk_b, sk_b) $$ is the public and secret key pair of Bob. The parties authenticate the public key of each other through the certificates, where $$ cert_a $$ includes $$ pk_a $$, the identity $$ id_a $$ of Alice, and possibly other information; $$ cert_b $$ includes $$ pk_b $$, the identity $$ id_b $$ of Bob, and possibly other information. The certificates are signed by the Certificate Authority (CA). The steps of an STS-KDF protocol run are shown in the listing Protocol 1 and in Figure 1.

Figure 1. STS-KDF protocol. STS-KDF: station-to-station with key derivation function.

Authenticated key exchange

Authenticated Key Exchange (AKE) aims to provide two communicating parties some assurance that they know the identities of each other and share a secret key only known to them ^[4]. The shared secret key can be used further to provide privacy, data integrity, or both.

Krawczyk ^[12] proposes several authenticated DH key exchange protocols under the name SIGMA. These protocols adapt the sign-and-MAC approach using DH key exchange and have been used in Internet Key Exchange (IKE) protocols ^[25]. The author begins by studying STS protocols and builds the SIGMA protocols upon them. The basic form of SIGMA is similar to STS-KDF. Still, the MAC computation differs from the STS-KDF in that only the certificate or identifier is used as an input instead of the signature, while the MAC key is derived from the DH key. Another variation of SIGMA includes encryption of all the messages except for the public key to provide identity protection.

Krzywiecki et al. ^[26] designed an AKE protocol for wearable devices by improving the SIGMA protocol of Krawczyk ^[12]. Krzywiecki et al. ^[26] aim to prevent impersonation attacks by splitting the signing key into two signing modules and renewing the partial keys. They claim that the impersonation attack would be successful only if the attacker captures both partial keys.

Key encapsulation mechanism

A KEM is a public encryption scheme that produces a shared key that can be used for symmetric encryption. The notion of KEMs was introduced by Cramer and Shoup ^[7] to build an efficient hybrid encryption scheme with an unrestricted message space.

KEM: The KEM consists of three algorithms ^[7,8]:

1. Key Generation is a probabilistic, polynomial-time key generation algorithm that takes a security parameter $$ k $$ as input and generates a pair of public and secret keys $$ (PK, SK) $$:

$$ (PK, SK) \longleftarrow KEM\_KeyGen(1^k). $$

2. Key Encapsulation is a probabilistic, polynomial-time encryption algorithm that takes a public key $$ PK $$ as input and generates a cipher text $$ C $$ and a KEM key $$ K $$:

$$ (C, K) \longleftarrow KEM\_Encaps(PK) $$.

3. Key Decapsulation is a deterministic, polynomial-time decryption algorithm that takes a ciphertext $$ C $$ and the secret key $$ SK $$ as input and recovers the KEM key $$ K $$:

$$ K \longleftarrow KEM\_Decaps(C, SK) $$.

The KEM key $$ K $$, the output of the functions $$ KEM\_Encaps $$ and $$ KEM\_Decaps $$, is shared between communicating parties.

Split KEM: Next, we consider KEM in a secret-splitting scenario. Ebina et al. introduced a distributed KEM decapsulation, where the secret key $$ SK $$ is split into $$ n $$ parts, $$ SK_1 $$, $$ SK_2 $$, $$\dots, SK_n $$, and the encapsulated key $$ K $$ is reconstructed from $$ t $$ out of $$ n $$ potential partial decapsulation results, $$ K_1, K_2, \cdots, K_n $$^[11]. The Split KEM below is an adaptation of their construction for our scenario, where $$ t=n=2 $$. For the purposes of formal analysis, we have combined some of the seven algorithms in Section 2.3 of Ebina et al. ^[11] to form the following set of five.

1. Split Key Generation is a probabilistic, polynomial-time key generation algorithm that takes a security parameter $$ k $$ as input and outputs public encapsulation key PK, two decapsulation key shares $$ SK_1, SK_2 $$, and a verification key $$ vk $$:

$$ (PK, (SK_1, SK_2), vk) $$$$ \longleftarrow SplitKEM\_KeyGen(1^k) $$.

2. Split Key Encapsulation is a probabilistic, polynomial-time encryption algorithm that takes a public key $$ PK $$ as input and outputs a ciphertext $$ C $$ and a session key $$ K $$:

$$ (C, K) \longleftarrow SplitKEM\_Encaps(PK) $$.

3. Split Key Decapsulation is a deterministic, polynomial-time decapsulation algorithm that takes decapsulation key shares $$ SK_1 $$ and $$ SK_2 $$ and the ciphertext C as input and outputs session key shares $$ K_1 $$ and $$ K_2 $$, respectively:

$$ K_1 \longleftarrow SplitKEM\_Decaps(C, SK_1) $$.

$$ K_2 \longleftarrow SplitKEM\_Decaps(C, SK_2) $$.

4. Split Key Reconstruction is a deterministic, polynomial-time key generation algorithm that takes the two session key shares $$ K_1, K_2 $$ as input and outputs the session key $$ K $$:

$$ K \longleftarrow SplitKEM\_Recons(K_1, K_2) $$.

5. Split Key Share Verification is a deterministic, polynomial-time algorithm that takes $$ PK $$, $$ C $$, $$ vk $$, and a key share $$ K_i $$ as input and outputs 0 or 1:

$$ 0/1 \longleftarrow SplitKEM\_Verif(PK, C, K_i, vk) $$ for $$ i=1, 2 $$.

We say that $$ K_i $$ is a valid share if $$ SplitKEM\_Verif(PK, C, K_i, vk)=1 $$.

The outputs, $$ K_1 $$ and $$ K_2 $$, of the function $$ SplitKEM\_Decaps $$, are reconstructed using the function $$ SplitKEM\_Recons $$ to obtain the shared key $$ K $$, which is identical to the second output of the function $$ SplitKEM\_Encaps $$.

Authenticated encryption

The communication between two parties over a network requires two main security goals: privacy and authentication. Achieving both privacy and authentication at the same time is called authenticated encryption (AE). The three basic ways to achieve AE are (1) MAC-then-Encrypt; (2) Encrypt-then-MAC; and (3) Encrypt-and-MAC ^[27].

Since some application settings require associated data, which should be authenticated without encryption, in addition to the authenticated and encrypted data, the notion of AE with associated data (AEAD) is introduced. The AEAD was first formalized by Rogaway et al. in 2002 using the generic composition of a nonce-based, privacy-only encryption scheme and a pseudorandom function ^[28].

The National Institute of Standards and Technology (NIST) initiated a standardization process for lightweight cryptography to select one or more schemes for AEAD in 2015 and announced the decision in 2023. The permutation-based AEAD and a hashing scheme named ASCON are chosen to be standardized ^[29].

Split-key scenarios

We model the scenario where the secret keys of the users could be split with, e.g., an assistant device. In our model, the users are called Alice and Bob. Alice splits her key into two pieces and distributes each piece in two devices, Alice1 and Alice2, where Alice2 is the assistant device. Alice requires the full cooperation of both Alice1 and Alice2 to use her key, e.g., for digital signature. Similarly, Bob splits his key between Bob1 and Bob2. The following four cases of the split key scenario are illustrated in Figure 2.

Figure 2. Cases of the system model: (ⅰ) no split key; (ⅱ) Alice's keys are split between Alice1-Alice2; (ⅲ) Bob's keys are split between Bob1-Bob2; (ⅳ) both Alice's and Bob's keys are split between Alice1-Alice2 and Bob1-Bob2, respectively.

(ⅰ) No Split Key (Alice-Bob);

(ⅱ) Split Key for Alice (Alice2-Alice1-Bob);

(ⅲ) Split Key for Bob (Alice-Bob1-Bob2);

(ⅳ) Split Key for both Alice and Bob (Alice2-Alice1-Bob1-Bob2).

Note that our secret splitting can be seen as a special case of threshold secret sharing where the threshold $$ t $$ equals the number of shares $$ n $$ and $$ n=2 $$. However, in our setting, the secret is not reconstructed from the shares, which is in contrast with the traditional notion of secret sharing introduced in ^[30]. See also ^[31] for different types of secret sharing.

Adversary model

As described in Section 3.1, the system model has two parties, say, Alice and Bob, that communicate over an unsecured channel. When the split key scenarios are considered, the number of parties in the model can be three or four.

We assume that the outsiders are Dolev-Yao adversaries; the attacker (a) can see any message that is sent to the network, (b) is a legitimate user of the network and can start a conversation with other users, and (c) has an opportunity to be a receiver of any initiator of the protocol ^[32]. In addition to this definition, any message that is sent through the network by legitimate users is assumed to be either created or passed on by the attacker ^[14]. In brief, the attacker, namely a Dolev-Yao adversary, "can compose messages, replay them, or decipher them if she knows the right keys, but cannot otherwise crack encrypted messages" ^[33].

We assume perfect cryptographic primitives, i.e., attackers can decrypt secrets only if they possess the corresponding keys, and hash functions are assumed to be one-way and collision-resistant. Moreover, we consider a more powerful adversary following the extended Canetti–Krawczyk (eCK) model ^[34]. In particular, the adversary is allowed to compromise some parties, e.g., by physical access or malware in a device ^[14]. Furthermore, we consider the possibility of the key reveals.

Security properties

In the following, we give an overview of the main security properties provided by our proposed AKA protocols. For simplicity, we state the security properties in the case of an AKA protocol between two parties, say A and B.

Secrecy: One of the main goals of an AKA protocol is to agree on a cryptographic session key between the participating parties. The protocol is said to achieve session key secrecy if the shared key between A and B at the end of the protocol is not revealed to any malicious third party.

Mutual Authentication: Mutual authentication in an AKA protocol between two parties ensures that both parties are who they claim to be. In other words, mutual authentication is achieved if both sides correctly verify each other's identity.

Forward Secrecy: An AKA protocol satisfying forward secrecy ensures that the compromise of a long-term private key does not compromise past session keys resulting from past AKA executions.

Resistance to Unknown Key Share (UKS) attack: An AKA protocol, say between two parties A and B, is said to be vulnerable to a UKS attack if, by the end of the protocol, A believes that she shares the session key with B, which is the case, while B ends up believing that he shares the key with a party (e.g., the attacker) that is different from A.

Resistance to Key Compromise Impersonation (KCI) attack: A key compromise impersonation (KCI) attack against an AKA protocol is successful if the attacker manages to impersonate a party by compromising a private key.

Identity Confidentiality: An AKA protocol is said to provide identity confidentiality if the protocol protects the parties' privacy, especially their identities.

New variants of station-to-station protocols

We will now describe two protocols for the "no split-key" setting, depicted as the case (i) in Figure 2: the Privacy-Enhanced STS-KDF-CB protocol and the Privacy-Enhanced STS-KDF-CB protocol with KEM that uses KEM instead of Diffie–Hellman key exchange and signature.

Next, we present Privacy-Enhanced STS-KDF-CB. In this protocol, the DH Key Exchange and the signature scheme are used as in the generic STS-KDF. Second, we adopt the KEM to the STS-KDF-CB protocol to provide flexibility in implementing different cryptosystems.

Privacy-enhanced STS-KDF-CB protocol with KEM

Next, we present the Privacy-Enhanced STS-KDF-CB Protocol with KEM, where we replace both the DH key exchange and the signature scheme with KEM. The certified public keys of the parties are used for the KEM instead of the signature scheme.

In this adaptation, we assume that Alice already knows who she is communicating with; therefore, she has the certificate of Bob when she starts the protocol. Only Alice needs to encrypt her certificate and send it to Bob to prove herself.

Protocol 3: Privacy-Enhanced STS-KDF-CB with KEM
Setup:$$ Alice $$ and $$ Bob $$ apply $$ KEM\_KeyGen() $$ to generate their public-secret key pairs, $$ pk_a\text{-}sk_a $$ and $$ pk_b\text{-}sk_b $$, respectively. $$ Alice $$ and $$ Bob $$ have certificates for their public keys, $$ cert_a $$ and $$ cert_b $$.
The Protocol: (cf. Figure 5.)
1. (a) Alice generates the key pair $$ (PK_a, SK_a) $$ with the $$ KEM\_KeyGen() $$ function. Note that the newly generated $$ PK_a $$ and $$ SK_a $$ are not the same as certified $$ pk_a $$ and $$ sk_a $$.
(b) Alice knows and has verified the certificate of Bob before starting the protocol, so she knows his public key $$ pk_b $$. By using this public key, Alice applies the encapsulation function and gets a ciphertext and a session key: $$ (C_0, K_0)=KEM\_Encaps(pk_b) $$.
(c) Alice then encrypts her certificate by using the session key derived above: $$ enc=ENC_{K_0}(cert_a) $$.
2. Alice sends $$ PK_a $$, $$ C_0 $$, and $$ enc $$ to Bob.
3. (a) Bob applies the decapsulation function on the ciphertext $$ C_0 $$ and his secret key $$ sk_b $$: $$ K_0=KEM\_Decaps(C_0, sk_b) $$.
(b) Bob decrypts $$ enc $$ to get the certificate of Alice: $$ cert_a=DEC_{K_0}(enc) $$. Bob also verifies that the certificate of Alice is not the same as his certificate, i.e., $$ cert_a \neq cert_b $$.
(c) Bob applies the encapsulation function on the public key $$ PK_a $$ to get the session key and the ciphertext: $$ (C_1, K_1)=KEM\_Encaps(PK_a) $$.
(d) Bob also applies the encapsulation function on the certified public key $$ pk_a $$ to get another session key and the ciphertext: $$ (C_2, K_2)=KEM\_Encaps(pk_a) $$.
(e) Bob then derives the shared session key from the session keys: $$ K=KDF(K_0, K_1, K_2, cert_a, cert_b) $$.
(f) Bob computes the MAC of the ciphertexts and the certificates using the derived key $$ K $$: $$ mac_1=MAC_{K}(C_0, C_1, C_2, cert_b, cert_a) $$.
4. Bob sends the ciphertexts $$ C_1 $$, $$ C_2 $$, and $$ mac_1 $$ to Alice.
5. (a) Alice applies the decapsulation function on the ciphertext $$ C_1 $$ and her secret key $$ SK_a $$ to get the session key: $$ K_1=KEM\_Decaps(C_1, SK_a) $$.
(b) Alice then applies the decapsulation function on the ciphertext $$ C_2 $$ and her secret key $$ sk_a $$ to get the other session key: $$ K_2=KEM\_Decaps(C_2, sk_a) $$.
(c) Alice then derives the shared session key: $$ K=KDF(K_0, K_1, K_2, cert_a, cert_b) $$.
(d) Alice verifies the $$ mac_1 $$.
(e) Alice computes the MAC of the ciphertexts and the certificates using the shared session key $$ K $$: $$ mac_2=MAC_{K}(C_0, C_1, C_2, cert_a, cert_b) $$.
6. Alice sends $$ mac_2 $$ to Bob.
7. Bob verifies the $$ mac_2 $$.

Please note that replacing the DH key exchange in STS-KDF with a KEM can be done as follows. Using the same notations as in Figure 1, a KEM version of STS-KDF is achieved by minor changes at Alice's and Bob's sides. On Alice's side, it is enough to replace generating a random $$ x $$ by generating a pair of KEM public-secret keys $$ (PK, SK) $$, and then Alice sends $$ PK $$ instead of $$ g^x $$. At Bob's side, generating a random $$ y $$ is replaced by encapsulation using the received $$ PK $$, and finally, Bob sends the ciphertext resulting from encapsulation instead of sending $$ g^y $$. On both sides, the DH key is replaced by the session key produced by the KEM. Such a KEM variant of STS-KDF, however, would inherit the security properties of the original protocol. In particular, it would be vulnerable to the attack described in Section 4.

Similar modifications can be done for the STS-KDF-CB protocol in Figure 4, with the additional change of using the KEM key instead of the DH key in Step 8. This variant would protect against the reflection attack of Section 4.

Figure 4. Privacy-Enhanced STS-KDF Certificate-Binding (STS-KDF-CB) protocol. STS-KDF: station-to-station with key derivation function.

Figure 5. Privacy-Enhanced STS-KDF-CB protocol with KEM.

Protocol 4: Split-Key Privacy-Enhanced STS-KDF-CB
Setup:
ⅰ. Alice and Bob choose a safely large prime $$ p $$ and a generator $$ g\:(mod\;p) $$, where $$ p $$ and $$ g $$ are public.
ⅱ. Alice1 and Alice2 generate a public key $$ pk_a $$ for signature verification and split the secret signing key into the shares, $$ sk_{a_1} $$ and $$ sk_{a_2} $$, respectively. Similarly, Bob1 and Bob2 generate a public key $$ pk_b $$ for signature verification and split the secret signing key into the shares, $$ sk_{b_1} $$ and $$ sk_{b_2} $$, respectively. A threshold signature scheme can be used to construct signatures from these shares [40].
ⅲ. Alice1 gets a certificate for her public verification key $$ pk_a $$, and Bob1 gets a certificate for his public verification key $$ pk_b $$.
The Protocol: (cf. Figure 6.)
1. (a) Alice1 chooses random $$ x\in \mathbb{Z}_p $$.
(b) Alice2 computes her public DH key: $$ g^x $$.
2. Alice1 sends $$ g^x $$ to Bob1.
3. (a) Bob1 chooses random $$ y\in \mathbb{Z}_p $$.
(b) Bob1 computes his public DH key: $$ g^y $$.
(c) Bob1 computes the shared DH key: $$ K_{DH}=(g^x)^y=g^{xy} $$.
4. Bob1 sends the public DH keys, $$ (g^y, g^x) $$ to Bob2.
5. Bob2 signs the DH keys with his secret key $$ sk_{b_2} $$: $$ \sigma_{b_2}=Sig_{sk_{b_2}}(g^y, g^x) $$.
6. Bob2 sends the signature $$ \sigma_{b_2} $$ to Bob1.
7. (a) Bob1 also signs the DH keys with his secret key $$ sk_{b_1} $$ with the contribution of Bob2 to get the signature to send to Alice: $$ \sigma_b=Sig_{sk_{b_1}}(\sigma_{b_2}, g^y, g^x) $$.
(b) Bob applies AEAD on his signature and certificate: $$ enc_1=AEAD_{K_{DH}}(\sigma_b, cert_b) $$.
8. Bob1 sends $$ g^y $$ and $$ enc_1 $$ to Alice1.
9. (a) Alice1 computes the shared DH key: $$ K_{DH}=(g^y)^x=g^{xy} $$.
(b) Alice1 then decrypts the $$ enc_1 $$ by using the derived key to get the signature and the certificate of Bob: $$ (\sigma_b, cert_b)=DEC_{K_{DH}}(enc_1) $$.
(c) Alice1 verifies the certificate, i.e., $$ cert_b \neq cert_a $$ and the signature $$ \sigma_b $$.
10. Alice1 sends the public DH keys, $$ (g^x, g^y) $$ to Alice2.
11. Alice2 signs the DH keys with her secret key $$ sk_{a_2} $$: $$ \sigma_{a_2}=Sig_{sk_{a_2}}(g^x, g^y) $$.
12. Alice2 sends the signature $$ \sigma_{a_2} $$ to Alice1.
13. (a)Alice1 also signs the DH keys with her secret key $$ sk_{a_1} $$ with the contribution of Alice2 to get the signature to send to Bob: $$ \sigma_a=Sig_{sk_{a_1}}(\sigma_{a_2}, g^x, g^y) $$.
(b) Alice1 applies AEAD on her signature and certificate: $$ enc_2=AEAD_{K_{DH}}(\sigma_a, cert_a) $$.
14. Alice1 sends $$ \sigma_a $$, $$ enc_2 $$, and $$ mac_2 $$ to Bob1.
15. (a) Bob decrypts the $$ enc_2 $$ to get the signature and the certificate of Alice: $$ (\sigma_a, cert_a)=DEC_{K_{DH}}(enc_2) $$.
(b) Bob verifies the certificate, i.e., $$ cert_a \neq cert_b $$ and the signature $$ \sigma_a $$.
16. Alice and Bob derive the session key $$ K $$ from the shared DH key and their certificates: $$ K=KDF(K_{DH}, cert_a, cert_b) $$.

Figure 6. Split-Key Privacy-Enhanced STS-KDF-CB protocol.

Split-key settings for station-to-station protocol

In this section, we adopt the privacy-enhanced variants of STS-KDF-CB to the setting in case (ⅳ) of Figure 2, where both of the parties of the protocol have split keys. By splitting the keys, we aim to protect the security of the key if the device is compromised since compromising two or more devices is harder than a single device.

In these split-key protocols, neither Alice nor Bob is aware that the other party has a split key. The protocols for the hybrid cases (ⅱ) or (ⅲ) in Figure 2 can be constructed by combining a split-key protocol from this section with the corresponding protocol from Section 5.1 above.

Split-key privacy-enhanced STS-KDF-CB with KEM

Next, we present how we adopt the split-Key KEM construction (see Section 2.5) to the privacy-enhanced STS-KDF-CB with KEM.

Protocol 5: Split-Key Privacy-Enhanced STS-KDF-CB with KEM
Setup:
ⅰ. Alice1 and Alice2 apply $$ SplitKEM\_KeyGen() $$ to generate a public key $$ pk_a $$, split secret keys, $$ sk_{a_1} $$ and $$ sk_{a_2} $$, respectively, and a verification key $$ vk_a $$. Similarly, Bob1 and Bob2 apply $$ SplitKEM\_KeyGen() $$ to generate a public key $$ pk_b $$ and split secret keys, $$ sk_{b_1} $$ and $$ sk_{b_2} $$, respectively, and a verification key $$ vk_a $$.
ⅱ. Alice1 gets a certificate for her public key $$ pk_a $$, and Bob1 gets a certificate for his public key $$ pk_b $$.
The Protocol: (cf. Figure 7.)
1. (a) Alice1 generates key pair $$ (PK_a, SK_a) $$ with $$ KEM\_KeyGen() $$ function. Note that the newly generated $$ PK_a $$ and $$ SK_a $$ are not the same as certified $$ pk_a $$ and $$ sk_a $$.
(b) Alice1 has the certificate of Bob before starting the protocol, so she knows his public key $$ pk_b $$. By using this public key, Alice1 applies the split encapsulation function and gets a ciphertext and a session key: $$ (C_0, K_0)=SplitKEM\_Encaps(pk_b) $$.
(c) Alice1 then encrypts her certificate by using the session key derived above: $$ enc=ENC_{K_0}(cert_a) $$.
2. Alice1 sends $$ PK_a $$, $$ C_0 $$, and $$ enc $$ to Bob1.
3. Bob1 sends $$ C_0 $$ to Bob2.
4. Bob2 applies the split decapsulation function on the ciphertext $$ C_0 $$ and his share of the secret key $$ sk_{b_2} $$ to get part of the session key: $$ K_0'=SplitKEM\_Decaps(C_0, sk_{b_2}) $$.
5. Bob2 sends the key part $$ K_0' $$ to Bob1.
6. (a) Bob1 first verifies that the key part he received from Bob2 is derived by using the correct secret key: $$ SplitKEM\_Verif(pk_b, C_0, K_0', vk_b)=True/False $$.
(b) Bob1 then applies the split decapsulation function on the ciphertext $$ C_0 $$ and his share of the secret key $$ sk_{b_1} $$: $$ K_0''=SplitKEM\_Decaps(C_0, sk_{b_1}) $$.
(c) Bob1 applies the split reconstruction function on the key parts $$ K_0' $$ and $$ K_0'' $$: $$ K_0=SplitKEM\_Recons(K_0', K_0'') $$.
(d) Bob1 decrypts $$ enc $$ to get the certificate of Alice: $$ cert_a=DEC_{K_0}(enc) $$. Bob also verifies that the certificate of Alice is not the same as his own certificate, i.e., $$ cert_a\neq cert_b $$.
(e) Bob1 applies the encapsulation function on the public key $$ PK_a $$ to get another session key and the ciphertext: $$ (C_1, K_1)=KEM\_Encaps(PK_a) $$.
(f) Bob1 also applies the split encapsulation function on the certified public key $$ pk_a $$ to get one more session key and the ciphertext: $$ (C_2, K_2)=SplitKEM\_Encaps(pk_a) $$.
(g) Bob1 then derives the shared session key from the derived keys above and the certificates: $$ K=KDF(K_0, K_1, K_2, cert_a, cert_b) $$.
(h) Bob1 computes the MAC of the ciphertexts and the certificates using the derived key $$ K $$: $$ mac_1=MAC_{K}(C_0, C_1, C_2, cert_b, cert_a) $$.
7. Bob1 sends the ciphertexts $$ C_1 $$, $$ C_2 $$, and $$ mac_1 $$ to Alice1.
8. Alice1 applies the decapsulation function on the ciphertext $$ C_1 $$ and her secret key $$ SK_a $$ to get the session key: $$ K_1=SplitKEM\_Decaps(C_1, SK_a) $$.
9. Alice1 sends $$ C_2 $$ to Alice2.
10. Alice2 applies the split decapsulation function on the ciphertext $$ C_2 $$ and her share of the secret key $$ sk_{a_2} $$ to get part of the session key: $$ K_2'=SplitKEM\_Decaps(C_2, sk_{a_2}) $$.
11. Alice2 sends the key part $$ K_2' $$ to Alice1.
12. (a) Alice1 first verifies that the key part she received from Alice2 is derived by using the correct secret key: $$ SplitKEM\_Verif(pk_a, C_2, K_2', vk_a)=True/False $$.
(b) Alice1 then applies the split decapsulation function on the ciphertext $$ C_2 $$ and her share of the secret key $$ sk_{a_1} $$: $$ K_2''=SplitKEM\_Decaps(C_2, sk_{a_1}) $$.
(c) Alice1 applies the split reconstruction function on the key parts $$ K_2' $$ and $$ K_2'' $$: $$ K_2=SplitKEM\_Recons(K_2', K_2'') $$.
(d) Alice1 derives the shared session key from the derived keys above and the certificates: $$ K=KDF(K_0, K_1, K_2, cert_a, cert_b) $$.
(e) Alice1 verifies the $$ mac_1 $$.
(f) Alice1 computes the MAC of the ciphertexts and her certificate with the certificate of Bob using the shared session key $$ K $$: $$ mac_2=MAC_{K}(C_0, C_1, C_2, cert_a, cert_b) $$.
13. Alice1 sends $$ mac_2 $$ to Bob1.
14. Bob1 verifies the $$ mac_2 $$.

Figure 7. Split-Key Privacy-Enhanced STS-KDF-CB Protocol with KEM.

Modeling the protocols

The ProVerif model is constructed in three parts: declarations, process macros, and main process.

The cryptographic primitives are formalized using declarations, which are a finite set of types, free names, and constructors (functions) ^[13]. We have used the following primitives, for which examples of constructions are given in the ProVerif manual ^[13]: symmetric encryption, MAC, DH Key Exchange, digital signature, and AEAD. In addition, we have modeled the following primitives, some of which have been used in our earlier work.

Split-Key Digital Signatures: In addition to the digital signatures, we have added a function for reconstructing the split secret keys. We then defined split signing functions for the parties in the protocol who want to collectively create digital signatures:

The equation below defines that the result of the reconstruction of split signatures should be the same as the result of the message signed with the reconstructed key. This equation is important, especially in scenarios where one party splits her key while the other party does not, as described in cases (ⅱ) and (ⅲ) of the split key scenarios in Section 3.1.

Key Encapsulation Mechanism (KEM): The KEM is modeled using the following five functions: key generation, encapsulation, KEM key derivation, ciphertext generation, and decapsulation of the KEM key. It is important to recall that the encapsulation algorithm is a probabilistic algorithm with two outputs, the ciphertext and the KEM key; thus, we model the two outputs with two separate functions: KEMkey and KEMCipher, taking randomized public encryption as input, i.e., output of Encaps function:

The equation below ensures that the key generated during encapsulation ($$\texttt{KEMkey}$$ function) is the same as the key generated by decapsulation ($$\texttt{DecapsKey}$$ function).

Split Key Encapsulation Mechanism (Split KEM): In addition to the functions that are defined for KEM, we added functions for split key generation, key share verification, and reconstruction of the key shares, which are the outputs of split decapsulation:

The reduction below ensures the verification of valid splits. The equation, in the end, ensures that the key generated during encapsulation ($$\texttt{SplitKEMkey}$$ function) is the same as the key generated after reconstructing the key shares that are the outputs of decapsulation ($$\texttt{ReconstKey}$$ function).

The process macro consists of sub-processes such that different sub-processes are defined for different parties in the protocol in order to ease the development: Privacy-Enhanced STS-KDF-CB Protocol (Section 5.1.1) and Privacy-Enhanced STS-KDF-CB with KEM Protocol (Section 5.1.2), have two parties, say Alice and Bob. Split-Key Privacy-Enhanced STS-KDF-CB Protocol (Section 5.2.1) and Split-Key Privacy-Enhanced STS-KDF-CB with KEM Protocol (Section 5.2.2) have two additional parties, say Alice2 and Bob2. In ProVerif models, we created a sub-process for each party.

Finally, the protocol is encoded as a main process using the process macros. Next, we explain the main processes of the protocols of Section 5. We model the CA by simply generating secret and public $$ sk_{CA} $$ and $$ pk_{CA} $$ in the main process, where $$ pk_{CA} $$ is output in the public channel that we call $$ \texttt{internet}$$. Then, to construct a certificate for a user with identity, say Alice, holding a pair of public/private keys $$ (pk_1, sk1) $$, we use the function $$\texttt{makecert(Alice}$$, $$ pk_1 $$, $$ sk_1 $$).

Protocol 1: STS-KDF: The main process creates secret-public signing and verification keys for CA, Alice, and Bob.

Protocol 2: Privacy-Enhanced STS-KDF-CB: The main process of Protocol 2 has the same main process as Protocol 1.

Protocol 3: Privacy-Enhanced STS-KDF-CB with KEM: The main process of Protocol 2 differs from Protocol 1 only when creating secret and public keys: $$\texttt{new sk1:skey; let pk1=pk(sk1)}$$ for Alice and $$\texttt{new sk2:skey; let pk2=pk(sk2)}$$ for Bob. Note that, in this protocol, keys for asymmetric encryption are derived instead of signature keys.

Protocol 4: Split-Key Privacy-Enhanced STS-KDF-CB: This protocol has two more parties participating, and the main process is prepared accordingly:

Protocol 5: Split-Key Privacy-Enhanced STS-KDF-CB with KEM: The setup of the main process of Protocol 5 is similar to Protocol 4, except for generating split keys for asymmetric encryption. In addition, in this protocol, a verification key for Split-KEM is generated for Alice1 and Bob1: $$ \texttt{let vk1=vk(pk1, sk1, sk2) in}$$ and $$ \texttt{let vk3=vk(pk3, sk3, sk4) in}$$, respectively.

Queries

In ProVerif, $$\texttt{events}$$ are defined while modeling the protocol to record incidents, e.g., key derivation and signature verification. These events are used to check if the protocol runs without errors by checking the reachability of events and construct correspondence assertions by capturing the relationships between events ^[13].

A query is a statement about a security property that is wanted to verify. It is used to express a specific security property or behavior that is expected by a protocol or system to satisfy.

Next, we list the queries that we have constructed to verify the security properties. Note that the protocols with KEM do not have queries for DH key $$ K_{DH} $$.

Secrecy: We want to prove the secrecy of the key that is derived during the protocol run. Therefore, we constructed the following queries:

Mutual Authentication: In ProVerif, the correspondence is defined for two events, $$\texttt{e2}$$ and $$\texttt{e1}$$, such that the query for $$\texttt{event(e2(M))==>event(e1(N))}$$ means if an event $$\texttt{e2(M)}$$ has been executed, then event $$\texttt{e1(N)}$$ has been previously executed. The in-built functionality, injective correspondence, of ProVerif additionally checks if the number of occurrences of $$\texttt{e1(N)}$$ is greater than or equal to the number of occurrences of $$\texttt{e2(M)}$$, in addition to the correspondence queries ^[13]. Mutual authentication can be proved by proving injective agreement based on the shared keys:

Forward Secrecy: To prove forward secrecy we use phases^[13]. We leak the long-term secret keys after the initial run of the protocol (phase 1) and show the secrecy property of the session that took place before the leak $$\texttt{(phase 0)}$$. For this end, we use: $$\texttt{phase 1; out(internet, (sk1, sk2, skCA))}$$.

Resistance to Unknown Key Share (UKS) attack: In order to construct queries for proving the resistance to UKS attacks, we use the events that are used to prove mutual authentication so that if these events occur for the same key, then the identities of the parties should be same. We check the UKS attack resistance for the keys $$ K_{DH} $$ and $$ K $$, and identities $$ Alice $$ and $$ Bob $$.

Resistance to Key Compromise Impersonation (KCI) attack: We want to verify that the protocol is resistant to KCI attacks by leaking the secret keys in the main process. Consequently, if the secrecy and correspondence queries remain true, then we conclude that the protocol is resistant to KCI attacks:

When KCI resistance is checked, these lines should be replaced with the corresponding lines in the main process.

Identity Confidentiality: The identity confidentiality of the users against outsiders can be verified by the notion of observational equivalence, see ^[13] Section 4.3.2. When we check the observational equivalence of Bob, we ask ProVerif to choose an identity for Bob while we assign a new identity to Alice. Note that $$\texttt{Bob1}$$ and $$\texttt{Bob2}$$ are public names. These are the identity assignments for Alice and Bob to check observational equivalence of Bob:

Note that the certificates, and, therefore, the identities, are already public. While creating certificates, we send the certificates that are made for Alice, Bob1, and Bob2 to the public network. However, we also create another certificate for chosen Bob, which should be the same as the certificate of either Bob1 or Bob2, and we send this certificate to Bob via a private channel. In addition, in our protocols, the certificates are sent in an encrypted form.

Formal verification results

After introducing how to construct the model for formally verifying the protocols, we now explain the results of the formal verification. We will start with the security properties of the STS-KDF protocol (Protocol 1) and then continue with the security properties of the other protocols when they differ from those of the STS-KDF protocol. A summary of the formal verification results is given in Table 1 and Table 2.

The identity confidentiality results vary depending on users. Table 2 presents the ProVerif results for identity confidentiality of user identities.

The following is the explanation of security properties that we get from ProVerif results.

Secrecy of $$ K $$: The attacker cannot capture the shared key $$ K $$.

Mutual authentication on $$ K_{DH} $$: The injective correspondences on $$ K_{DH} $$ are true. This means that the mutual authentication between Alice and Bob is achieved for $$ K_{DH} $$.

Mutual authentication on $$ K $$: The injective correspondences on $$ K $$ are false, which means that there is no mutual authentication between Alice and Bob for the key $$ K $$. This is because the parties do not perform key confirmation on $$ K $$. In this protocol, the master key is $$ K_{DH} $$, and this key is confirmed in the protocol. In addition, the identities of the parties are also confirmed through the certificates. STS-KDF is a standalone protocol, and $$ K $$ will be confirmed indirectly later when it is used.

Forward Secrecy: The STS-KDF protocol has forward secrecy. The leak of the secret keys of Alice, Bob, and CA does not help the attacker recover the session keys derived during earlier sessions.

Resistance to Unknown Key Share Attack on $$ K_{DH} $$: STS-KDF protocol is secure against the UKS attacks on $$ K_{DH} $$.

Resistance to Unknown Key Share Attack on $$ K $$: STS-KDF protocol is secure against the UKS attacks $$ K $$.

Resistance to Key Compromise Impersonation (KCI) attack: When the secret keys of Alice and Bob are leaked at the beginning of the protocol, the secrecy of the keys and the mutual authentication between Alice and Bob on $$ K_{DH} $$ both return false. This means that the STS-KDF protocol is vulnerable to KCI attacks.

Identity Confidentiality: The certificates are sent in plaintext in the protocol; therefore, identity confidentiality is trivially not true for STS-KDF.

Next, we highlight the differences in security properties between STS-KDF and the protocols developed in this paper.

Privacy-Enhanced STS-KDF-CB protocols (Protocols 2, 3, 4, and 5) provide identity confidentiality so that the identities of the parties are not captured by outsiders and passive attackers. However, if the attacker starts Protocols 2 and 4 by sending the first message containing his public key to Bob, then Bob derives the shared DH key ($$ K_{DH} $$) using the attacker's public key. Even though Bob encrypts his certificate with $$ K_{DH} $$, the attacker also derives the same key. Therefore, the attacker can decrypt the message in Step 4 of Figure 5 and obtain Bob's certificate. On the other hand, Protocols 3 and 5 can overcome this problem.

A limitation of our ProVerif model is that it cannot detect information exposure through error messages. However, the attacker could learn the identity of Bob with this kind of information exposure in Protocols 3 and 5. For example, the attacker replays Message (2) of Protocol 3 in Figure 5. If the ciphertext $$ C_0 $$ is computed with the correct $$ pk_b $$, then Bob can execute the rest of (3) and send (4). Bob can understand in (7) that either the other party is not Alice or does not have the key. Therefore, the protocol fails at the end. If the ciphertext $$ C_0 $$ is computed with the wrong $$ pk_b $$, then Bob cannot execute (3.a) and understands that this message is not intended for him. If Bob rejects explicitly by raising an Error at this step, the attacker would understand that this user is not the same Bob that the original Message (2) was sent to. The protocol could be enhanced in such a way that Bob rejects implicitly as follows. He sends an invalid ciphertext, which the attacker cannot distinguish from a successful reply to Message (2). The genuine Alice (who in the example sent the original Message (2)) would still understand the rejection because the ciphertext is invalid.

In Privacy-Enhanced STS-KDF-CB protocols, parties check the certificate of the other party so that they do not receive their own certificates. They do this check by executing $$\texttt{if certA <>certB then}$$ line. When we apply observational equivalence, we choose from two identifiers, Bob1 and Bob2, but they keep using the same public-secret key pair. This is why there is no observation equivalence in Protocols 3 and 5. However, if we check $$\texttt{if Alice <>Bob && pkA <>pkB}$$ by restricting that the public keys are also different, we can get observational equivalence.

Privacy-Enhanced STS-KDF-CB with KEM (Protocol 3) and Split-Key Privacy-Enhanced STS-KDF-CB with KEM (Protocol 5) protocols achieve mutual authentication for the key $$ K $$.

Note that the queries related to $$ K_{DH} $$ are non-applicable for Protocols 3 and 5 since the DH key exchange is replaced by KEM; therefore, the key $$ K_{DH} $$ is not derived.

Considering Protocols 2 and 3, when the secret key of Alice is leaked at the beginning of the protocol, the secrecy of Bob's key and injective correspondence of Bob for Alice on $$ K_{DH} $$ return false. Similarly, if Bob's key is leaked, then the secrecy of Alice's key is compromised, and the injective correspondence of Bob for Alice on $$ K_{DH} $$ returns false. This means that if the key of one party is leaked, the secrecy and authentication of the other party is compromised.

In a split-key setting (Protocols 4 and 5), a KCI attack is unsuccessful only if the secret keys of Alice2 and Bob2 are leaked. However, the cases for Alice1 and Bob1 are similar to those of Alice and Bob in Protocols 2 and 3.

Construction of reflection attack in ProVerif

In Section 4, we have explained that the reflection attack happens in a setting where the parties in the protocol have the same secret key but different identities and, therefore, different certificates. In order to capture the reflection attack in ProVerif, we have modified the protocol such that (ⅰ) only one secret key is created and assigned to the parties, (ⅱ) the certificates are created with different identities but the same public key, and (ⅲ) we allow that Alice and Bob can be both initiator and responder in the protocol.

In this setting, we could capture the reflection attack against STS-KDF in ProVerif. When the protocol model is executed, the mutual authentication for the DH key returns false. The traces captured from the query,

ProVerif proved that the reflection attack is not successful when a similar setting is applied to Privacy-Enhanced STS-KDF-CB and Privacy-Enhanced STS-KDF-CB with KEM protocols.

Authors' contributions

Conceptualization: Akman G, Damir MT, Ginzboorg P, Sovio S, Niemi V

Supervision: Ginzboorg P, Sovio S, Niemi V

Writing - original draft preparation: Akman G

Writing - review and editing: Damir MT, Ginzboorg P, Sovio S, Niemi V

Formal analysis: Akman G, Damir MT

Visualization: Akman G

All authors have read and agreed to the published version of the manuscript.

Availability of data and materials

The source code of our ProVerif Models is available in a GitHub repository ^[41].

Financial support and sponsorship

This research is a result of a funded collaboration project between the University of Helsinki and Huawei Technologies, Finland.

Conflicts of interest

All authors declared that there are no conflicts of interest.

Ethical approval and consent to participate

Not applicable.

Consent for publication

Not applicable.

Copyright

© The Author(s) 2023.