PQuAKE - Post-Quantum Authenticated Key Exchange
draft-uri-cfrg-pquake-00
This document is an Internet-Draft (I-D).
Anyone may submit an I-D to the IETF.
This I-D is not endorsed by the IETF and has no formal standing in the
IETF standards process.
| Document | Type | Active Internet-Draft (individual) | |
|---|---|---|---|
| Authors | Uri Blumenthal , Brandon Luo , Sean O'Melia , Gabriel Torres , David A. Wilson | ||
| Last updated | 2026-06-04 | ||
| RFC stream | (None) | ||
| Intended RFC status | (None) | ||
| Formats | |||
| Stream | Stream state | (No stream defined) | |
| Consensus boilerplate | Unknown | ||
| RFC Editor Note | (None) | ||
| IESG | IESG state | I-D Exists | |
| Telechat date | (None) | ||
| Responsible AD | (None) | ||
| Send notices to | (None) |
draft-uri-cfrg-pquake-00
Crypto Forum Research Group U. Blumenthal
Internet-Draft B. Luo
Intended status: Informational S. O'Melia
Expires: 6 December 2026 G. Torres
D. Wilson
MIT
4 June 2026
PQuAKE - Post-Quantum Authenticated Key Exchange
draft-uri-cfrg-pquake-00
Abstract
This document defines the Post-Quantum Authenticated Key Exchange
(PQuAKE) protocol that addresses the needs of bandwidth- and/or
power-constrained environments, while maintaining strong security
guarantees. It accomplishes that by minimizing the number of bits
that need to be exchanged and by utilizing an implicit peer
authentication approach similar to Menezes-Qu-Vanstone (MQV) design.
This protocol is suitable for integration into protocols that
establish dynamic secure sessions, such as Extensible Authentication
Protocol (EAP), Internet Key Exchange Version 2 (IKEv2), or Secure
Communications Interoperability Protocol (SCIP). This protocol has
proofs in the verifiers Verifpal and CryptoVerif for security
properties such as secrecy of the session key, mutual authentication,
identity hiding with a pre-shared secret, and forward secrecy of the
session key. The authors are in the process of publishing the
proofs.
About This Document
This note is to be removed before publishing as an RFC.
The latest revision of this draft can be found at
https://mouse07410.github.io/pquake-draft/draft-uri-cfrg-pquake.html.
Status information for this document may be found at
https://datatracker.ietf.org/doc/draft-uri-cfrg-pquake/.
Discussion of this document takes place on the Crypto Forum Research
Group Research Group mailing list (mailto:cfrg@irtf.org), which is
archived at https://mailarchive.ietf.org/arch/browse/cfrg/.
Subscribe at https://www.ietf.org/mailman/listinfo/cfrg/.
Source for this draft and an issue tracker can be found at
https://github.com/mouse07410/pquake-draft.
Status of This Memo
This Internet-Draft is submitted in full conformance with the
provisions of BCP 78 and BCP 79.
Internet-Drafts are working documents of the Internet Engineering
Task Force (IETF). Note that other groups may also distribute
working documents as Internet-Drafts. The list of current Internet-
Drafts is at https://datatracker.ietf.org/drafts/current/.
Internet-Drafts are draft documents valid for a maximum of six months
and may be updated, replaced, or obsoleted by other documents at any
time. It is inappropriate to use Internet-Drafts as reference
material or to cite them other than as "work in progress."
This Internet-Draft will expire on 6 December 2026.
Copyright Notice
Copyright (c) 2026 IETF Trust and the persons identified as the
document authors. All rights reserved.
This document is subject to BCP 78 and the IETF Trust's Legal
Provisions Relating to IETF Documents (https://trustee.ietf.org/
license-info) in effect on the date of publication of this document.
Please review these documents carefully, as they describe your rights
and restrictions with respect to this document.
Table of Contents
1. Introduction
1.1. Compliance requirements for the components
1.2. Mandatory-To-Implement algorithms
2. Conventions and Definitions
3. Protocol Description
3.1. Protocol Diagram
3.2. Exchange certificates
3.2.1. Key Derivation of k_hid with preshared secret
3.2.2. Key Derivation of k_hid without preshared secret
3.2.3. Initiator
3.2.4. Responder
3.3. Encapsulate shared secrets
3.3.1. Initiator
3.3.2. Responder
3.4. Decapsulate ciphertexts and key derivation
3.4.1. Initiator
3.4.2. Responder
3.5. Key Confirmation
3.5.1. Initiator
3.5.2. Responder
3.6. Error Handling
4. Protocol Messages
4.1. Message Format
4.2. Hello Messages
4.2.1. Initiator Hello
4.2.2. Responder Hello
4.3. Certificate Exchange
4.4. Certificate Format
4.5. Encapsulation
4.6. Key Confirmation
5. Integration into IKEv2
6. Integration into EDHOC
7. Integration into EAP
8. Formal Proofs
8.1. Methodology
8.2. Proven Security Properties
8.3. Cryptographic Assumptions
8.4. Proof Approach (Intuition)
8.5. Limitations and Future Work
9. Security Considerations
10. IANA Considerations
11. References
11.1. Normative References
11.2. Informative References
Acknowledgments
Authors' Addresses
1. Introduction
The primary goal of PQuAKE is to minimize the communication overhead
of Post-Quantum (PQ) public-key cryptography during a key exchange.
Bandwidth or power limited devices may not realistically use
alternative PQ key exchanges such as the TLS handshake protocol to
derive a shared symmetric key, as PQ digital signatures and keys are
drastically larger. This protocol minimizes the communication
overhead by reducing the number of signatures transmitted by each
party to one offline-generated certificate signature. It is designed
to be an add-on to such protocols as EAP [EAP], IKEv2, and others.
Since computing a PQ digital signature typically is more expensive
than performing a PQ KEM, there is a benefit of reduced computational
costs.
The overall idea of the implicit authentication of the peers comes
from the MQV protocol.
Both parties MAY have a pre-shared symmetric secret key, usually
distributed among all the members of the given network or Community
of Interest (COI). Adding a pre-shared symmetric key to the key
derivation ensures confidentiality of the peers' identities
(certificates) against active attackers that do not have that pre-
shared key.
The protocol maintains the following security guarantees:
* The secure channel between the Initiator and Responder is mutually
authenticated - Key freshness, aka a new key is generated for this
channel, and it hasn't been reused or stale; - If two parties
properly follow the protocol, both parties will compute the same
shared keys that are known only to them; - Perfect Forward
Secrecy, aka after the channel is closed, there is no way for an
adversary to break security properties associated with the shared
key established via this protocol; - Security against replay
attacks; - Confidentiality of peers' identities against passive
adversary; - Confidentiality of peers' identities against active
adversary (aka, Man-In-The-Middle) when both peers utilize long-
term pre-shared key.
This protocol has proofs in the verifiers Verifpal and CryptoVerif
for security properties such as secrecy of the session key, mutual
authentication, identity hiding with a preshared secret, and forward
secrecy of the session key. The authors are in the process of
publishing the proofs.
It is important to note that PQuAKE does not replace protocols like
the TLS record protocol, only the handshake protocol. Other
protocols such as IKEv2, SCIP, or EAP may integrate PQuAKE into their
key exchange phase.
1.1. Compliance requirements for the components
The building blocks of this protocol SHALL have the following
security properties:
* Symmetric Key Cryptosystem - IND-CCA2 - Key Encapsulation
Mechanism (KEM) - Implicit, IND-CCA2 and IK-CCA2 - Key Derivation
Function 1 - Random Oracle Hash Function - Key Derivation Function
2 - Random Oracle Hash Function - Message Authentication Code
(MAC) - Pseudorandom Function
1.2. Mandatory-To-Implement algorithms
While this protocol has been formally proven to work with any KEM,
MAC, and symmetric cipher that exhibit the above properties --
interoperability requires that a Mandatory-To-Implement (MTI) set of
algorithms is specified for the Version 1 of the protocol:
* Enc: AES-GCM-256 - KEM: ML-KEM-1024 - Hash: SHA384 - MAC: HMAC -
KDF: HKDF - Signature: ML-DSA-87
2. Conventions and Definitions
The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT",
"SHOULD", "SHOULD NOT", "RECOMMENDED", "NOT RECOMMENDED", "MAY", and
"OPTIONAL" in this document are to be interpreted as described in
BCP 14 [RFC2119] [RFC8174] when, and only when, they appear in all
capitals, as shown here.
3. Protocol Description
The PQuAKE protocol consists of four steps. Within each step, the
exchanges can happen asynchronously, but one step (aka, all of the
exchanges of that step) MUST conclude before the peers can proceed to
the next one. If any step results in an error, the protocol SHOULD
abort. That includes receiving an out-of-order or corrupted message,
or not receiving an expected message within the deployer-configured
time interval. However, the protocol SHOULD only abort at the end of
the protocol if the peer's identity does not match an out-of-band
verification, and an implicit KEM without aborts SHOULD be used.
Ideally, the protocol SHOULD only abort after the key confirmation
step if the reason for aborting is related to the identities of the
two parties.
Currently, no notification to the other party, such as information
about an abnormal completion and/or giving details of the error, is
included in the protocol.
The four steps are the following:
1. Establish an ephemeral symmetric key via hello messages and
exchange encrypted certificates (one MUST use an encryption
scheme with IND-CCA2 security and an implicit KEM with IND-CCA2
security and IK-CCA2 security). 2. Encapsulate shared secrets
and exchange the ciphertexts.
2. Decapsulate shared secrets, derive key confirmation keys and a
session key. 4. Perform Key Confirmation.
Note that both peers take full transcripts (chain-hashes) of all the
messages they send and receive, and include the resulting hash
outputs among the inputs of the Key Derivation Function (KDF) that
gets invoked to generate shared secrets (first for encrypting
certificates, and the next time - to provide the shared secret that
is the purpose of this protocol).
While both parties have to share their certificates or identities for
authentication, we assume the identities of each party shall remain
confidential to those outside of this exchange. They encrypt their
certificates with a shared symmetric ephemeral key that they generate
via a ephemeral KEM. This key is used to encrypt the certificate and
is an input to the KDF when generating the shared key. The final KDF
that provides the negotiated shared secret, will also include this
symmetric key in its input.
Instead of generating a signature over the handshake transcript like
TLS, PQuAKE performs an implicit authentication of the handshake. It
does this by making the protocol's session key dependent on not only
a series of KEM calculated shared secrets but also dependent on the
hashes of the sent and received messages. Since only their
corresponding party, who they have authenticated, can know those
secrets, deriving the same session key implicitly authenticates each
other while creating a shared secret.
3.1. Protocol Diagram
Initiator Responder
-------------------------------------------------------------------
Establish confidential link and exchange certificates
-----------------------------------------------------
(sk_e, pk_e) <- KEM.keygen()
{ pk_e } -->
(ct_e, ss_e) <- KEM.encap(pk_e)
<-- { ct_e }
ss_e <- KEM.decap(ct_e, sk_e)
k_hid <- kdf_1(ss_pre, ss_e || "HID")
k_hid <- kdf(ss_pre, ss_e || "HID")
e_cert_i <- Enc(k_hid, cert_i) e_cert_r <- Enc(k_hid, cert_r)
{ e_cert_i } --> <-- { e_cert_r }
Encapsulate and send shared secrets
-----------------------------------
cert_r <- Dec(k_hid, e_cert_r) cert_i <- Dec(k_hid, e_cert_i)
if cert_r is not valid, abort if cert_i is not valid, abort
(ct_i, ss_i) <- KEM.encap(pk_r) (ct_r, ss_r) <- KEM.encap(pk_i)
{ ct_i } --> <-- { ct_r }
Decapsulate shared secrets and derive session keys
--------------------------------------------------
ss_r <- KEM.decap(sk_i, ct_r) ss_i <- KEM.decap(sk_r, ct_i)
send_hash <- H(hf, pk_e, e_cert_i, ct_i)
send_hash <- H(hf, ct_e, e_cert_r, ct_r)
recv_hash <- H(hf, ct_e, e_cert_r, ct_r)
recv_hash <- H(hf, pk_e, e_cert_i, ct_i)
S <- ss_e||ss_i||ss_r||send_hash||recv_hash
S <- ss_e||ss_i||ss_r||recv_hash||send_hash
k_C_i, k_C_r, ... <- kdf_2(hf2, S)
k_C_i, k_C_r, ... <- kdf_2(hf2, S)
Key Confirmation
----------------
{ HMAC(k_C_i, recv_hash || send_hash) } -->
<-- { HMAC(k_C_r, send_hash || recv_hash) }
3.2. Exchange certificates
During this step, both nodes establish a shared ephemeral key via a
KEM, then use it to encrypt certificates before transmitting them.
The initiator generates an ephemeral key and transmits the
encapsulated secret. The responder MUST decapsulate the ciphertext.
Both parties MUST derive a shared ephemeral key from the encapsulated
secret and the pre-shared secret if it is present. Both parties MUST
encrypt and transmit their certificates. Both parties MUST validate
the certificate's signature. If the verification of a signature
fails, the protocol MUST abort. Implementors need to be careful to
avoid aborting based off the other node's identity until the end of
the protocol to maintain identity hiding of the peer. Note that key
encapsulation mechanism SHOULD be IND-CCA2 and IK-CCA2 secure and
SHOULD NOT abort (it SHOULD be an implicit KEM).
3.2.1. Key Derivation of k_hid with preshared secret
k_hid <- kdf_1(ss_pre, ss_e || "HID");
3.2.2. Key Derivation of k_hid without preshared secret
k_hid <- kdf_1(ss_e, "HID");
3.2.3. Initiator
e_cert_i <- E(k_hid, cert_i);
3.2.4. Responder
e_cert_r <- E(k_hid, cert_r);
3.3. Encapsulate shared secrets
During this step, both nodes generate an encapsulated secret via a
KEM. The ciphertexts are exchanged.
3.3.1. Initiator
(ct_r, ss_r) <- KEM.encap(pk_i);
3.3.2. Responder
(ct_i, ss_i) <- KEM.encap(pk_r);
3.4. Decapsulate ciphertexts and key derivation
The ciphertexts are decapsulated by both parties. At this point,
both sides have all the shared secrets required to derive a set of
session keys.
3.4.1. Initiator
send_hash <- hash(pk_e, e_cert_i, ct_i);
recv_hash <- hash(ct_e, e_cert_r, ct_r);
transcript <- (send_hash, recv_hash);
k_C_i, k_C_r, k_session = kdf_2(ss_e, ss_i, ss_r, transcript);
3.4.2. Responder
send_hash <- hash(ct_e, e_cert_r, ct_r);
recv_hash <- hash(pk_e, e_cert_i, ct_i);
transcript <- (recv_hash, send_hash);
k_C_i, k_C_r, k_session = kdf_2(ss_e, ss_i, ss_r, transcript);
3.5. Key Confirmation
Key confirmation is done by calculating an HMAC of the chain-hash of
all the sent and received messages correspondingly, using the
appropriate Key Confirmation key derived in step 3. The initiator
MUST use the key K~ir~, and the responder MUST use the key K~ri~.
3.5.1. Initiator
C_i <- HMAC(k_C_i, send_hash || recv_hash);
3.5.2. Responder
C_r <- HMAC(k_C_r, recv_hash || send_hash);
3.6. Error Handling
We make no assumptions about the underlying transport that carries
PQuAKE messages, because no error - whether maliciously introduced or
accidental - in any of its messages can impact correctness of the
protocol itself. We consider two kinds of errors:
a. Corruption of a message - will result in protocol failure (abort)
b. Failure to receive a message within expected time interval, aka
timeout - will result in protocol failure (abort).
Handling the protocol timeout (how long to wait until declaring
failure to receive) is the responsibility of the implementation
deployer. The implementer SHOULD make this value configurable.
Note: the more the underlying transport does to detect or mitigate
line errors (aka, non-malicious errors), the likelier the protocol is
to successfully complete. Ideally, the transport would offer at
least the capabilities of UDP.
4. Protocol Messages
We do not include explicit checksums because it is practically
impossible for the protocol to succeed if any message would arrive
corrupted, either maliciously, or by a random error.
4.1. Message Format
A message of the protocol is formatted as follows:
0 1 2 3 0 1 2 3 4 5 6 7 0
1 2 3 4 5 6 7 0 1 2 3 4 5 6 7 0 1 2 3 4 5 6 7
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
| Version | Type | Length |
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
| Data ...
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
Version: 8 bits
The version field indicates the format of the initiator hello
message. This document describes version 1.
Type: 8 bits
This field indicates the current step of the protocol.
Length: 16 bits
Length is the length of the data, measured in octets. This field
allows the length of the data to be up to 65535 octets.
Data: variable
This field changes based on the current step of the protocol.
4.2. Hello Messages
The Initiator generates an ephemeral KEM key-pair (sk_e, pk_e) =
KEM.keygen() and sends the public key pk_e to its intended recipient
(the Responder). The Responder performs encapsulation (ct_e, ss_e) =
KEM.encap(pk_e) and sends the ciphertext ct_e to the Initiator.
4.2.1. Initiator Hello
An Initiator Hello message is formatted as follows:
0 1 2 3 0 1 2 3 4 5 6 7 0
1 2 3 4 5 6 7 0 1 2 3 4 5 6 7 0 1 2 3 4 5 6 7
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
| Version | Type | Length |
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
| Ephemeral Public Key ...
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
Version: 8 bits
The version field indicates the format of the initiator hello
message. This document describes version 1.
Type: 1
This field indicates the state of the protocol.
Length: 16 bits
Length is the length of the ephemeral public key, measured in octets.
This field allows the length of a ephemeral public key to be up to
65535 octets.
Ephemeral Public Key: variable
This field SHOULD be unique for each protocol execution.
4.2.2. Responder Hello
A Responder Hello message is formatted as follows:
0 1 2 3 0 1 2 3 4 5 6 7 0
1 2 3 4 5 6 7 0 1 2 3 4 5 6 7 0 1 2 3 4 5 6 7
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
| Version | Type | Length |
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
| Encapsulated Secret ...
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
Type: 2
Encapsulated Secret: variable
The size of this field depends on the key encapsulation mechanism
used.
4.3. Certificate Exchange
A Certificate Exchange message is formatted as follows:
0 1 2 3 0 1 2 3 4 5 6 7 0
1 2 3 4 5 6 7 0 1 2 3 4 5 6 7 0 1 2 3 4 5 6 7
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
| Version | Type | Length |
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
| Initial Vector | Encrypted Certificate ...
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
| Authentication Tag |
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
Type: 3 for initiator, 4 for responder
Initial Vector: 96 bits
Encrypted Certificate: variable
Authentication Tag: 128 bits
The certificate encrypted with the derived key k_hid.
4.4. Certificate Format
For now, we use standard X.509 certificate [X.509] with OIDs
specifying ML-KEM [FIPS203] and ML-DSA [FIPS204] correspondingly.
Future extensions may use different certificate formats.
4.5. Encapsulation
An Encapsulation message is formatted as follows:
0 1 2 3 0 1 2 3 4 5 6 7 0
1 2 3 4 5 6 7 0 1 2 3 4 5 6 7 0 1 2 3 4 5 6 7
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
| Version | Type | Length |
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
| Encapsulated Secret ...
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
Type: 5 for initiator, 6 for responder
Encapsulated Secret: variable
The size of this field depends on the key encapsulation mechanism
used.
4.6. Key Confirmation
A Key Confirmation message is formatted as follows:
0 1 2 3 0 1 2 3 4 5 6 7 0
1 2 3 4 5 6 7 0 1 2 3 4 5 6 7 0 1 2 3 4 5 6 7
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
| Version | Type | Length |
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
| Key Confirmation Value ...
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
Type: 7 for initiator, 8 for responder
Key Confirmation Value: 384 bits (output size of SHA384)
This field is the computed HMAC value of the exchange transcript.
5. Integration into IKEv2
PQuAKE can be integrated into IKEv2 [IKEV2] as an alternative
authenticated key exchange mechanism.
One possible approach is:
* Use IKE_SA_INIT to perform classical negotiation and optional
hybrid key exchange signaling - Use IKE_INTERMEDIATE exchanges to
carry PQuAKE messages - Replace explicit signatures in IKE_AUTH
with PQuAKE key confirmation
This results in an implicitly authenticated key exchange, where
authentication is achieved via shared secret derivation rather than
explicit signatures.
This section is *illustrative only*. A complete and interoperable
integration requires a dedicated specification that defines:
* Payload formats - Negotiation mechanisms - Transcript binding -
Error handling and downgrade protection
Such work is out of scope for this document.
6. Integration into EDHOC
PQuAKE can be conceptually integrated into EDHOC by replacing or
augmenting its authenticated key exchange phase with PQuAKE's
implicit authentication mechanism.
A possible mapping includes:
* Using EDHOC message_1 / message_2 to carry the ephemeral KEM
exchange
* Encrypting credentials using the derived ephemeral secret -
Embedding PQuAKE encapsulation messages into subsequent EDHOC
exchanges - Using EDHOC exporter interface to derive application
keys from the PQuAKE session key
This would preserve EDHOC's compactness while enabling post-quantum
implicit authentication.
This is a *proof-of-concept illustration only*. A production-quality
integration would require a dedicated RFC specifying:
* Message encoding and transcript construction - Credential formats
- Interaction with EDHOC authentication methods - Security
analysis specific to EDHOC composition
7. Integration into EAP
PQuAKE may be incorporated into the Extensible Authentication
Protocol (EAP) [EAP] as a new EAP method.
In such a design:
* The PQuAKE exchange would form the EAP authentication conversation
- Certificates or identities would be transported within EAP
payloads - The derived session key would be exported via the EAP
key hierarchy
This approach enables post-quantum authenticated key exchange for
network access scenarios (e.g., Wi-Fi, 5G, enterprise access).
This is a *proof-of-concept illustration only*. A standards-track
integration would require a dedicated RFC defining:
* EAP method type and state machine - Fragmentation and
retransmission behavior - Key derivation and export interfaces -
Interaction with AAA infrastructure
8. Formal Proofs
The security properties of PQuAKE have been analyzed using both
symbolic and computational models, following the methodology
developed for [CAKE-HI].
8.1. Methodology
Two independent formal verification frameworks were used:
* *CryptoVerif* (computational model): - Game-based proofs via
sequence-of-games transformations - Adversary modeled as
probabilistic polynomial-time (PPT), including quantum adversaries
with classical oracle access - *Verifpal* (symbolic model): -
Active attacker model with message modification and replay -
Automated reachability and secrecy analysis
These tools provide complementary assurances: CryptoVerif establishes
computational security under standard assumptions, while Verifpal
validates protocol logic against a wide class of symbolic attacks.
8.2. Proven Security Properties
Under the assumptions listed below, the following properties are
established:
* *Secrecy of the session key*: Reduced to IND-CCA2 security of the
KEM and the random-oracle behavior of KDFs
* *Mutual authentication*: Successful key confirmation implies that
both parties performed correct decapsulation using their
respective long-term secret keys
* *Forward secrecy*: Achieved via inclusion of the ephemeral KEM
shared secret; compromise of long-term keys does not reveal past
session keys
* *Key freshness*: Derived keys are indistinguishable from random
and unique across sessions
* *Identity hiding*: Achieved via encryption of certificates under
an ephemeral shared key, relying on IND-CCA2 encryption and IK-
CCA2 KEM properties
8.3. Cryptographic Assumptions
The proofs rely on the following assumptions:
* KEM is *IND-CCA2* and *IK-CCA2* secure - KEM is *implicitly
rejecting* - KDF behaves as a *random oracle* - HMAC is a
*pseudorandom function (PRF)* - Hash function (e.g., SHA-384) is
*collision-resistant* - Domains of KDF invocations are properly
separated
8.4. Proof Approach (Intuition)
* Secrecy and forward secrecy are obtained by replacing KEM-derived
shared secrets with uniformly random values under IND-CCA2
security, then applying random oracle arguments to the KDF.
* Authentication follows from the fact that successful key
confirmation requires correct computation of shared secrets
derived via decapsulation with the corresponding private key.
* Identity hiding is obtained by combining: - IND-CCA2 security of
certificate encryption - IK-CCA2 security of the KEM - PRF
security of HMAC
8.5. Limitations and Future Work
* Current proofs rely on the (classical) random oracle model -
Extensions to the quantum random oracle model (QROM) remain future
work
* Stronger composability guarantees (e.g., UC-security) are not yet
established
Full formal models and proof artifacts are in the process of
publication.
9. Security Considerations
This is a security protocol, and it holds the properties described in
(TODO reference) in the presence of passive or active attacker on the
network.
One potential concern is the confidentiality of the peers' identities
carried in their certificates. An active attacker can learn their
identities during the certificate exchange step. Using a pre-shared
secret will prevent disclosure of these certificates, keeping peers
identities confidential. Since there are costs associated with out-
of-band distribution of that secret, it would be typically shared
among the Community of Interest (CoI). In that case, this protocol
would protect peers identities against active attackers outside of
this Community of Interest, but not against an active attacker that
is a member of CoI.
10. IANA Considerations
None.
11. References
11.1. Normative References
[IKEV2] Kaufman, C., Hoffman, P., Nir, Y., Eronen, P., and T.
Kivinen, "Internet Key Exchange Protocol Version 2
(IKEv2)", STD 79, RFC 7296, DOI 10.17487/RFC7296, October
2014, <https://www.rfc-editor.org/rfc/rfc7296>.
[RFC2119] Bradner, S., "Key words for use in RFCs to Indicate
Requirement Levels", BCP 14, RFC 2119,
DOI 10.17487/RFC2119, March 1997,
<https://www.rfc-editor.org/rfc/rfc2119>.
[RFC8174] Leiba, B., "Ambiguity of Uppercase vs Lowercase in RFC
2119 Key Words", BCP 14, RFC 8174, DOI 10.17487/RFC8174,
May 2017, <https://www.rfc-editor.org/rfc/rfc8174>.
[X.509] Housley, R., Ford, W., Polk, W., and D. Solo, "Internet
X.509 Public Key Infrastructure Certificate and CRL
Profile", RFC 2459, DOI 10.17487/RFC2459, January 1999,
<https://www.rfc-editor.org/rfc/rfc2459>.
11.2. Informative References
[BATTARBEE-2025-1228]
Battarbee, C., Striecks, C., Perret, L., Ramacher, S., and
K. Verhaeghe, "Quantum-Safe Hybrid Key Exchanges with KEM-
Based Authentication", IACR ePrint 2025/1228, 2025,
<https://eprint.iacr.org/2025/1228>.
[BJM-KA] Blake-Wilson, S., Johnson, D., and A. Menezes, "Key
Agreement Protocols and Their Security Analysis",
DOI 10.1007/BFb0024447, December 1997,
<https://doi.org/10.1007/BFb0024447>.
[CAKE-HI] Blumenthal, U., Itkis, G., Khazan, R., Luo, B., O'Melia,
S., Proulx, B., Stott, D., Torres, G., and D. A. Wilson,
"CAKE-HI - Compact Authenticated Key Exchange Hiding
Identities", unpublished manuscript, 14 pp., n.d..
[CHEN-MCELIECE-FPGA]
Chen, P., "Complete and Improved FPGA Implementation of
Classic McEliece", CHES 2022, 2022,
<https://eprint.iacr.org/2022/412>.
[CLASSIC-MCELIECE]
Bernstein, D. J., "Classic McEliece (Round 4)", NIST
PQC Round 4, October 2022, <https://classic.mceliece.org>.
[EAP] Aboba, B., Simon, D., and P. Eronen, "Extensible
Authentication Protocol (EAP) Key Management Framework",
RFC 5247, DOI 10.17487/RFC5247, August 2008,
<https://www.rfc-editor.org/rfc/rfc5247>.
[FALCON] Fouque, P., Hoffstein, J., Kirchner, P., Lyubashevsky, V.,
Pornin, T., Prest, T., Ricosset, T., Seiler, G., Whyte,
W., and Z. Zhang, "Falcon: Fast-Fourier Lattice-based
Compact Signatures over NTRU", NIST PQC Round 3/4
Submission, 2020, <https://falcon-sign.info/falcon.pdf>.
[FIPS203] National Institute of Standards and Technology, "Module-
Lattice-Based Key-Encapsulation Mechanism Standard",
FIPS 203, August 2024,
<https://csrc.nist.gov/pubs/fips/203/final>.
[FIPS204] National Institute of Standards and Technology, "Module-
Lattice-Based Digital Signature Standard", FIPS 204,
August 2024, <https://csrc.nist.gov/pubs/fips/204/final>.
[FIPS206] National Institute of Standards and Technology, "FN-DSA
(Draft)", FIPS 206 (Draft), 2025,
<https://csrc.nist.gov/pubs/fips/206/ipd>.
[FRONTIERS-PQ-SESSION]
"Design and Implementation of an Authenticated Post-
Quantum Session Protocol", Frontiers in Physics 2025,
DOI 10.3389/fphy.2025.1723966, November 2025,
<https://doi.org/10.3389/fphy.2025.1723966>.
[GAZDAG-IKEV2-PQ]
Gazdag, S., Grundner-Culemann, S., Guggemos, T., Heider,
T., and D. Loebenberger, "A Formal Analysis of IKEv2's
Post-Quantum Extension", ACSAC 2021,
DOI 10.1145/3485832.3485885, December 2021,
<https://doi.org/10.1145/3485832.3485885>.
[HALAK-CORTEX-M0]
Halak, B., "Benchmarking NIST-Standardized ML-KEM and ML-
DSA on ARM Cortex-M0+ (RP2040)", arXiv 2603.19340, 2025,
<https://arxiv.org/abs/2603.19340>.
[HMQV] Krawczyk, H., "HMQV: A High-Performance Secure Diffie-
Hellman Protocol", CRYPTO 2005, IACR ePrint 2005/176,
2005, <https://eprint.iacr.org/2005/176>.
[I-D.celi-wiggers-tls-authkem]
Wiggers, T., Celi, S., Schwabe, P., Stebila, D., and N.
Sullivan, "KEM-based Authentication for TLS 1.3", Work in
Progress, Internet-Draft, draft-celi-wiggers-tls-authkem-
07, 4 May 2026, <https://datatracker.ietf.org/doc/html/
draft-celi-wiggers-tls-authkem-07>.
[I-D.ietf-ipsecme-ikev2-mlkem]
Kampanakis, P., "Post-quantum Key Exchange with ML-KEM in
the Internet Key Exchange Protocol Version 2 (IKEv2)",
Work in Progress, Internet-Draft, draft-ietf-ipsecme-
ikev2-mlkem-05, 14 March 2026,
<https://datatracker.ietf.org/doc/html/draft-ietf-ipsecme-
ikev2-mlkem-05>.
[I-D.uri-lake-pquake]
Blumenthal, U., Luo, B., O'Melia, S., Torres, G., and D.
A. Wilson, "PQuAKE - Post-Quantum Authenticated Key
Exchange", Work in Progress, Internet-Draft, draft-uri-
lake-pquake-00, 22 April 2025,
<https://datatracker.ietf.org/doc/html/draft-uri-lake-
pquake-00>.
[I-D.wang-ipsecme-kem-auth-ikev2]
WANG, G. and V. Smyslov, "KEM-based Authentication for
IKEv2 with Post-quantum Security", Work in Progress,
Internet-Draft, draft-wang-ipsecme-kem-auth-ikev2-03, 2
March 2026, <https://datatracker.ietf.org/doc/html/draft-
wang-ipsecme-kem-auth-ikev2-03>.
[I-D.wiggers-tls-authkem-psk]
Wiggers, T., Celi, S., Schwabe, P., Stebila, D., and N.
Sullivan, "KEM-based pre-shared-key handshakes for TLS
1.3", Work in Progress, Internet-Draft, draft-wiggers-tls-
authkem-psk-05, 4 May 2026,
<https://datatracker.ietf.org/doc/html/draft-wiggers-tls-
authkem-psk-05>.
[KEMTLS] Schwabe, P., Stebila, D., and T. Wiggers, "Post-Quantum
TLS without Handshake Signatures", ACM CCS 2020, IACR
ePrint 2020/534, 2020, <https://ia.cr/2020/534>.
[KEMTLS-PSK]
Schwabe, P., Stebila, D., and T. Wiggers, "More Efficient
KEMTLS with Pre-Shared Keys", ESORICS 2021, IACR
ePrint 2021/779, 2021, <https://ia.cr/2021/779>.
[KEMTLS-TAMARIN]
Celi, S., Hoyland, J., Stebila, D., and T. Wiggers, "A
Tale of Two Models: Formal Verification of KEMTLS in
Tamarin", ESORICS 2022, IACR ePrint 2022/1111, 2022,
<https://ia.cr/2022/1111>.
[KORANGA-PQC-BENCH]
Koranga, A., "Benchmarking Different PQC Libraries",
LinkedIn post, 2025, <https://www.linkedin.com/posts/
aditya-koranga_pqc-cupqc-postquantumcryptography-activity-
7363632983175548929-dkWs/>.
[LIBMCELIECE-SPEED]
Bernstein, D. J., "libmceliece speed table", 6 May 2025,
<https://lib.mceliece.org/speed.html>.
[LIBOQS] Open Quantum Safe, "liboqs", n.d.,
<https://github.com/open-quantum-safe/liboqs>.
[MCELIECE1978]
McEliece, R. J., "A Public-Key Cryptosystem Based On
Algebraic Coding Theory", DSN Progress Report 42-44, JPL,
pp. 114-116, 1978, <https://ipnpr.jpl.nasa.gov/
progress_report2/42-44/44N.PDF>.
[MQV] Law, L., Menezes, A., Qu, M., Solinas, J., and S.
Vanstone, "An Efficient Protocol for Authenticated Key
Agreement", DOI 10.1023/A:1022595222606, 1998,
<https://doi.org/10.1023/A:1022595222606>.
[NIST-SP-800-227]
National Institute of Standards and Technology,
"Recommendation for Key Management: Part 4 - Post-Quantum
Cryptography (Draft)", NIST SP 800-227 (Draft), 2025,
<https://csrc.nist.gov/publications/detail/sp/800-227/
draft>.
[PQ-CRYSTALS-DILITHIUM]
CRYSTALS team, "pq-crystals/dilithium (SUPERCOP,
KabyLake)", n.d.,
<https://github.com/pq-crystals/dilithium>.
[RFC8784] Fluhrer, S., Kampanakis, P., McGrew, D., and V. Smyslov,
"Mixing Preshared Keys in the Internet Key Exchange
Protocol Version 2 (IKEv2) for Post-quantum Security",
RFC 8784, DOI 10.17487/RFC8784, June 2020,
<https://www.rfc-editor.org/rfc/rfc8784>.
[RFC9370] Tjhai, CJ., Tomlinson, M., Bartlett, G., Fluhrer, S., Van
Geest, D., Garcia-Morchon, O., and V. Smyslov, "Multiple
Key Exchanges in the Internet Key Exchange Protocol
Version 2 (IKEv2)", RFC 9370, DOI 10.17487/RFC9370, May
2023, <https://www.rfc-editor.org/rfc/rfc9370>.
[RFC9867] Smyslov, V., "Mixing Preshared Keys in the
IKE_INTERMEDIATE and CREATE_CHILD_SA Exchanges of the
Internet Key Exchange Protocol Version 2 (IKEv2) for Post-
Quantum Security", RFC 9867, DOI 10.17487/RFC9867,
November 2025, <https://www.rfc-editor.org/rfc/rfc9867>.
[SHOR1997] Shor, P. W., "Polynomial-Time Algorithms for Prime
Factorization and Discrete Logarithms on a Quantum
Computer", SIAM J. Comput. vol. 26, no. 5, pp. 1484-1509,
DOI 10.1137/S0097539795293172, 1997,
<https://doi.org/10.1137/S0097539795293172>.
[WIGGERS-THESIS]
Wiggers, T., "Post-Quantum TLS", Ph.D. Thesis, Radboud
University, January 2024,
<https://thomwiggers.nl/publication/thesis/>.
[WOLFSSL-BENCH]
wolfSSL, "wolfSSL Benchmark, Appendix G (Intel x86-64,
AVX2)", n.d.,
<https://www.wolfssl.com/documentation/manuals/wolfssl/
appendix07.html>.
Acknowledgments
The authors want to thank Roger Khazan (MIT/LL), Adam Margetts (MIT/
LL) for reviewing this work and giving helpful suggestions.
Authors' Addresses
Uri Blumenthal
MIT
United States of America
Email: uri@ll.mit.edu
Brandon Luo
MIT
United States of America
Email: brandon.luo@ll.mit.edu
Sean O'Melia
MIT
United States of America
Email: sean.omelia@ll.mit.edu
Gabriel Torres
MIT
United States of America
Email: gabriel.torres@ll.mit.edu
David A. Wilson
MIT
United States of America
Email: david.wilson@ll.mit.edu