The Formosa Crypto project federates multiple projects in machine-checked cryptography and high-assurance cryptographic engineering under a single banner, to better support developers and users.
Join us on Zulip.
Formosa News
-
libjade release 2022.12.0 (December 5, 2022)
The first version of libjade is available. Read the announcement.
-
Jasmin release 2022.09.0 (October 3, 2022)
A new version of Jasmin is available. Read the announcement.
-
Jasmin lecture in Nancy (July 7, 2022)
During the Cyber in Nancy summer school, Vincent Laporte and Benjamin Grégoire gave a lecture on Jasmin.
-
Jasmin compiler in the opam repository (June 28, 2022)
The Jasmin compiler can be installed using the opam package manager. Learn how.
-
EasyCrypt and Jasmin tutorial in Šibenik (June 7, 2022)
Manuel Barbosa will be giving a tutorial on machine-checked cryptography in EasyCrypt and Jasmin at the Summer School on Real-World Crypto and Privacy in Šibenik, Croatia, on June 16th. More details and links to material.
-
Jasmin release 2022.04.0 (May 6, 2022)
A new version of the Jasmin compiler is available. Read the announcement.
Formosa Projects
- EasyCrypt — Project Website — Project Repository
EasyCrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code. Its main application is the construction and verification of game-based cryptographic proofs.
- Jasmin — Project Website — Project Repository
Jasmin is a workbench for high-assurance and high-speed cryptography. Jasmin implementations aim at being efficient, safe, correct, and secure.
- Libjade — Project Website — Project Repository
Libjade is a cryptographic library written in jasmin, with computer-verified proof of correctness and security in EasyCrypt. The primary focus of libjade is to offer high-assurance software implementations of post-quantum crypto primitives.
Formosa People
-
Adrien Koutsos (Inria Paris)
-
Alley Stoughton (Boston University)
-
Andreas Hülsing (Eindhoven University of Technology)
-
Basavesh Ammanaghatta Shivakumar (Max Planck Institute for Security and Privacy)
-
Benjamin Grégoire (Inria Sophia-Antipolis Méditerranée)
-
François Dupressoir (University of Bristol)
-
Gilles Barthe (Max Planck Institute for Security and Privacy & IMDEA Software Institute)
-
Jean-Christophe Léchenet (Inria Sophia-Antipolis Méditerranée)
-
José Bacelar Almeida (Universidade do Minho & HASLab/INESC TEC)
-
Manuel Barbosa (Universidade do Porto & HASLab/INESC TEC)
-
Miguel Quaresma (Max Planck Institute for Security and Privacy)
-
Peter Schwabe (Max Planck Institute for Security and Privacy & Radboud University)
-
Pierre-Yves Strub (Meta)
-
Tiago Oliveira (Max Planck Institute for Security and Privacy)
-
Vincent Laporte (Inria)
Formosa Supporters
Formosa and its component projects are supported by a variety of funders and
institutions. We gratefully acknowledge their support, including historical
support for the founding projects.