Tidy: Symbolic Verification of Timed Cryptographic Protocols
Gilles Barthe, Ugo Dal Lago, Giulio Malavolta, Itsaka Rakotonirina · Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security · 2022
Timed cryptography refers to cryptographic primitives designed to meet their security goals only for a short (polynomial) amount of time. Popular examples include timed commitments and verifiable delay functions. Such primitives are commonly used to guarantee fairness in multiparty protocols ("either none or all parties obtain the output of the protocol'') without relying on any trusted party. Despite their recent surge in popularity, timed cryptographic protocols remain out of scope of current symbolic verification tools, which idealise cryptographic primitives as algebraic operations, and thus do not consider fine-grained notions of time.