含代数运算和时间特征的安全协议分析与验证
批准号：
90604007
项目类别：
重大研究计划
资助金额：
28.0 万元
负责人：
李梦君
依托单位：
学科分类：
计算机图像视频处理与多媒体技术
结题年份：
2008
批准年份：
2006
项目状态：
已结题
项目参与者：
李梦君、刘锋、刘万伟、张玲、周倜
项目摘要
结项摘要
项目成果
李梦君的其他基金
相似基金
相关文献
中文摘要
安全协议是解决开放互联网络安全问题的最有效手段之一，安全协议的分析与验证是一件十分有意义的研究工作。本课题以含代数运算和时间特征的安全协议作为主要研究对象，具体研究它的建模方法和安全性质的分析与验证方法，需要解决的理论问题有：在抽象解释理论框架下安全协议中的时间要素的建模；等式理论合一化问题的合一化算法；约束可满足性问题的求解；逻辑程序的正规逼近问题；设计判定逻辑程序不动点计算是否等停机的近似算法
英文摘要
期刊论文列表
专著列表
科研奖励列表
会议论文列表
专利列表
登录
查看更多内容
DOI：
--
发表时间：
--
期刊：
周倜，李梦君，李舟军，陈火旺，安全协议的进程代数规约到逻辑程序的自动转换，《计算机工程与科学》，2006，28(1)，22-24
影响因子：
--
作者：
[]
通讯作者：
DOI：
--
发表时间：
--
期刊：
软件学报
影响因子：
--
作者：
[王杰生, 李梦君, 李舟军]
通讯作者：
李舟军
DOI：
--
发表时间：
--
期刊：
周倜, 李梦君, 李舟军. 公钥Kerberos 协议的认证服务过程的建模与验证.计算机工程与科学, 2008, 30(11).
影响因子：
--
作者：
[]
通讯作者：
DOI：
--
发表时间：
--
期刊：
李梦君，王桢珍，李舟军，陈火旺，ACUN理论一般合一化问题的合一化算法，《计算机工程与科学》，2006,28(5),71-75
影响因子：
--
作者：
[]
通讯作者：
DOI：
--
发表时间：
--
期刊：
李梦君，李舟军，陈火旺，安全协议的扩展Horn逻辑模型及其验证方法，《计算机学报》，2006，29(9):1666-1678
影响因子：
--
作者：
[]
通讯作者：
共 10 条
大规模软件验证若干关键技术研究及支持工具
-
批准号：61672525
-
项目类别：面上项目
-
资助金额：62.0万元
-
批准年份：2016
-
负责人：李梦君
-
依托单位：
大规模软件基于抽象解释理论的时序性质验证及支持工具
-
批准号：60703075
-
项目类别：青年科学基金项目
-
资助金额：18.0万元
-
批准年份：2007
-
负责人：李梦君
-
依托单位：
国内基金
海外基金