欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
分析了Bruno Blanchet和Martin Abadi提出的基于Horn逻辑的安全协议模型及其验证方法，针对它们构造不满足安全性质的安全协议反例的不足，提出了安全协议的扩展Horn逻辑模型和修改版本的安全协议验证方法，使得能够从安全协议的扩展Horn逻辑模型和修改版本的安全协议验证过程中自动构造不满足安全性质的安全协议反例．在基于函数式编程语言Objective Carol开发的安全协议验证工具SPVT中，实现了上述算法，验证了算法的正确性．
英文摘要：
Based on analyzing and pointing out the limitations for constructing counter-examples of the security protocol＇s Horn logic model and its verification method proposed by Bruno Blanchet and Martin Abadi, the security protocol＇s extended Horn logic model and the modifiedversion verification method are presented such that the counter-examples are able to be constructed from them automatically. In the authors＇ verifier SPVT developed based on the functional programming language Objective Caml, these algorithms are implemented and their correctness are proved.
同期刊论文项目
同项目期刊论文
期刊信息
位置：