Automatic implementations synthesis of secure protocols and attacks from abstract models
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...
Main Authors: | , , , , |
---|---|
Other Authors: | , , , , , , , , , |
Format: | Conference Object |
Language: | English |
Published: |
HAL CCSD
2022
|
Subjects: | |
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 |
id |
ftanrparis:oai:HAL:hal-03835049v1 |
---|---|
record_format |
openpolar |
spelling |
ftanrparis:oai:HAL:hal-03835049v1 2024-09-15T18:13:19+00:00 Automatic implementations synthesis of secure protocols and attacks from abstract models Sivelle, Camille Debbah, Lorys Puys, Maxime Lafourcade, Pascal Franco-Rondisson, Thibault 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) Rekyavik, Iceland 2022 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 en eng HAL CCSD info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-031-22295-5_13 hal-03835049 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 doi:10.1007/978-3-031-22295-5_13 info:eu-repo/semantics/OpenAccess Nordic Workshop on Secure IT Systems https://uca.hal.science/hal-03835049 Nordic Workshop on Secure IT Systems, 2022, Rekyavik, Iceland. pp.234-252, ⟨10.1007/978-3-031-22295-5_13⟩ https://link.springer.com/chapter/10.1007/978-3-031-22295-5_13 [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] info:eu-repo/semantics/conferenceObject Conference papers 2022 ftanrparis https://doi.org/10.1007/978-3-031-22295-5_13 2024-09-05T00:06:58Z 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. Conference Object Iceland Reykjavik University Portail HAL-ANR (Agence Nationale de la Recherche) 234 252 |
institution |
Open Polar |
collection |
Portail HAL-ANR (Agence Nationale de la Recherche) |
op_collection_id |
ftanrparis |
language |
English |
topic |
[INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] |
spellingShingle |
[INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] Sivelle, Camille Debbah, Lorys Puys, Maxime Lafourcade, Pascal Franco-Rondisson, Thibault Automatic implementations synthesis of secure protocols and attacks from abstract models |
topic_facet |
[INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] |
description |
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. |
author2 |
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 |
author |
Sivelle, Camille Debbah, Lorys Puys, Maxime Lafourcade, Pascal Franco-Rondisson, Thibault |
author_facet |
Sivelle, Camille Debbah, Lorys Puys, Maxime Lafourcade, Pascal Franco-Rondisson, Thibault |
author_sort |
Sivelle, Camille |
title |
Automatic implementations synthesis of secure protocols and attacks from abstract models |
title_short |
Automatic implementations synthesis of secure protocols and attacks from abstract models |
title_full |
Automatic implementations synthesis of secure protocols and attacks from abstract models |
title_fullStr |
Automatic implementations synthesis of secure protocols and attacks from abstract models |
title_full_unstemmed |
Automatic implementations synthesis of secure protocols and attacks from abstract models |
title_sort |
automatic implementations synthesis of secure protocols and attacks from abstract models |
publisher |
HAL CCSD |
publishDate |
2022 |
url |
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 |
op_coverage |
Rekyavik, Iceland |
genre |
Iceland Reykjavik University |
genre_facet |
Iceland Reykjavik University |
op_source |
Nordic Workshop on Secure IT Systems https://uca.hal.science/hal-03835049 Nordic Workshop on Secure IT Systems, 2022, Rekyavik, Iceland. pp.234-252, ⟨10.1007/978-3-031-22295-5_13⟩ https://link.springer.com/chapter/10.1007/978-3-031-22295-5_13 |
op_relation |
info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-031-22295-5_13 hal-03835049 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 doi:10.1007/978-3-031-22295-5_13 |
op_rights |
info:eu-repo/semantics/OpenAccess |
op_doi |
https://doi.org/10.1007/978-3-031-22295-5_13 |
container_start_page |
234 |
op_container_end_page |
252 |
_version_ |
1810451045124407296 |