Cryptology ePrint Archive: Report 2013/506

A Formal Proof of Countermeasures against Fault Injection Attacks on CRT-RSA

Pablo Rauzy and Sylvain Guilley

Abstract: In this article, we describe a methodology that aims at either breaking or proving the security of CRT-RSA algorithms against fault injection attacks. In the specific case-study of BellCoRe attacks, our work bridges a gap between formal proofs and implementation-level attacks. We apply our results to three versions of CRT-RSA, namely the naive one, that of Shamir, and that of Aumüller et al. Our findings are that many attacks are possible on both the naive and the Shamir implementations, while the implementation of Aumüller et al. is resistant to all fault attacks with one fault. However, we show that the countermeasure is not minimal, since two tests out of seven are redundant and can simply be removed.

Category / Keywords: implementation / RSA, CRT, fault injection, BellCoRe attack, formal proof, OCaml

Date: received 16 Aug 2013

Contact author: rauzy at enst fr

Available format(s): PDF | BibTeX Citation

Note: This paper will appear as is in the PROOFS 2013 workshop informal preproceedings.

Version: 20130817:204627 (All versions of this report)

Short URL:

Discussion forum: Show discussion | Start new discussion

[ Cryptology ePrint archive ]