Transactions on Cryptographic Hardware and Embedded Systems 2026
Testing Security Equivalence in the Random Probing Model
README
Artifact
This artifact contains the source code and the data to reproduce the results as presented in "Testing Security Equivalence in the Random Probing Model" accepted to TCHES 2026, Issue 1.
1. Overview
We provide the verilog files generated by HADES to create secure masked implementations for the first- and second-order of the Present and Skinny 4-bit S-box. We also present the optimized version for each of those implementations. And for each of the aforementioned circuits, we introduced security flaws to create insecure circuits. In addition, we supply the secure implementations for the considered multiplication gadgets in verilog for the first- and second-order.
From those files, we generate and provide the netlist that are processed by VERICA+.
Then, we supply the verification results from VERICA+ in the threshold probing and random probing model for those hardware implementations.
Afterward, we provide the script used to run our superiority and equivalence test to generate the tables and figures in our paper.
Finally, we give license and contact information.
1.1 Naming Convention
The files for the Sboxes are following the naming convention:
[SBOX]_[SEC]_[D]_[GADGET][_OPT]
with
[SBOX]:PresentSBoxorSkinnySBox,[SEC]:Secsecure orInsecinsecure,[D]:1first-order or2second-order,[GADGET]:DOM,HPC1,HPC2orHPC3for the multiplication gadget.[OPT]: add_Optif optimized circuit, otherwise leave blank.
1.2 Structure
We provide an algebraic high-level description of the gadgets, the Present and Skinny 4-bit S-boxes in
./description_circuits.md
with the optimization and injected security flaws.
The implementations .v generated by HADES, along with testbenches, are stored in compressed folders (.zip):
verilog/
Gadget/
PresentSBox/
SkinnySBox/
where PresentSBox and SkinnySBox contain the generic implementation of the gadgets to run the design compiler.
The netlists .v compiled from the previous files are in compressed folders (.zip):
netlist/
Gadget/
PresentSBox/
SkinnySBox/
The verifications results .log from VERICA+ are stored in:
verica/
SkinnySBox/
Order_1/
Order_2/
PresentSBox/
Order_1/
Order_2/
along with the annotation files and the modified random probing verification (without the binomial tree optimization).
2. HADES - Masked Implementations
We contacted the authors of HADES (https://doi.org/10.46586/tches.v2025.i4.1-45) to have a preliminary access to the code.
We could generate the masked implementations of our Sboxes.
We provide as well testbenches to simulate the designs: They are identified by the file name TB_XXX.v.
We would like to give special thanks to Fabian Buschkowski for his support with HADES.
3. Netlists
We compiled the previous designs with Synopsys Design Compiler, using the standard cell library NANG45, to generate the netlists that are input to VERICA+.
4. VERICA+ - Security Verification
We run security verification tests in the threshold probing and random probing model with VERICA+ (See branch VERICA+ in https://github.com/Chair-for-Security-Engineering/VERICA).
The netlists to verify should be put in the folder ./test of VERICA+.
To run the verification, we also give:
- the
ConfigurationRandomProbing.cppfile to replace in./src/analyzer/in order to deactivate the binomial tree optimization, before compiling VERICA+. - the
.jsonfiles to configure the tool for the design to verify, to put in the folder./testof VERICA+ along with the netlist. The path to this file should be changed in.config/verica.jsoninannotation.
Once VERICA+ compiled, run bin/release/verica -c config/verica.json to verify the desired design and the ouput is stored in ./log/verica.log.
5. Tests Script
To run the script testing.R, we use the log files obtained from VERICA+. The script was tested with the version 4.3.0 of R.
It assumes the folder structure given for verica/ in this artifact which are input to the script.
5.1 General Configuration
We precise where to edit or comment/uncomment the lines of the script in general:
- l.569 for the path to the log files,
- l.571 for the path to store the result, saved as
.csvfiles,
5.2 Superiority Testing
For the superiority test:
- l.600-l.676 to uncomment to run the superiority test,
- l.598 and l.601-l.604 to choose the S-box (see
[SBOX]), - l.614 to choose the gadget (see
[GADGET]), - l.617 to choose between the secure or the insecure version of the circuit (see
[SEC]). - l.598 and l.601-l.604 to choose the masking order (see
[D]), - l.659-l.676 outputs the graphic for the superiority test.
Comment: not possible to choose between optimized and non-optimized version, the script always runs for both.
For comparison to STRAPS:
- l.872-l.922 to uncomment to run the comparison to STRAPS,
- l.877 to choose the circuit,
- l.882-l.898 outputs the graphic for the confidence intervals
- l.900-l.922 outputs the graphic for the rejection rates
5.3 Equivalence Testing
For the equivalence test:
- l.679-l.870 to uncomment to run the equivalence test,
- l.681 and l.684-l.687 to choose the S-box (see
[SBOX]), - l.699 to choose the gadget (see
[GADGET]), - l.710 to choose between the secure or the insecure version of the circuit (see
[SEC]). - l.681 and l.684-l.687 to choose the masking order (see
[D]). - l.755-l.812 outputs the graphic for the equivalence test,
- l.817-l.870 produce the tables for cross design comparison,
- l.817-l.819 and l.823-l.824 to change the compared designs.
Comment: not possible to choose between optimized and non-optimized version, the script always runs for both.
6. License and Contact
Please contact Anna Guinet ([email protected]) or Carina Graw ([email protected]) for questions about this artifact.
The files in the folders
verilog/
PresentSBox/DOM/
PresentSBox/HPC1/
SkinnySBox/DOM/
SkinnySBox/HPC1/
follow the license of https://github.com/Chair-for-Security-Engineering/AGEMA/
The files in the folders
verilog/
PresentSBox/HPC2/
PresentSBox/HPC3/
SkinnySBox/HPC2/
SkinnySBox/HPC3/
follow the license of https://github.com/Chair-for-Security-Engineering/HPC3
The verilog .v files in the folder
verilog/
follow the license of https://github.com/Chair-for-Security-Engineering/HADES/
The files in the folder
verica/
follow the license of https://github.com/Chair-for-Security-Engineering/VERICA
The remaining files in this artifact fall under the GNU General Public License version 3 licence (see LICENSE.txt).