Documentation
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 https://eprint.iacr.org/2016/270 for more details about the tool.
Overview
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.