Please use this identifier to cite or link to this item:
|Title:||Formal verification of a CRT-RSA implementation against fault attacks||Authors:||Christofi, Maria Dolores
|Major Field of Science:||Medical and Health Sciences||Field Category:||Basic Medicine||Keywords:||Countermeasures;Cryptographic implementation;Fault attacks;Formal verification;Frama-C;RSA-CRT||Issue Date:||15-Feb-2013||Source:||Journal of Cryptographic Engineering, 2013, vol. 3, pp. 157-167||Volume:||3||Start page:||157||End page:||167||Journal:||Journal of Cryptographic Engineering||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. © 2013 Springer-Verlag Berlin Heidelberg.||ISSN:||2190-8508||DOI:||10.1007/s13389-013-0049-3||Rights:||© Springer||Type:||Article||Affiliation :||Gemalto
Versailles Saint-Quentin-en-Yvelines University
|Appears in Collections:||Άρθρα/Articles|
checked on Jul 25, 2021
checked on Aug 2, 2021
Items in KTISIS are protected by copyright, with all rights reserved, unless otherwise indicated.