Hacspec

Cryspen @ VSTTE 2024

Karthik gave an invited talk on High Assurance Post-Quantum Cryptography at VSTTE 2024.

Verified Software: Theories, Tools, and Experiments is a conference that aims to advance the state of the art in software verification. At VSTTE 2024 in Prague, Karthik spoke about how formal …

Cryspen @ Crypto 2024

Karthik gave an invited talk on Formal Methods for Cryptography at Crypto 2024.

Crypto is the top international conference on cryptography and is held every year (since 1981) in Santa Barbara, California. This year, Crypto invited Karthikeyan Bhargavan, our Chief Research …

Cryspen @ FMCP 2024

We gave a talk at the NIST workshop on Formal Methods within Certification Programs.

The US National Institute of Standards and Technology (NIST) publishes a number of important cryptographic standards (including upcoming ones for post-quantum cryptography), and runs the cryptographic …

Unlocking New Possibilities

Cryspen partners with SandboxAQ to accelerate hax adoption

We have been developing the hax toolchain over the last two years, in collaboration with research teams at Inria and the University of Aarhus. To showcase its capabilities we have successfully applied …

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 …

/images/posts/pexels-egor-kamelev-751689.jpeg

Specifying Oblivious Pseudonymization

An executable hacspec specification of ScrambleDB, a utility-preserving pseudonymization system using convertible PRFs for oblivious data linking.

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. Find …

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 …

/images/posts/rwc-karthik-franziskus.jpeg

Cryspen @ RWC 2023

Cryspen’s Real World Crypto 2023 talk in Tokyo on the hacspec language, the hax tool, and the libcrux cryptographic library.

At Real World Crypto 2023 in Tokyo, we gave a talk on the hacspec language, the hax tool, and the libcrux crypto library. Designing and implementing cryptographic software is a perilous endeavor. …

An Executable HPKE Specification

The first executable specification of HPKE (RFC 9180), written in hacspec as an annotated companion to the RFC for implementers.

HPKE, published as RFC 9180, describes a scheme for hybrid public key encryption. 📚 Read our TL;DR on HPKE if you need more background on HPKE. In this post, I describe the first executable HPKE …