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 
Chetali, Boutheïna 
Goubin, Louis 
Vigilant, David 
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

CORE Recommender
Show full item record


checked on Jul 25, 2021

Page view(s)

Last Week
Last month
checked on Aug 2, 2021

Google ScholarTM



Items in KTISIS are protected by copyright, with all rights reserved, unless otherwise indicated.