Artifact for "Foundations for Cryptographic Reductions in CCSA Logics"
David Baelde, Adrien Koutsos, Justine Sauvage · HAL (Le Centre pour la Communication Scientifique Directe) · 2024
Artifact for the CCS 2024 paper "Foundations for Cryptographic Reductions in CCSA Logics".The Computationally Complete Symbolic Attacker (CCSA) approach to securityprotocol verification relies on probabilistic logics to reason about theinteraction traces between a protocol and an arbitrary adversary. The proofassistant Squirrel implements one such logic. CCSA logics come withcryptographic axioms whose soundness derives from the security of standardcryptographic games, e.g. PRF, EUF, IND-CCA. Unfortunately, these axioms arecomplex to design and implement; so far, these tasks are manual, ad hoc anderror-prone. We solve these issues by providing a formal and systematic methodfor deriving axioms from cryptographic games. Our method relies onsynthesizing an adversary against some cryptographic game, through the notionof bi-deduction. Concretely, we define a rich notion of bi-deduction, justifyhow to use it to derive cryptographic axioms, provide a proof system forbi-deduction, and an automatic proof-search method which we implemented inSquirrel.