Cryptographic Reductions By Bi-Deduction
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…
