Refinement-based Verification of Cryptographic Protocols with Quantitative Values

Cryptographic protocols are notoriously hard to design and analyse, giving meaning to analysers such as Tamarin or ProVerif conducting automatic verification in a symbolic model of cryptography. While those tools handle many real-world protocols, they lack support when security relies on quantitative constraints. Examples include time-sensitive protocols, that are crucial for achieving fairness in the presence of a dishonest majority, e.g., to realise fair exchanges.

We present a technique for verifying cryptographic protocols involving critical quantitative features such as timeouts or timelocks. It builds upon existing qualitative analysers as black boxes, to verify a quantitative model through Counter-Example-Guided Abstraction Refinement (CEGAR). It first generates a sound approximated model for the symbolic analyser, checks the potential attack trace it produces, and refines the approximated model based on false alarms. We demonstrate the feasibility of this approach through a fully automated tool using the Tamarin prover as a backend.

Using our tool, we analyse multiple protocols achieving fairness through timed cryptography, e.g., coin flipping or fair signing. Further, we study atomic swap protocols, which enable the exchange of cryptocurrencies among mutually distrusting users. Even though these protocols have been extensively studied in the literature and deployed, our tool identified multiple subtle attack vectors that undermine their security and enable attackers to steal funds.