This blog post describes our project about the formalization and formal verification of binding properties for KEMs in EasyCrypt. In doing so, it tries to assume as little prior knowledge as possible and explain much of the material from the ground up in an intuitive way.

Here is the story of how we traced a cryptographic vulnerability through a major software supply-chain to uncover a flaw in its identity verification process.

In this blog post, we describe how we at SandboxAQ, together with Cryspen, formally verified key components of Sandwich—an open-source, unified API that simplifies the use of cryptographic libraries for developers, enabling crypto-agility.

This post describes a survey of 20 million public keys from diverse sources on the Internet and cryptographic weaknesses found.

This blogpost describes our investigation and proof of concept to enhance the security of Signal Messenger key management on desktop.

This blogpost serves as a gentle introduction to a widely used security model for analyzing real-world post-quantum cryptosystems, including the recent NIST standards, called the "quantum random oracle model".

This blog post gives an overview of the area of formally verified cryptography and SandboxAQ's activities in this area.

This blog post describes the main idea of each of our three papers that have been accepted at CRYPTO 2024.

This blogpost discusses the Real World PQC workshop we hosted in March 2024 in Toronto, followed by our teams attendance and participation at RSA in May.

This blogpost describes the papers, presentations, and attendees from the SandboxAQ cybersecurity group at the IACR flagship conference Eurocrypt 2024.