A Higher-Order Indistinguishability Logic for Cryptographic Reasoning

The field of cryptographic protocol verification in the computational model aims at obtaining formal security proofs of protocols. To facilitate writing such proofs, which are complex and hard to automate, Bana and Comon have proposed the Computationally Complete Symbolic Attacker (CCSA) approach, which is based on a first-order logic with a probabilistic computational semantics. Later, a meta-logic was built on top of the CCSA logic, to extend it with support for unbounded protocols and effective mechanisation. This meta-logic was then implemented in the SQUIRREL prover.

In this paper, we propose a careful re-design of the SQUIRREL logic, providing clean and robust foundations for its future development. We show in this way that the original meta-logic was both needlessly complex and too restrictive. Our new, higherorder logic avoids the indirect definition of the meta-logic on top of the CCSA logic, decouples the logic from the notion of protocol, and supports advanced generic reasoning and non-computable functions. We also equip it with generalised cryptographic rules to reason about corruption. This theoretical work justifies our extension of SQUIRREL with higher-order reasoning, which we illustrate on case studies.

global goal hybrid [ α ] (N 1 : int) (t l , tr : int → α) (z : α) : const(N 1 ) ⇒ ( ∀ (N 0 : int), const(N 0 ) ⇒ [ N 0 ≤ N 1 ] ⇒ ( z, λ(i:int). if i < N 0 then t l i else z ∼ z, λ(i:int). if i < N 0 then tr i else z ) ⇒ ( z, (λ(i:int). if i < N 0 then t l i else z), t l N 0 ∼ z, (λ(i:int). if i < N 0 then tr i else z), tr N 0 )) ⇒ ( z, λ(i:int). if i ≤ N 1 then t l i else z ∼ z, λ(i:int). if i ≤ N 1 then tr i else z ).