An OCaml implementation of the PlonK proving system, enhanced with techniques for proof aggregation. Developed by the Cryptography Team at Nomadic Labs. See our research paper.

A tool for fully automated synthesis of indifferentiability attacks, developed as part of this research project.

A prototype implementation of a contingent payments protocol, which leverages a cryptocurrency system to realize secure fair-exchange of information. See our paper.

A prototype implementation of our constructions of multi-authority controlled-functional encryption for quadratic functions from this paper. Unfortunately, the implementation is not open-source.

A proof-of-concept implementation of attribute-based encryption in the framework of predicate encodings and pair encodings. See our paper.

The Generic Group Model Symbolic Solver is an extension of the Generic Group Analyzer Unbounded that handles polynomial divisions in the exponent.

The Generic Group Analyzer Unbounded is a tool for automated analysis of cryptographic constructions and assumptions in the generic group model.