论文部分内容阅读
提出一种能对安全协议进行分析的自动化验证机制。提出需求的概念,认为需求是攻击者未知但又对攻击者合成目标项至关重要的知识集合,并建立了以需求为中心的攻击者模型;设计一种以攻击者为中心的状态搜索方式,按需添加协议会话实例,为避免新增协议会话实例引起攻击者推理出现时序矛盾,引入回溯机制以确保状态转移过程中攻击者知识能正确增长。实验表明,该系统能正确验证协议的安全性,状态空间数目略优于Scyther工具。