Automatic Implementations Synthesis of Secure Protocols and Attacks from Abstract Models
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 pro...
Main Authors: | , , , , |
---|---|
Other Authors: | , , , , , |
Format: | Conference Object |
Language: | English |
Published: |
HAL CCSD
2022
|
Subjects: | |
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 |
Summary: | 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. |
---|