You are looking at a specific version 20140130:172147 of this paper. See the latest version.

Paper 2013/810

Formal Analysis of CRT-RSA Vigilant's Countermeasure Against the BellCoRe Attack

Pablo Rauzy and Sylvain Guilley

Abstract

In our paper at PROOFS 2013, we formally studied a few known countermeasures to protect CRT-RSA against the BellCoRe fault injection attack. However, we left Vigilant's countermeasure and its alleged repaired version by Coron et al. as future work, because the arithmetical framework of our tool was not sufficiently powerful. In this paper we bridge this gap and then use the same methodology to formally study both versions of the countermeasure. We obtain surprising results, which we believe demonstrate the importance of formal analysis in the field of implementation security. Indeed, the original version of Vigilant's countermeasure is actually broken, but not as much as Coron et al. thought it was. As a consequence, the repaired version they proposed can be simplified. It can actually be simplified even further as two of the nine modular verifications happen to be unnecessary. Fortunately, we could formally prove the simplified repaired version to be resistant to the BellCoRe attack, which was considered a "challenging issue" by the authors of the countermeasure themselves.

Note: This is the final version of the paper, submitted here for self-archiving (green Open Access) under Creative Commons Attribution 4.0 International License.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Published elsewhere. ACM SIGPLAN on Program Protection and Reverse Engineering Workshop 2014
DOI
10.1145/2556464.2556466
Keywords
RSACRTfault injectionBellCoRe attackformal proofOCaml
Contact author(s)
rauzy @ enst fr
History
2014-05-22: last of 5 revisions
2013-12-06: received
See all versions
Short URL
https://ia.cr/2013/810
License
Creative Commons Attribution
CC BY
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.