Cryptographic protocol verification with hax

This blog post details an example of how to use our hax toolchain for verifying the security of cryptographic protocol implementations written in Rust.

Conference Talks

We have been travelling the world to talk about our recent work

Cryspen attended a number of conference in April and March. Here is a list of all slides and videos. We will update links when more resources become available.

Post-Quantum OpenMLS

Get started with post-quantum secure end-to-end encrypted with OpenMLS.

OpenMLS now offers security against harvest-now-decrypt-later (HNDL) quantum adversaries. In #1546 we merged support for the X-Wing KEM draft, which is an early draft for securely combining …

Post-Quantum Group Messaging

Get post-quantum security for end-to-end encrypted messaging with MLS.

With multiple post-quantum cryptographic algorithms (ML-KEM, ML-DSA) nearing standardization, enterprises, research groups, and standards bodies have started investigating what post-quantum secure …

Verifying Libcrux's ML-KEM

How we verified our Rust ML-KEM implementation in libcrux using hax and F*

In a recent blog post, we described Cryspen’s new Rust implementation of ML-KEM in Rust, and talked about how our high-assurance development methodology helped us find a new timing bug in …

Verified ML-KEM (Kyber) in Rust

We implemented ML-KEM in Rust and formally verified its correctness with hax

ML-KEM, previously known as Kyber, is the first post-quantum secure key-encapsulation mechanism (KEM) to get standardised by NIST in FIPS 203. Cryspen has built a new high assurance Rust …

Welcome Jan & Lucas

📢 Exciting News! Cryspen is thrilled to announce the addition of two exceptional minds to our team: Dr. Lucas Franceschino and Jan Winkelmann.

An Analysis of Signal's PQXDH

A comprehensive, machine-checked, post-quantum security proof of the Signal PQXDH protocol.

Signal recently published a new, post-quantum secure, version of their X3DH protocol called PQXDH. As with any new cryptographic protocol, it is important to precisely analyse its security …

Announcing Campus Cyber Circus Project

Cryspen partners with Inria to build a new integrated development and verification environment

🎉 We’re excited to announce that Cryspen partnered with Inria on a transfer project to build a new integrated development and verification environment (IDVE). The project is part of the transfer …