nach oben

Journal of Cryptographic Engineering

Erschienen in:

01.09.2013 | Special Section on PROOFS workshop

Formal verification of a CRT-RSA implementation against fault attacks

verfasst von: Maria Christofi, Boutheina Chetali, Louis Goubin, David Vigilant

Erschienen in: Journal of Cryptographic Engineering | Ausgabe 3/2013

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Cryptosystems are highly sensitive to physical attacks, which lead security developers to design more and more complex countermeasures. Nonetheless, no proof of flaw absence has been given for any implementation of these countermeasures. This paper aims to formally verify an implementation of one published countermeasure against fault injection attacks. More precisely, the formal verification concerns Vigilant’s CRT-RSA countermeasure which is designed to sufficiently protect CRT-RSA implementations against fault attacks. The goal is to formally verify whether any possible fault injection threatening the pseudo-code is detected by the countermeasure according to a predefined attack model.

Vorheriger Artikel Improved algebraic side-channel attack on AES

Nächster Artikel A formal study of two physical countermeasures against side channel attacks

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Nur mit Berechtigung zugänglich

WHY is a general-purpose verification condition generator, which is used as a back-end by other verification tools and can also be used directly to verify programs. WHY produces verification conditions from annotated programs given as input.

ACSL. http://frama-c.com/acsl.html

Aizatulin, M., Dupressoir, F., Gordon, A.D., Jürjens, J.: Verifying cryptographic code in C: some experience and the Csec challenge. In: Formal Aspects of Security and Trust—8th International Workshop, FAST 2011, Leuven, Belgium, September 12–14, 2011. Revised Selected Papers. Lecture Notes in Computer Science, vol. 7140, pp. 1–20. Springer (2012)

Aumüller, C., Bier, P., Fischer, W., Hofreiter, P., Seifert, J.P.: Fault attacks on RSA with CRT: concrete results and practical countermeasures. In: CHES. Lecture Notes in Computer Science, vol. 2523, pp. 260–275. Springer (2003)

Bar-El, H., Choukri, H., Naccache, D., Tunstall, M., Whelan, C.: The sorcerer’s apprentice guide to fault attacks. IACR Cryptol. ePrint Arch. 2004, 100 (2004)

Berthomé, P., Heydemann, K., Kauffmann-Tourkestansky, X., Lalande, J.F.: Attack model for verification of interval security properties for smart card C codes. In: Proceedings of the 5th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, PLAS ’10, pp. 2:1–2:12. ACM, New York (2010). doi:10.1145/1814217.1814219

Berthomé, P., Heydemann, K., Kauffmann- Tourkestansky, X., Lalande, J.F.: Simulating physical attacks in smart card C codes: the jump attack case. In: e-Smart (2011)

Boneh, D., DeMillo, R.A., Lipton, R.J.: On the importance of eliminating errors in cryptographic computations. J. Cryptol. 14(2), 101–119 (2001)MathSciNetMATHCrossRef

Boscher, A., Naciri, R., Prouff, E.: CRT RSA algorithm protected against fault attacks. In: WISTP. Lecture Notes in Computer Science, vol. 4462, pp. 229–243. Springer, Heraklion (2007)

Butelle, F., Hivert, F., Mayero, M., Toumazet, F.: Formal proof of SCHUR conjugate function. In: AISC/MKM/Calculemus. Lecture Notes in Computer Science, vol. 6167, pp. 158–171. Springer, Berlin (2010)

10.

Chen, H., Dean, D., Wagner, D.: Model checking one million lines of C code. In: NDSS. The Internet Society (2004)

11.

Coron, J.S., Giraud, C., Morin, N., Piret, G., Vigilant, D.: Fault attacks and countermeasures on vigilant’s RSA-CRT algorithm. In: FDTC, pp. 89–96. IEEE Computer Society (2010)

12.

Coron, J.S., Naccache, D., Tibouchi, M.: Fault attacks against emv signatures. In: CT-RSA. Lecture Notes in Computer Science, vol. 5985, pp. 208–220. Springer, San Francisco (2010)

13.

Duprat, S., Gaufillet, P., Lamiel, V.M., Passarello, F.: Formal verification of SAM state machine implementation. In: Embedded Real Time Software and Systems (ERTS’10) (2010)

14.

frama-c. http://frama-c.com/

15.

Giraud, C.: An RSA implementation resistant to fault attacks and to simple power analysis. IEEE Trans. Comput. 55(9), 1116–1120 (2006)CrossRef

16.

Hoare, C.A.R.: An axiomatic basis for computer programming (reprint). Commun. ACM 26(1), 53–56 (1983)MathSciNetCrossRef

17.

Jessie. http://krakatoa.lri.fr#jessie

18.

Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291–314 (2001)MathSciNetMATHCrossRef

19.

Lenstra, A.: Memo on RSA signature generation in the presence of faults (1996). http://infoscience.epfl.ch/record/164524/files.nscan20.PDF

20.

Meola, M.L., Walker, D.: Faulty logic: reasoning about fault tolerant programs. In: Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20–28, 2010. Lecture Notes in Computer Science, vol. 6012, pp. 468–487. Springer, Berlin (2010)

21.

Rivain, M.: Securing RSA against fault analysis by double addition chain exponentiation. IACR Cryptol. ePrint Arch. 2009, 165 (2009)

22.

Shamir, A.: Improved method and apparatus for protecting public key schemes from timing and fault attacks. Patent number WO9852319 (1998)

23.

Vigilant, D.: RSA with CRT: a new cost-effective solution to Thwart fault attacks. In: CHES. Lecture Notes in Computer Science, vol. 5154, pp. 130–145. Springer, Berlin (2008)

24.

Why. http://why.lri.fr/

Titel: Formal verification of a CRT-RSA implementation against fault attacks
verfasst von: Maria Christofi
Boutheina Chetali
Louis Goubin
David Vigilant
Publikationsdatum: 01.09.2013
Verlag: Springer Berlin Heidelberg
Erschienen in: Journal of Cryptographic Engineering / Ausgabe 3/2013
Print ISSN: 2190-8508
Elektronische ISSN: 2190-8516
DOI: https://doi.org/10.1007/s13389-013-0049-3

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner