Protocol Security Testing with SPIN and TTCN-3

Protocol security testing is an important technique to ensure the security of communication protocols. However, methods considering both effective detection to specification vulnerabilities and efficient testing on protocol implementations are not well developed. In this paper, we present a general method for protocol security testing including protocol verification with SPIN model checker and protocol testing with formal testing language TTCN-3. We use threat model to model malicious entities and import the classification of information security to achieve a complete analysis of security requirements for protocol verification. We also develop a SPIN Trail to TTCN-3(st2ttcn) conversion tool to generate test cases automatically from counter examples obtained from model checking. As a case study, we apply our approach to the security testing of Source Address Validation Improvements (SAVI) protocol. We test two versions of SAVI-DHCP protocol. Security vulnerabilities have been found and tested in corresponding implementations.