Logics for cryptographic protocols have proved to be of invaluable help in validating and correcting these protocols. However, they are not very helpful to the implementor of these protocols.
It is often difficult to grasp the subtleties of the initial assumptions. Some of them are implicitly imposed by the logic (such as integrity of encrypted messages). Moreover, the idealization process widens the gap between the specification and the implementation even further.
In this paper, we have presented an action-based syntax for the specification of cryptographic protocols, which can be analysed correctly and provides useful guidelines for implementors or even enable automatic generation of code.