基于SPIN和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) convention tool to generate testcases 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. The result indicates that our method is effective and efficient.