A formal language for primary specifications of the cryptographic protocols

Use of the formal methods in the development of the protocol implementations improves the quality of these implementations. The greatest benefit would result from the formalizing of the primary specifications usually contained in the RFC documents. This paper proposes a formal language for primary specifications of the cryptographic protocols, which aims at fulfilling (in a higher degree than in the existing approaches) the conditions required from primary specifications: they have to be concise, declarative, expressive, unambiguous and executable; in addition, the tools supporting the language have to provide the possibility of automatic deriving of the high quality test suites from the specifications. The proposed language is based on a machine (dubbed the C2-machine) specifically designed for the domain of the cryptographic protocols. Protocol specification is defined as a program of the C2-machine. This program consists of two parts: the definition of the protocol packets and the definition of the non-deterministic behavior of the protocol parties. One execution of the program simulates one run of the protocol. All the traces, which can be potentially produced by such execution, by definition, comprise all conformant traces of the protocol; in other words, the program of the C2-machine defines the operational contract of the protocol. In the paper, to make the design and operational principles of the C2-machine easier to understand, two abstractions of the C2-machine are presented: C0-machine and C1-machine. C0-machine is used to explain the approach taken in expressing non-determinism of the protocols. The abstraction level of the C1-machine (which is a refinement of C0-machine) is enough to define the semantics of the basic C2-machine instructions. To enhance the readability of the programs and to reach the level of declarativeness and conciseness of the formalized notations used in some of conventional RFCs (e.g. TLS RFCs), C2-machine implements some syntactic tricks on top of the basic instructions. To use C2-specifications in the black-box testing, the special form of the C2-machine (C2-machine with excluded role) is presented. Throughout the paper the proposed concepts are illustrated by examples from the TLS protocol.