International Association for Cryptologic Research
In the authors' paper at PROOFS 2013, they formally studied a few known countermeasures to protect CRT- RSA against the BellCoRe fault injection attack. However, they left vigilant's countermeasure and its alleged repaired version by the researcher as future work, because the arithmetical framework of their tool was not sufficiently powerful. In this paper they bridge this gap and then use the same methodology to formally study both versions of the counter-measure. They obtain surprising results, which they believe demonstrate the importance of formal analysis in the field of implementation security.