Communication protocol is the cornerstone of today's network system. The correctness and security of a protocol rely on both a flawless specification and a faithful implementation. While prevalent work focuses on validating the soundness of specification, implementations are inherently more complicated and might introduce vulnerabilities. Existing protocol testing solutions for security purposes depend heavily on expert insights of protocols and manual efforts, and could hardly be generalized or automated. Formal methods have been proved promising toward developing automated and generic protocol verification and testing methods. This thesis studies a model based formal approach for testing security related properties for communication protocol systems. A formal protocol model: Symbolic Parameterized Extended Finite State Machine (SP-EFSM) is proposed that that augments the traditional communicating EFSM model with a symbolic protocol message language and parameterized input and output symbols in order to cope with the rich semantics of modern protocol with cryptographic primitives. A protocol is specified by a set of communicating SP-EFSM and various verification problems could be rigorously using this formal model.
The power of the proposed model is demonstrated by its application to several newly emerging and interesting problems related to protocol security and reliability. This thesis shows that the formal modeling techniques could contribute to solutions that are fundamentally more general and automatic. For the problem of black box testing of message confidentiality (a.k.a. secrecy) a supervised FSM learning approach is used to discover the internal structure of black-box implementations by active testing and to validate the confidentiality property on-the-fly. For the problem of protocol fingerprinting, SP-EFSM model is used to record the distinguishing structural aspects of an implementation based on which a complete taxonomy of fingerprint matching and discovery problems is formulated. This thesis also evaluates the feasibility of using SP-EFSM model in practice. In the test generation module of a real world virtual security testbed, it is integrated as the mechanism to specify sophisticated features of a security device. Abstract test sequences with high fault coverage are automatically generated and translated into executable test cases, providing a plausible alternative to the traditional scheme of manual test design.