Logics for cryptographic protocols have proved very useful in
validating the correctness of these protocols. However,
neither the specification, nor the logic proof help the implementor
of the protocol. Although the proof states the assumptions explicitly,
it does not ---in general--- contain guidelines for the implementation.
In this paper, we present a theorem prover whose input is very close
to a program written in a procedural language. Moreover, explicit
guidelines for implementors may be given.
