[1]唐郑熠,杨芳,薛醒思.安全协议验证中DY模型的构建框架[J].福建理工大学学报,2015,13(03):239-243.[doi:10.3969/j.issn.1672-4348.2015.03.007]
　Tang Zhengyi,Yang Fang,Xue Xingsi.A framework for constructing DY model in security protocol verification[J].Journal of Fujian University of Technology;,2015,13(03):239-243.[doi:10.3969/j.issn.1672-4348.2015.03.007]
点击复制

安全协议验证中DY模型的构建框架()
分享到：

《福建理工大学学报》[ISSN:2097-3853/CN:35-1351/Z]

卷:
第13卷
期数:
2015年03期
页码:
239-243
栏目:
出版日期:
2015-06-25

文章信息/Info

Title:
A framework for constructing DY model in security protocol verification
作者:
唐郑熠; 杨芳; 薛醒思
福建工程学院信息科学与工程学院
Author(s):
Tang Zhengyi;  Yang Fang;  Xue Xingsi
College of Information Science and Engineering, Fujian University of Technology
关键词:
安全协议;  形式化;  DY模型;  攻击者;  OtwayRees协议
Keywords:
security protocol;  formalization;  Dolev and Yao (DY) model;  intruder;  OtwayRees protocol
分类号:
TP393.08
DOI:
10.3969/j.issn.1672-4348.2015.03.007
文献标志码:
A
摘要:
攻击者建模是安全协议验证工作的一个重要部分，直接影响到验证的效率与质量，但目前却还没有一个可遵循的形式化框架，影响了建模工作的准确性与客观性。针对这一问题，通过对在安全协议验证中具有广泛影响的DY模型进行形式化，建立了一个DY模型的构建框架，刻画了攻击者的构成要素、行为规则以及行为模式，从而保证了攻击者具有合理的行为与能力，并能在攻击过程中获取新的知识，不断增强攻击能力。最后，将该工作运用到OtwayRees协议的验证中，找出了该协议中所存在的漏洞，从而证明了该构建框架的有效性。
Abstract:
The modelling of intruders is an important part of security protocol verification, which directly affects the efficiency and correctness of verification. There is no available formal framework of introders modelling, which is a disadvantage for modelling work. A framework for formalizing/constructing DY model that has extensive influence on security protocol verification was proposed. The framework can depict the components, behaviours and behaviour model of the intruders, which ensures that the intruder has reasonable behaviours and ability and can acquire new knowledges in the attacking process to enhance contantly the attacking ability. The effectiveness of the framework was confirmed in the verification of OtwayRees protocol in which a fault in the protocol was found.

参考文献/References:

[1]Dolev D, Yao A. On the security of public key protocols[J]. IEEE Transactions on Information Theory,1983,29(2):198-208.
[2]钟军,吴雪阳,江一民,等.一种安全协议的安全性分析及攻击研究[J].计算机工程与科学,2014,36(6):1077-1082.
[3]冉俊铁,吴尽昭.基于SPIN的安全协议形式化验证技术[J].计算机应用,2014:34(S2):85-90.
[4]陈春玲,田国良.安全协议的SPIN建模与分析[J].南京航空航天大学学报,2009,41(5):672-676.
[5]Fu Yulong, Ousmane K. A finite transition model for security protocol verification[C]//Proc of 6th International Conference on Security of Information and Networks. Aksaray, Turkey,2013.
[6]龙士工,王巧丽,李祥.密码协议的Promela语言建模及检测[J].计算机应用,2005,25(7):1548-1550.
[7]Kanovich M, Kiriginc T B, Nigamd Vi,et al. Bounded memory DolevYao adversaries in collaborative systems[J]. Information and Computation, 2014, 238: 233-261.
[8]Mazare L. Satisfiability of DolevYao constraints[J]. Electronic Notes in Theoretical Computer Science,2005,125(1):109-124.
[9]Otway D, Rees O. Efficient and timely mutual authentication[J]. ACM Operating Systems Review,1987,21(1):8-10.
[10]Abadi M, Needham R. Prudent engineering practice for cryptographic protocols[J]. IEEE Transactions on Software Engineering,1996,22(1):6-15.

更新日期/Last Update: 2015-06-25