finja

The finja (Fault INJection Analysis) tool is being developed as part of my PhD work. It helps me to formally analyze some kinds of fault injection attacks and countermeasures against them. It uses modular arithmetic as a framework since it was first developped to analyze BellCoRe attacks on CRT-RSA computations.

The source code is released under CeCILL license and is available here.

Installation and usage instructions can be found in the README file.

Results

The original work which lead to the developement of finja has been described in my paper A Formal Proof of Countermeasures Against Fault Injection Attacks on CRT-RSA, which was presented at PROOFS 2013; an extended version was published in the Journal of Cryptographic Engineering.

Since then, finja has been improved and used to continue my work on countermeasures against fault injection attacks, which gave birth to two other papers: Formal Analysis of CRT-RSA Vigilant's Countermeasure Against the BellCoRe Attack, in PPREW 2014; and Countermeasures Against High-Order Fault-Injection Attacks on CRT-RSA, in FDTC 2014.

In addition, finja has been used by other researchers to analyse another family of countermeasures, spawning yet another publication: Algorithmic Countermeasures Against Fault Attacks and Power Analysis for RSA-CRT, in COSADE 2016.