专利详情

专利名称	一种安全协议形式化验证方法
申请号	CN201010578947.2	专利类型	发明专利
公开（公告）号	CN102065083A	公开（授权）日	2011.05.18
申请（专利权）人	中国科学院软件研究所	发明（设计）人	薛锐;彭建华;刘峰
主分类号	H04L29/06(2006.01)I	IPC主分类号	H04L29/06(2006.01)I
专利有效期	一种安全协议形式化验证方法至一种安全协议形式化验证方法	法律状态	实质审查的生效
说明书摘要	本发明提供了一种安全协议的形式化验证方法，其步骤包括：1)在设定的网络环境下，给定一个安全协议；2)根据安全协议执行步骤实现的功能对安全协议进行分层；3)将期望的安全目标分解为与各分层对应的子目标；4)依次对各分层进行建模，对各子目标进行描述；5)分别在步骤4)构造的分层模型上验证是否满足与之对应的子目标，若满足则完成对安全协议的验证。本发明的方法将层次式与模型检测方案结合起来，通过将安全协议划分成层次分明的模块分别进行验证，降低了准确建模的复杂性；在不影响验证结果正确性的前提下，极大地削减了检测过程中状态空间的规模。