| 主权项 |
一种基于漏洞攻击的安全协议验证方法，其特征是采用注入攻击实现对安全协议漏洞的验证，步骤包括：1)对安全协议的会话数据类型的建立数据类型映射模式，创建进程状态变迁规则，实现对安全协议的建模，并确认安全协议的一致性目标；所述建模的内容包括二个部分，一部分是安全协议中使用到的数据类型，另一部分即是表述安全协议交互过程的进程状态变迁规则；建模的过程：首先对安全协议的非形式化表述中的会话数据类型进行确认，并采用递归函数实现对会话数据映射形成的数据模式表述数据类型；进程状态变迁规则是由进程状态发生变迁时所需满足的条件约束、进程状态变迁过程中的实参替代变量的替代集、以及表述协议当前状态、变迁后状态的谓词来组成的；通过变迁规则与协议交互数据类型结合来建立安全协议的模型；2)生成安全协议会话空间：包括生成安全协议参与者、和参与者掌握的知识集合以及安全协议攻击者掌握的知识集合；3)对安全协议会话空间中执行的会话，生成注入消息求解目标，来实现对求解目标的解析，形成求解目标逻辑表达式；4)对求解目标逻辑表达式中的每个子式，生成求解数据集，由求解目标子式和求解数据集生成求解域；5)判断当前求解域所位于的求解路径；若当前求解域所位于的求解路径上存在其它求解域，并且其它求解域与当前求解域具备相似求解域关系，则终止当前求解域求解，直接进入步骤7)，反之进入步骤6)；6)对当前求解域，调用模型校验技术中的基于约束求解算法，实现递归方式的求解；7)若步骤6)中求解成功，则表示攻击者采用求解的会话消息已注入被攻击会话，此时判断被攻击的安全协议会话的进程状态是否为结束，若不是结束，则回到步骤4)，求解下一个会话消息；若会话的进程状态为结束，则进入步骤8)；8)分析攻击者的注入攻击是否造成安全协议一致性目标的破坏，若是则说明发现安全协议的漏洞，对安全协议实现了验证。 |
