CISPA
Browse
cispa_all_4016.pdf (1.17 MB)

CryptoBap: A Binary Analysis Platform for Cryptographic Protocols

Download (1.17 MB)
conference contribution
posted on 2024-03-05, 12:19 authored by Faezeh NasrabadiFaezeh Nasrabadi, Robert KünnemannRobert Künnemann, Hamed Nemati
We introduce CryptoBap, a platform to verify weak secrecy and authentication for the (ARMv8 and RISC-V) machine code of cryptographic protocols. We achieve this by first transpiling the binary of protocols into an intermediate representation and then performing a crypto-aware symbolic execution to automatically extract a model of the protocol that represents all its execution paths. Our symbolic execution resolves indirect jumps and supports bounded loops using the loop-summarization technique, which we fully automate. The extracted model is then translated into models amenable to automated verification via ProVerif and CryptoVerif using a third-party toolchain. We prove the soundness of the proposed approach and used CryptoBap to verify multiple case studies ranging from toy examples to real-world protocols, TinySSH, an implementation of SSH, and WireGaurd, a modern VPN protocol.

History

Preferred Citation

Faezeh Nasrabadi, Robert Künnemann, Hamed Nemati. CryptoBap: A Binary Analysis Platform for Cryptographic Protocols. In: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (CCS). 2023.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

ACM Conference on Computer and Communications Security (CCS)

Legacy Posted Date

2023-08-29

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_4016, author = {Faezeh Nasrabadi AND Robert Künnemann AND Hamed Nemati}, title = {CryptoBap: A Binary Analysis Platform for Cryptographic Protocols}, booktitle = {Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (CCS)}, year = {2023} }

Usage metrics

    Categories

    No categories selected

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC