位置：立项数据库 > 立项详情页
含代数运算和时间特征的安全协议分析与验证
  • 项目名称：含代数运算和时间特征的安全协议分析与验证
  • 项目类别：重大研究计划
  • 批准号：90604007
  • 申请代码：F0205
  • 项目来源：国家自然科学基金
  • 研究期限：2006-01-01-2008-12-31
  • 项目负责人：李梦君
  • 负责人职称：副教授
  • 依托单位：中国人民解放军国防科学技术大学
  • 批准年度：2006
中文摘要：

安全协议是解决开放互联网络安全问题的最有效手段之一，安全协议的分析与验证是一件十分有意义的研究工作。本课题以含代数运算和时间特征的安全协议作为主要研究对象，具体研究它的建模方法和安全性质的分析与验证方法，需要解决的理论问题有在抽象解释理论框架下安全协议中的时间要素的建模；等式理论合一化问题的合一化算法；约束可满足性问题的求解；逻辑程序的正规逼近问题；设计判定逻辑程序不动点计算是否等停机的近似算法

中文主题词： 代数运算;时间特征;安全协议;形式化方法;可证明安全性理论
成果综合统计
成果类型
数量
  • 期刊论文
  • 会议论文
  • 专利
  • 获奖
  • 著作
  • 25
  • 9
  • 0
  • 0
  • 0
期刊论文
安全协议逻辑程序不停机性快速预测的动态方法
基于Horn 逻辑扩展模型的安全协议反例的自动构造
用描述逻辑进行语义Web服务组合
公钥Kerberos 协议的认证服务过程的建模与验证.
使用组合协议逻辑PCL 验证Amended Needham-Schroeder协议
ACUN理论一般合一化问题的合一化算法
安全协议的进程代数规约到逻辑程序的自动转换
基于Horn 逻辑扩展模型的时间敏感安全协议验证
基于抽象解释理论的程序验证技术
基于动态博弈描述的电子商务协议公平性
安全协议的扩展Horn逻辑模型及其验证方法
基于面向服务架构的网上支付安全体系研究与实现
基于双难题的环Z_n上圆锥曲线的数字签名
安全协议分析中参与者个数上确界的论证
基于Horn逻辑扩展模型的安全协议反例的自动构造
一种基于线索化二叉排序树的数据流挖掘的决策树分类新算法
蛋白质相互作用研究中的计算方法综述
二进制立方形递归网络的拓扑结构
基于Horn逻辑扩展模型的时间敏感安全协议验证
时间敏感的安全协议建模与验证：研究综述
一门新的面向构件语言
会议论文
An abstract and refinement framework for verifying security protocols based on logic programming.
Modeling and Verifying Time Sensitive Security Protocols with Constraints
Constraint Abstract in Verification of Security Protocol
Constraints Solution for Time Sensitive Security Protocols
Local Abstract Verification and Refinement of Security Protocols
A Novel Derivation Framework For Definite Logic Program
Supremum of Agent Number Needed in Analyzing Security Protocols Based on Horn Logic
SPVT-II: An Efficient Security protocol Verifier based on logic programming
A novel fairness property of electronic commerce protocols and its game based formalization
相关项目
状态转换系统的格值量化验证方法研究
期刊论文 9 会议论文 5
基于控制机制的软件可靠性新技术及其理论研究
期刊论文 65
物联网中RFID标签群组通信认证协议和安全体系研究
期刊论文 9 会议论文 3
软件工程学
期刊论文 17 会议论文 16
主动覆盖网络服务体系结构及关键技术的研究
期刊论文 7 会议论文 3 著作 5
基于LFSR序列的公钥密码算法及RSA模数安全分析
期刊论文 7
基于进程代数的电子商务协议形式化研究
期刊论文 16 会议论文 11
基于事件逻辑的安全协议形式化分析及验证
期刊论文 19 获奖 1
面向安全群体通信的新型签密及应用研究
期刊论文 58 会议论文 11 获奖 4 著作 2
李梦君的项目
大规模软件基于抽象解释理论的时序性质验证及支持工具
期刊论文 9 会议论文 6
大规模软件验证若干关键技术研究及支持工具