SSMCI:以攻击者为中心的安全协议验证机制

摘要

提出一种能对安全协议进行分析的自动化验证机制.提出需求的概念,认为需求是攻击者未知但又对攻击者合成目标项至关重要的知识集合,并建立了以需求为中心的攻击者模型;设计一种以攻击者为中心的状态搜索方式,按需添加协议会话实例,为避免新增协议会话实例引起攻击者推理出现时序矛盾,引入回溯机制以确保状态转移过程中攻击者知识能正确增长.实验表明,该系统能正确验证协议的安全性,状态空间数目略优于Scyther工具.%A automatic verification mechanism for security protocols analysis was proposed. The attacker model was proposed and the concept of 'need' was defined, a knowledge set which was necessary for the attacker to compose a tar-get message term but unknown to the attacker. The attacker model was established as needed. The mechanism centered on the attacker was designed, in which whether add a protocol session was determined by the attacker. This might cause contradiction in time sequence, so some back-track algorithm was adopted to solve this contradiction. Experiments show that the system can verify the security of the protocol, and the number of state space is slightly better than the Scyther tool.