Paper 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.
Note: This paper will appear as is in the PROOFS 2013 workshop informal preproceedings.
Metadata
- Available format(s)
- Category
- Implementation
- Publication info
- Preprint. MINOR revision.
- Keywords
- RSACRTfault injectionBellCoRe attackformal proofOCaml
- Contact author(s)
- rauzy @ enst fr
- History
- 2014-01-30: last of 4 revisions
- 2013-08-17: received
- See all versions
- Short URL
- https://ia.cr/2013/506
- License
-
CC BY