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

• Swarn Priya defends her PhD (November 27, 2023)
  

  Swarn Priya defended her PhD on November 22, 2023. Learn more.

• Swarn Priya wins L’Oréal-UNESCO 2023 prize (October 9, 2023)
  

  Swarn Priya won the L’Oréal-UNESCO “Pour les Femmes et la Science” Young Talents France 2023 Award. Read more.

• Jasmin release 2023.06.1 (July 31, 2023)
  

  A new minor version of Jasmin is available. Read the announcement.

• Jasmin release 2023.06.0 (June 9, 2023)
  

  A new major version of Jasmin is available. Read the announcement.

• Jasmin release 2022.09.3 (May 31, 2023)
  

  A new minor version of Jasmin is available. Read the announcement.

• Jasmin release 2022.09.2 (April 14, 2023)
  

  A new minor version of Jasmin is available. Read the announcement.

• 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. More details and links to material.

• 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, centre de 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, centre d’Université Côte d’Azur)

• Chitchanok Chuengsatiansup (The University of Melbourne, Australia)

• Christian Doczkal (Max Planck Institute for Security and Privacy)

• Denis Firsov (Taltech & Guardtime)

• Fabio Campos (RheinMain University of Applied Sciences & Radboud University)

• François Dupressoir (University of Bristol)

• Gilles Barthe (Max Planck Institute for Security and Privacy & IMDEA Software Institute)

• Jean-Christophe Léchenet (Inria, centre d’Université Côte d’Azur)

• José Bacelar Almeida (Universidade do Minho & HASLab/INESC TEC)

• Kai-Chun Ning (Max Planck Institute for Security and Privacy)

• Lionel Blatter (Max Planck Institute for Security and Privacy)

• Manuel Barbosa (Universidade do Porto & HASLab/INESC TEC)

• Matthias Meijers (Eindhoven University of Technology (TU/e))

• Miguel Quaresma (Max Planck Institute for Security and Privacy)

• Peter Schwabe (Max Planck Institute for Security and Privacy & Radboud University)

• Pierre-Yves Strub (PQShield)

• Rui Fernandes (Max Planck Institute for Security and Privacy)

• Santiago Arranz Olmos (Max Planck Institute for Security and Privacy)

• Swarn Priya (Inria, centre d’Université Côte d’Azur)

• Tiago Oliveira (Max Planck Institute for Security and Privacy)

• Vincent Hwang (Max Planck Institute for Security and Privacy)

• Vincent Laporte (Inria, centre de l’Université de Lorraine)

• Yuval Yarom (Ruhr University Bochum)

Formosa Affiliations and Supporters

Formosa and its component projects are supported by a variety of funders and institutions. Our active members work for the following institutions.

In addition, other institutions support, and have supported Formosa or its constituent projects financially. We gratefully acknowledge their support.