基于进程代数的复杂安全协议的形式化分析与验证-东篱科研大数据发现系统（DRDS）

位置：立项数据库 > 立项详情页

基于进程代数的复杂安全协议的形式化分析与验证

项目名称：基于进程代数的复杂安全协议的形式化分析与验证
项目类别：面上项目
批准号：60473057
申请代码：F020201
项目来源：国家自然科学基金
研究期限：2005-01-01-2007-12-31

项目负责人：李舟军
负责人职称：教授
依托单位：中国人民解放军国防科学技术大学
批准年度：2004

中文摘要：

安全协议的缺陷是导致网络安全问题的重要原因之一.安全协议的形式化分析与验证技术能全面深入地检测安全协议中的细微漏洞,被实践证明是一条确保协议正确性的重要途径.复杂安全协议指被广泛实用于Internet的大型安全协议,如Kerberos5协议、TLS协议、IPSec协议及电子商务协议等.本课题以复杂安全协议作为研究对象,以进程代数作为基本工具,研究适合于对复杂安全协议进行验证的安全协议建模方法、安全性质的刻画方法、安全协议的验证方法及验证的优化方法、基于构件的复杂安全协议的设计和分析方法,以及实现一个能够对复杂安全协议进行自动分析和验证的工具.本课题的研究有助于提高和保证包括电子商务在内的各种网上应用的安全性.

中文主题词：复杂安全协议;进程代数;形式化验证;

英文摘要：

Complex Security Protocol; Pro

英文主题词： Complex Security Protocol; Pro

结论摘要：

安全协议的形式化分析与验证技术能全面深入地检测安全协议中的细微漏洞,被实践证明是确保协议正确的重要途径. 本课题以复杂安全协议作为研究对象,以进程代数作为基本工具,重点研究了适合于对复杂安全协议进行验证的安全协议建模方法、安全性质的刻画方法、安全协议的验证方法及验证的优化方法,设计并实现一个能够对复杂安全协议进行自动分析和验证的工具。主要的研究成果包括基于扩展Horn逻辑的安全协议模型，安全协议反例的自动构造算法，安全协议基于抽象解释理论的验证方法，电子代币支付协议的建模与验证方法。本课题的研究有助于提高和保证包括电子商务在内的各种网上应用的安全性.

成果综合统计