2023/08/28 by Faezeh Nasrabadi, Nasrabadi, Faezeh, Robert Künnemann +3 · 1 citation
Computer Science · #Advanced Authentication Protocols Security #Cryptographic Implementations and Security #Cryptography and Security (cs.CR) #FOS: Computer and information sciences #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.2308.14450
openalex publication_date 2023/08/28 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.