New paper accepted for ACM CCS 2026
A new paper, “Automated Reasoning for Indistinguishability in the CCSA,” co-authored by Laura Kovács, key researcher at SBA Research and full professor at the Faculty of Informatics of the Vienna University of Technology (TU Wien), and Matteo Maffei, key researcher at SBA Research and Professor at TU Wien, has been accepted for presentation at the 33rd ACM Conference on Computer and Communications Security (CCS).
The 33rd ACM CCS will take place from November 15–19, 2026, at The World Forum in The Hague, Netherlands.
Title of the paper
Automated Reasoning for Indistinguishability in the CCSA
Abstract
Cryptographic protocols are the foundation of secure digital communication, yet their design remains error-prone, as evidenced by the vulnerabilities that have plagued even the most widely adopted protocols throughout history. Security properties are typically formalized using either trace properties or indistinguishability, each addressing distinct security guarantees, such as agreement and authenticity for the former and anonymity and strong secrecy for the latter. Formal verification of cryptographic protocols spans both symbolic and computational models. While symbolic techniques enable automation and scalability, they do not provide computational security guarantees. Computational models, though robust, are harder to formalize and automate. Recent advances, such as the Computationally Complete Symbolic Attacker (CCSA) model and its logic, the Bana-Comon Logic (BC Logic), bridge this gap by supporting both trace properties and indistinguishability. How ever, despite significant progress in proof assistants, automating indistinguishability remains a challenge due to its combination of unstructured equality theories, complex non-classical calculus, and partially inductive reasoning—all requiring expert knowledge in both cryptography and logic.
This paper introduces a novel approach to automate indistinguishability proofs in the CCSA model, implemented in the automated prover CRYPTOVAMPIRE2. We extend CRYPTOVAMPIRE to support indistinguishability by designing GOLGGE, a PROLOG-inspired backtracking engine over equality graphs (e-graphs), which provides strong, rewrite-driven equational reasoning capabilities. We adapt the BC Logic rules to this new framework, yielding semantically compatible statements. The effectiveness of our approach is demonstrated by automating all indistinguishability goals in the SQUIRREL repository.
Authors: Simon Jeanteur, Laura Kovács, Matteo Maffei, Michael Rawson
Links
Photocredit: Luiza Puiu, TU Wien