/images/posts/hpke_spec.png
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 …

/images/posts/tldr-hpke.jpg
TL;DR - Hybrid Public Key Encryption

A new standard for public key encryption

HPKE, defined in RFC 9180, is a CFRG standard that describes a scheme for hybrid public key encryption. It is co-authored by my Cryspen co-founder Karthikeyan Bhargavan and one of his PhD students …

/images/posts/erc-cover.jpg
Cryspen ERC PoC Grant

Karthik Bhargavan wins an ERC Proof of Concept grant to commercialise formal verification research through Cryspen.

Cryspen co-founder Karthik Bhargavan got awarded an ERC Proof of Concept grant for commercialising the know-how and landmark research results from his Inria research group PROSECCO through Cryspen. …