-
题名基于树语言逼近的安全协议形式化分析
被引量:1
- 1
-
-
作者
刘楠
朱文也
祝跃飞
陈晨
-
机构
信息工程大学信息工程学院
-
出处
《计算机科学》
CSCD
北大核心
2010年第1期176-180,共5页
-
基金
国家高技术研究发展计划(863)(2007AA01Z471)资助
-
文摘
利用形式化方法或工具自动化分析实用安全协议十分必要,定理证明技术因其可解决无限状态系统的验证备受关注,但扩展其验证规模和自动化实现时仍然存在一些局限性。以定理证明和重写逼近理论为基础,以项重写形式化定义协议模型,以树自动机模拟协议攻击者知识集,给出攻击者知识集可达项逼近求解的算法,并根据上述模型讨论秘密性和认证性的验证方法,最后以Needham-Schroeder公钥认证协议为例验证模型的有效性,并指出下一步研究方向。
-
关键词
安全协议
项重写
树自动机
树语言
逼近
秘密性
认证性
-
Keywords
Security protocol, TRS, Tree automata, Tree language, Approximation, Secrecy, Authentication
-
分类号
TP309
[自动化与计算机技术—计算机系统结构]
-
-
题名一种对MSR模型的新扩展
被引量:1
- 2
-
-
作者
陈晨
朱文也
陈卫红
刘楠
-
机构
信息工程大学信息工程学院
-
出处
《计算机工程》
CAS
CSCD
北大核心
2010年第8期138-140,共3页
-
基金
国家"863"计划基金资助项目(2007AA01Z471)
-
文摘
作为安全协议形式化建模方法之一的多集重写(MSR)模型虽然提供了基本的理论框架,但并不完善。针对其在类型攻击检测方面的不足,对原模型进行改进,扩展类型内容,丰富推演规则,使其能检测特定类型的攻击。给出安全属性的描述,并用实例验证扩展后的MSR模型中交换协议的非否认性和公平性。
-
关键词
多集重写模型
安全协议
非否认性
公平性
-
Keywords
MultiSet Rewriting(MSR) model
security protocol
non-repudiation
fairness
-
分类号
TP309
[自动化与计算机技术—计算机系统结构]
-
-
题名TA4SP的认证性扩展
- 3
-
-
作者
朱文也
祝跃飞
刘楠
陈晨
-
机构
信息工程大学信息工程学院
-
出处
《计算机工程》
CAS
CSCD
北大核心
2010年第2期144-146,共3页
-
基金
国家"863"计划基金资助项目(2007AA01471)
-
文摘
认证性是安全协议检测的重要特性之一,但TA4SP自动协议证明器无法对安全协议的认证性进行检测。针对该问题,提出一种TA4SP的认证性检测方法。该方法基于对TA4SP设计原理的分析,采用分层认证思想,实现对其认证性的理论扩展,其结构清晰、易于形式化。实例表明,通过该方法改进后的TA4SP能有效检测安全协议的认证性。
-
关键词
TA4SP系统
项重写系统
树自动机
认证性
-
Keywords
TA4SP system
Term Rewriting System(TRS)
tree automata
certification
-
分类号
TP309
[自动化与计算机技术—计算机系统结构]
-