In this presentation, we are interested in the Computationally Complete Symbolic Attack (CCSA) approach to security protocol verification, and its implementation in the proof assistant SQUIRREL.
The proof of a protocol relies on assumptions on the security provided by its primitives (e.g. hash, encryption, etc.), which are generally formulated in terms of indistinguishability of games.
Adding such assumptions to the CCSA logic and SQUIRREL is notably difficult, error prone and time-consuming task: it requires manual work for each assumption (axioms design, proof of correctness, implementation).
To solve these issues, we designed an extended notion of bideduction and associate to it a proof system that allows to prove reduction of arbitrary CCSA formulas to arbitrary games indistinguishability, by proving the existence of a witness program for the reduction. This work comes with the implementation of a proof-search procedure, encapsulated into one tactic in SQUIRREL.
