Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience

Security proofs for cryptographic systems can be carried out in different models which reflect different kinds of security assumptions. In the symbolic model, an attacker cannot guess a secret at all and can only apply a pre-defined set of operations, whereas in the computational model, he can hope to guess secrets and apply any polynomial-time operation. Security properties in the computational model are more difficult to establish and to check.

In this paper we present a framework for certified proofs of computational indistinguishability, written using the Coq proof assistant, and based on CIL, a specialized logic for computational frames that can be applied to primitives and protocols. We demonstrate how CIL and its Coq-formalization allow proofs beyond the black-box security framework, where an attacker only uses the input/output relation of the system by executing on chosen inputs without having additional information on the state. More specifically, we use it to prove the security of a protocol against a particular kind of side-channel attack which aims at modeling leakage of information caused by an intrusion into Alice and Bob’s computers.