tightPROVE is a formal verification tool for the tight probing security of masked implementations.
tightPROVE was introduced in the following publication:
Tight Private Circuits: Achieving Probing Security with the Least Refreshing
By Sonia Belaïd, Dahmun Goudarzi, and Matthieu Rivain.
In the proceedings of ASIACRYPT 2018.
This repository contains the code of tightPROVE implemented in SageMath:
- tightPROVE.sage
and a few examples of input files:
- example1.txt: the circuit corresponding to example 1 in the publication;
- example2.txt: the circuit corresponding to example 2 in the publication;
- example3.txt: the circuit corresponding to example 2 augmented with a refresh gadget;
- aes.txt: the AES s-box circuit considered in the publication.
Using the tool requires having SageMath installed (v6.10 or higher). Then simply run the following command line:
sage tightPROVE.sage file.txt
where file.txt is the input circuit file.
The input circuit format is as follows. Each line represents an operation or refresh gadget with the syntax
xor i jfor a Boolean addition gadget,and i jfor a Boolean multiplication gadget,ref ifor a refresh gadget,
where i and j are the indexes of the two operands, i.e., the output of operations from the i-th and j-th lines.
The inputs of the circuit are represented at the top of the file as
in 0
in 1
...