Affiliations: LSV, ENS Cachan, CNRS, INRIA, Cachan, France
Correspondence:
[*]
Corresponding author: Jean Goubault-Larrecq, LSV, ENS Cachan, CNRS, INRIA, 61 avenue du président Wilson, 94230 Cachan, France. Tel.: +33 1 47 40 75 68; Fax: +33 1 47 40 75 21; E-mail: [email protected].
Abstract: First-order logic models of security for cryptographic protocols, based on variants of the Dolev–Yao model, are now well-established tools. Given that we have checked a given security protocol π using a given first-order prover, how hard is it to extract a formally checkable proof of it, as required in, e.g., common criteria at the highest evaluation level (EAL7)? We demonstrate that this is surprisingly hard in the general case: the problem is non-recursive. Nonetheless, we show that we can instead extract finite models M from a set S of clauses representing π, automatically, and give two ways of doing so. We then define a model-checker testing M⊧S, and show how we can instrument it to output a formally checkable proof, e.g., in Coq. Experience on a number of protocols shows that this is practical, and that even complex (secure) protocols modulo equational theories have small finite models, making our approach suitable.