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: 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), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de 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)
• Format: Conference Object
• Language: English
• Published: HAL CCSD 2022
• Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR]; Iceland
• Online Access: https://hal.uca.fr/hal-03835049; https://hal.uca.fr/hal-03835049/document; https://hal.uca.fr/hal-03835049/file/Nordsec_2022_paper_7662.pdf

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.