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 …

Specifying Oblivious Pseudonymization

In this blog post we announce an executable specification in the hacspec specification language for the ScrambleDB pseudonymization system, developed by Cryspen as part of the BMBF ATLAS project.

Internet Defense Prize 2023

Cryspen co-founders win Usenix Security prizes

At the 32nd Usenix Security Symposium in Anaheim CA, a paper on the Messaging Layer Security Protocol, co-authored by our founders Jonathan Protzenko and Karthikeyan Bhargavan, was awarded both the …

Prairie and Atlas

Privacy-Preserving Data Analysis at Cryspen

With the widespread adoption and deployment of machine learning across enterprises, ever-increasing amounts of data are being collected, stored, communicated, combined, and computed over by …