Cryptographic stack machine notation one

A worthy cryptographic protocol specification has to be human-readable (declarative and concise), executable and formally verified in a sound model. Keeping in mind these requirements, we present a protocol message definition notation named CMN.1, which is based on an abstraction named cryptographic stack machine. The paper presents the syntax and semantics of CMN.1 and the principles of implementation of the CMN.1-based executable protocol specification language. The core language library (the engine) performs all the message processing, whereas a specification should only provide the declarative definitions of the messages. If an outcoming message must be formed, the engine takes the CMN.1 definition as input and produces the binary data in consistency with it. When an incoming message is received, the engine verifies the binary data with respect to the given CMN.1 definition memorizing all the information needed in the further actions. The verification is complete: the engine decrypts the ciphertexts, checks the message authentication codes and signatures, etc. Currently, the author's proof-of-concept implementation of the language (embedded in Haskell) can translate a CMN.1-based specifications both to the interoperable implementations and to the programs for the ProVerif protocol analyzer. The excerpts from the CMN.1-based TLS protocol specification and corresponding automatically generated ProVerif program are provided as an illustration.