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 pi 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 evaluation level 7? We demonstrate that this is surprisingly hard: the problem is non-recursive in general. On the practical side, we show how we can extract finite models M from a set S of clauses representing pi, automatically, in two ways. 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. This was implemented in the h1 tool suite. Experience on a number of protocols shows that this is practical.