Automatic implementations synthesis of secure protocols and attacks from abstract models

• Main Authors: Sivelle, Camille, Debbah, Lorys, Puys, Maxime, Lafourcade, Pascal, Franco-Rondisson, Thibault
• Other Authors: Département Systèmes (DSYS), Commissariat à l'énergie atomique et aux énergies alternatives - Laboratoire d'Electronique et de Technologie de l'Information (CEA-LETI), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne (UCA)-Institut national polytechnique Clermont Auvergne (INP Clermont Auvergne), Université Clermont Auvergne (UCA)-Université Clermont Auvergne (UCA), CYBERALPS, ANR-15-IDEX-0002,UGA,IDEX UGA(2015)
• Format: Conference Object
• Language: English
• Published: HAL CCSD 2022
• Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR]; Iceland; Reykjavik University
• Online Access: https://uca.hal.science/hal-03835049; https://uca.hal.science/hal-03835049/document; https://uca.hal.science/hal-03835049/file/Nordsec_2022_paper_7662.pdf; https://doi.org/10.1007/978-3-031-22295-5_13

NordSec 2022 : The 27th Nordic Conference on Secure IT System, 30 November 2022 - 02 December 2022 | Reykjavik University, Iceland International audience Attack generation from an abstract model of a protocol is not an easy task. We present BIFROST (Bifrost Implements Formally Reliable prOtocols for Security and Trust), a tool that takes an abstract model of a cryptographic protocol and outputs an implementation in C of the protocol and either a proof in ProVerif that the protocol is safe or an implementation of the attack found. We use FS2PV, KaRaMeL, ProVerif and a dedicated parser to analyze the attack traces produced by ProVerif. If an attack is found then BIFROST automatically produces C code for each honest participant and for the intruder in order to mount the attack.