中文摘要：

认证性建立通信双方的信任关系,是安全通信的重要保障.传统的协议测试方法只关注协议功能的正确性,无法满足认证性等安全属性测试的要求.因此,提出了一种针对协议认证性的安全属性测试方法,利用带目标集合的有限状态机模型SPG-EFSM来扩展描述协议安全属性,并在攻击场景分类的基础上设计了认证攻击算法.通过攻击算法找到了Woo-lam协议和μTESLA协议的认证性漏洞,该方法具有可行性、覆盖率高等特点.

英文摘要：

Authentication builds the trust relationship between communication parties, which is a magnitude guarantee for secure communications. However, existing protocol testing techniques focus on validating the protocol specification. Those techniques can not satisfy the requirements of testing protocol authentication as their lack of the method for describing security properties. Therefore, a protocol security property testing method is proposed for testing protocol authentication. This testing method uses a new formal model-Symbolic Parameterized Goal Extended Finite State Machine （SPG-EFSM） for de- scribing protocols and their security properties. Then, a protocol attack algorithm is designed for testing protocol authentica- tion based on different attack scenarios. Through test experiments on the well-known protocol Woo-lam and μTESLA, it is found that the SPG-EFSM based attack algorithm can find several protocol security flaws and has better feasibility and high coverage.