Cryspen’s Approach to TLS: A Critical Analysis

This is the fourth installment in our series examining Cryspen’s cryptographic libraries. Over the past month, we have disclosed eleven vulnerabilities spanning post-quantum key encapsulation, digital signatures, hybrid public key encryption, and the formally verified F* specifications underlying them. We now turn to Cryspen’s TLS implementations: rustls-libcrux, a cryptographic provider for rustls; Bertie, a standalone TLS 1.3 implementation that has been the subject of formal verification research; and libcrux-iot, an embedded-targeted fork of libcrux. Across these three projects, we found five more bugs, bringing the total to sixteen—including a signature verification function that rejects 75% of valid signatures, encryption that silently drops its authentication tag, a TLS client that performs no certificate validation, remote denial-of-service vectors, and a FIPS 204 parameter that is off by a factor of eight.

How Cryspen Handled our Disclosures

Before presenting our new findings, we document how Cryspen responded to our previous vulnerability disclosures.

In January 2026, we began our audit work and opened our first issue on Cryspen’s GitHub (#1299). It was professional and submitted in good faith. When Cryspen’s team responded, we acknowledged that their perspective was legitimate, closed the issue cooperatively, and moved on.

We then submitted four pull requests with tested fixes for security vulnerabilities, including a critical nonce reuse bug in hpke-rs (PR #117, PR #118) and issues in libcrux (PR #1315, PR #1316). These were submitted in the same professional manner as contributions from other external researchers such as Filippo Valsorda and “GuuJiang,” whom Cryspen had publicly thanked for their reports.

Cryspen’s response to our contributions was markedly different:

• They closed all four of our pull requests.
• They publicly accused us of “putting the community at risk” and called our disclosures “irresponsible.”
• They blocked us from their GitHub organization, preventing us from submitting any further issues or pull requests.
• They then copied our fixes and applied them without credit, after blocking us and closing the PRs.
• They published security advisories that downplayed severity and obscured impact—classifying our critical nonce reuse vulnerability as “medium severity” and describing fixes with vague labels like “fix context counter” and “avoid panic on AEADError” rather than honestly explaining the vulnerabilities and their impact.
• To date, no RustSec advisories exist for their most severe vulnerabilities.

The GitHub block had an immediate practical consequence: we discovered it when attempting to submit our fifth fix, a patch for an AES-GCM denial-of-service crash in libcrux-psq. That fix remains available on our fork but could never be submitted upstream.

We offered to continue disclosing our remaining findings, including those being revealed here today, as GitHub pull requests complete with tested fixes provided on the day of disclosure. Cryspen declined, and then accused us of not giving them time to address vulnerabilities before public disclosure—despite the fact that it was Cryspen who blocked our ability to submit fixes, after we had already disclosed four bugs complete with tested patches, free of charge.

To be clear: after we submitted our initial four bug disclosures with tested fixes, we were blocked by Cryspen from submitting additional fixes, something we discovered when trying to submit our fifth fix. In spite of this, Cryspen accused us of not giving them time to fix the bugs we were disclosing.

While Cryspen described our disclosures as “irresponsible” and “putting the community at risk”, we posit that it is their active lobbying to get their cryptographic libraries merged in production into Signal, Google and OpenMLS’s stacks, despite their being aware of, and at times openly admitting their immaturity, that constitute irresponsible behavior. Furthermore, Cryspen has often acted to downplay the severity of bugs that were found to impact applications such as Signal in production, and to this day has not issued complete or appropriate advisories for their most severe, critical vulnerabilities.

Cryspen’s own Code of Conduct commits to “accepting responsibility and apologizing to those affected by our mistakes, and learning from the experience” and “focusing on what is best not just for us as individuals, but for the overall community.” We leave it to the reader to judge whether Cryspen’s handling of our disclosures lived up to these principles.

Findings

Over the past month, we have published eleven vulnerabilities across Cryspen’s cryptographic libraries, spanning post-quantum key encapsulation, digital signatures, and hybrid public key encryption. Our findings included bugs in formally verified F* specifications, false proofs accepted by a build system that defaults to not checking them, and unproven axioms that render entire proof infrastructures unsound.

We now expand our scope to Cryspen’s TLS implementations. Cryspen maintains two: rustls-libcrux, a cryptographic provider for the rustls TLS library backed by libcrux primitives, and Bertie, a standalone TLS 1.3 implementation. We also examined libcrux-iot, Cryspen’s embedded-targeted fork of libcrux designed for constrained IoT devices.

Across these three projects, we found five new bugs: a signature verification function that rejects approximately 75% of valid ECDSA P-256 signatures, a TLS 1.2 encryption path that silently drops the authentication tag—eliminating all integrity protection—a TLS 1.3 client that performs no certificate chain validation or hostname verification, remote denial-of-service vectors exploitable with a single malformed handshake message, and a FIPS 204 parameter that is off by a factor of eight.

rustls-libcrux

The rustls-libcrux project provides a CryptoProvider implementation for the rustls TLS library, replacing rustls’s default cryptographic backend with Cryspen’s libcrux. It implements signature verification, AEAD encryption and decryption, key exchange, and RSA signing—the cryptographic foundation that the TLS protocol depends on for authentication, confidentiality, and integrity.

Finding 1: ECDSA P-256 Verification Rejects ~75% of Valid Signatures

File: libcrux-provider/src/verify.rs, lines 57–70.

The ECDSA P-256 signature verification code extracts the r and s components from a DER-encoded signature and converts them to fixed-size 32-byte arrays:

let r: [u8; 32] = sig.r.as_bytes().try_into().map_err(|_| InvalidSignature)?;
let s: [u8; 32] = sig.s.as_bytes().try_into().map_err(|_| InvalidSignature)?;

The sig.r and sig.s values are der::asn1::Int types. The Int::as_bytes() method returns the raw DER value bytes, which include a leading 0x00 sign byte when the most significant bit of the integer is set. This is how DER encodes positive integers: if the MSB would otherwise indicate a negative number, a 0x00 byte is prepended.

For ECDSA P-256, r and s are 32-byte unsigned scalars. When the MSB is set—which occurs with approximately 50% probability for each scalar—DER encoding prepends 0x00, making as_bytes() return 33 bytes. The try_into::<[u8; 32]>() conversion then fails with a length mismatch, and the signature is rejected as invalid.

The probability that at least one of r or s has its MSB set is 1 - 0.5 × 0.5 = 75%. Three out of every four valid ECDSA P-256 signatures will be rejected by this code.

This is the primary signature scheme for TLS 1.3 server authentication. A rustls client using the libcrux provider will fail to complete TLS handshakes with approximately 75% of servers, because the server’s valid certificate signature will be incorrectly rejected.

Finding 2: TLS 1.2 Encryption Drops Authentication Tag

File: libcrux-provider/src/aead.rs, lines 161–163.

The TLS 1.2 MessageEncrypter implementation discards the AEAD authentication tag:

libcrux::aead::encrypt(&self.0, payload.as_mut(), iv, &aad)
    .map_err(|_| rustls::Error::EncryptError)
    .map(|_| OutboundOpaqueMessage::new(m.typ, m.version, payload))
//       ^^^ tag discarded

The libcrux::aead::encrypt() function returns the authentication tag as a separate value. The TLS 1.3 code path handles this correctly, appending the tag to the ciphertext:

.map(|tag| {
    payload.extend_from_slice(tag.as_ref());
    OutboundOpaqueMessage::new(m.typ, m.version, payload)
})

The TLS 1.2 path captures the tag as _ and drops it. The resulting TLS record contains only ciphertext with no integrity protection. The receiving peer will fail to decrypt because it expects a 16-byte authentication tag appended to the ciphertext, and the connection will fail.

This is not a subtle vulnerability. Authenticated encryption without the authentication tag is just encryption—the entire integrity guarantee of the TLS record layer is eliminated. The fix is one line: append the tag, exactly as the TLS 1.3 path already does.

Bertie

Bertie is Cryspen’s standalone TLS 1.3 implementation, written in Rust. It is described as a “minimal, low-level TLS 1.3 implementation” and has been the subject of formal verification research. Unlike rustls-libcrux, which delegates protocol logic to rustls, Bertie implements the TLS 1.3 handshake and record layer from scratch.

Finding 3: No Certificate Chain Validation or Hostname Verification

Files: src/tls13cert.rs, lines 356–373; src/tls13handshake.rs, lines 318–331.

Bertie’s TLS 1.3 client accepts any certificate whose public key produces a valid CertificateVerify signature over the handshake transcript. No other validation is performed:

• No certificate chain validation (issuer signature verification)
• No hostname or SNI matching against Subject CN or Subject Alternative Name
• No validity period checking (expiration or not-before dates)
• No certificate extension validation (BasicConstraints, KeyUsage)
• No revocation checking (CRL or OCSP)
• No trust anchor verification (root CA store)

The verification_key_from_cert() function at tls13cert.rs:356 parses a certificate by skipping version, serial number, signature algorithm, issuer, validity, and subject fields—extracting only the SubjectPublicKeyInfo. The server_name stored in ServerPubInfo is populated during the handshake but never compared against any field in the certificate.

The handshake function put_server_signature() at tls13handshake.rs:318 extracts the public key using verification_key_from_cert() and verifies the CertificateVerify signature over the transcript. If the signature is valid, the handshake proceeds. The certificate itself is never examined.

An attacker can present a self-signed certificate for any domain—or a certificate with no domain at all—and Bertie will accept it, provided the CertificateVerify signature is valid with respect to the key in that certificate. This completely defeats server authentication. The attacker does not need to compromise a certificate authority, exploit a parsing vulnerability, or perform any cryptographic attack. They simply generate a key pair, create a self-signed certificate, and present it.

This is not a missing feature in an early prototype. Certificate validation is the mechanism by which TLS clients distinguish legitimate servers from imposters. Without it, the encrypted channel provides confidentiality against passive observers but no authentication whatsoever—the client cannot know who it is talking to.

Finding 4: Remote Denial of Service via .unwrap() in KEM Operations

File: src/tls13crypto.rs, lines 710, 750, 752.

Three .unwrap() calls on fallible decode() results will crash the process if given malformed key material:

// Line 710 — server-side, processes client's key_share
let pk = PublicKey::decode(alg.libcrux_kem_algorithm()?, &pk.declassify()).unwrap();

// Line 750 — client-side, processes server's key_share
let sk = PrivateKey::decode(librux_algorithm, &sk.declassify()).unwrap();

// Line 752 — client-side
let ct = Ct::decode(librux_algorithm, &ct).unwrap();

A remote attacker can crash a Bertie server by sending a ClientHello with a malformed key_share extension. The malformed public key bytes reach kem_encap() at tls13handshake.rs:620, where PublicKey::decode().unwrap() panics. Similarly, a malicious server can crash a Bertie client by sending a ServerHello with a malformed key_share, reaching kem_decap() at tls13handshake.rs:243.

This is a single-packet denial of service. No handshake completion is required. No authentication is needed. One malformed message crashes the process.

The fix is mechanical: replace .unwrap() with .map_err(|_| CRYPTO_ERROR)?. The correct error-handling pattern is used elsewhere in the same file.

libcrux-iot

libcrux-iot is Cryspen’s embedded-targeted fork of libcrux, designed for constrained IoT devices. It implements ML-KEM (FIPS 203), ML-DSA (FIPS 204), and SHA-3 (FIPS 202), with C code extracted via the Eurydice toolchain for deployment on bare-metal platforms.

Finding 5: ML-DSA Pre-Hash Uses Wrong Output Length

Files: ml-dsa/src/pre_hash.rs, line 40; ml-dsa/src/ml_dsa_44.rs, line 121; ml-dsa/src/ml_dsa_65.rs, line 134; ml-dsa/src/ml_dsa_87.rs, line 121.

FIPS 204 Table 2 specifies that the SHAKE-128 pre-hash output length for HashML-DSA is 256 bytes (2048 bits). The module docstring correctly states this:

//! pre-hash trait for SHAKE-128, with a digest length of 256 bytes.

But the implementation allocates a 32-byte buffer and asserts this size:

// pre_hash.rs:40
debug_assert_eq!(output.len(), 32);

All call sites allocate 32-byte buffers:

// ml_dsa_44.rs:121, ml_dsa_65.rs:134, ml_dsa_87.rs:121
let mut pre_hash_buffer = [0u8.classify(); 32];

This is not an edge case—the pre-hash output length is a fundamental parameter of the HashML-DSA mode. SHAKE-128 at 32 bytes produces a different digest than SHAKE-128 at 256 bytes. Signatures produced by this implementation using the sign_pre_hashed_shake128 API will not verify against any FIPS 204-compliant implementation that uses the correct 256-byte output, and vice versa.

The bug is present in the upstream cryspen/libcrux as well, indicating it was inherited rather than introduced during the IoT fork. The pre-hashed NIST KAT files were generated by the same codebase, so they cannot detect the discrepancy. ACVP test vectors do not cover the HashML-DSA mode.

Pure ML-DSA signing and verification—the default and most commonly used mode—is unaffected. Only the sign_pre_hashed_shake128 and verify_pre_hashed_shake128 APIs are impacted.

The Scope of the Problem

These five findings bring the total to sixteen bugs across Cryspen’s cryptographic ecosystem in one month. The pattern we have documented extends beyond any single library.

In libcrux, we found wrong F* specifications, false proofs, and unsound axioms. In hpke-rs, we found nonce reuse and broken forward secrecy. In rustls-libcrux, we find that TLS 1.3 connections will fail 75% of the time and TLS 1.2 encryption drops its authentication tag. In Bertie, we find a TLS implementation that does not validate certificates. In libcrux-iot, we find FIPS non-compliance in a post-quantum signature parameter.

The rustls-libcrux findings are particularly instructive. This is a cryptographic provider—its entire purpose is to correctly implement a small set of well-specified cryptographic operations for a well-tested TLS library. The operations are standard: ECDSA verification, AEAD encryption and decryption. The specifications are unambiguous. And yet the implementation rejects 75% of valid ECDSA signatures and drops authentication tags. These are not subtle corner cases. They are the primary code paths.

Bertie’s missing certificate validation is harder to characterize charitably. Certificate chain validation is not an optional feature of TLS. It is the mechanism by which a client determines whether the server is who it claims to be. A TLS 1.3 implementation that omits this check has not implemented TLS in any meaningful sense—it has implemented an encrypted channel to an unknown party.

The fact that Bertie has been the subject of formal verification research makes this omission more concerning, not less. The verification effort focused on the handshake protocol’s cryptographic properties while the most basic authentication mechanism was absent. This is verification theatre in its purest form: proving properties of a protocol that cannot authenticate its peer.

Across sixteen findings in six Cryspen projects, the pattern is consistent. The verified core is surrounded by an unverified periphery where basic engineering discipline is absent. The specifications that the verified code is checked against are themselves wrong. The build system defaults to not checking proofs. And the marketing claims make no distinction between what has been verified and what has not.

Formal verification is a tool. Like any tool, its value depends on how it is applied. When it is applied selectively, communicated imprecisely, and used to justify claims that the evidence does not support, it becomes something worse than useless: it becomes a source of false confidence. Users who trust “formally verified” to mean “safe to deploy” will deploy code that rejects valid signatures, drops authentication tags, and accepts certificates from anyone.