In this tutorial, you will learn how to use the GGA-Unbounded tool. This tool is designed to perform automated proofs of pairing-based cryptographic constructions in Generic Group Model. If you haven't done it yet, you should read the Introduction section to get an intuition of what the tool is for.
We refer to our paper for more details about the tool.


This tutorial consists of three chapters:
  • Chapter 1: Example:
    In this chapter we analyze a small example, to show how to translate a security experiment into polyomial constraints.

  • Chapter 2: Specifying security experiments:
    The description of the cryptographic constructions and the security experiment are given to the tool through an input file. In this chapter, we describe the syntax for input files.

  • Chapter 3: Proving security:
    In this chapter we describe the rules that are implemented in the tool and allow you to prove that the constraints derived from the input file are infeasible and thus, your construction is secure.




Detailed installation instructions can be found on the project webpage in the file or in the Get Started section.