Cryptographic protocol conformance testing based on domain-specific state machine

We present a method of conformance testing of the cryptographic protocol implementations that ensures a high degree of automation of the testing process and provides criteria for the quality assessment of the generated test suites. Our method is based on a kind of extended (non-finite) state machine which is specifically designed for the domain of cryptographic protocols. The key concept of the proposed machine is a built-in mechanism of sequences, which, firstly, sets an effective way to deal with the nondeterminism inherent in cryptographic protocols and, secondly, provides the means to express "inconvenient" (for the high-level declarative languages) requirements, such as e.g. "take the concatenation of the specified parts of all the previous messages which meet specified condition". Basing on this machine, we propose a high-level declarative language (embedded in Haskell) intended for development of interoperable protocol specifications used as input data for our testing tool. The protocol specification consists of two parts: a description of the structure of the protocol messages (this part, by virtue of its conciseness and declarativeness, can be directly incorporated in the primary specifications such as RFC) and a set of state machine transition functions binded to the sequences. In the paper, we present the principles of building of our machine and introduce the notion of sequences fuzzing. The proposed approach was successfully approved for the industrial cryptographic protocol TLS.