北京邮电大学学报

  • EI核心期刊

北京邮电大学学报 ›› 2011, Vol. 34 ›› Issue (2): 54-57.doi: 10.13190/jbupt.201102.54.yangyy

• 论文 • 上一篇    下一篇

模型检测中可变攻击者模型的构造

杨元原,马文平,刘维博   

  1. 西安电子科技大学 教育部计算机网络与信息安全重点实验室, 西安 710071
  • 收稿日期:2010-04-17 修回日期:2010-12-13 出版日期:2011-04-30 发布日期:2011-04-28
  • 通讯作者: 杨元原 E-mail:yangyy@mail.xidian.edu.cn
  • 基金资助:

    国家自然科学基金项目(61072140); 高等学校创新引智计划项目(B08038);高等学校博士学科点专项科研基金项目(20100203110003)

The Construction of Changeable Intruder Model in Model Checking

  • Received:2010-04-17 Revised:2010-12-13 Online:2011-04-30 Published:2011-04-28

摘要:

提出了一个可变攻击者模型构造方案. 该方案通过定义抽象项的概念及其运算规则,大大降低了攻击者进行代数运算的复杂度. 定义了攻击者行为库和攻击规则选择算法,使检测者能根据不同的协议构造不同的攻击者模型. 由于攻击者行为可任意组合,故实现了攻击者模型的可变性. 可变攻击者模型保证了模型检测工具对协议分析的效率和准确性.

关键词: 安全协议, 攻击者模型, 代数运算, 重写规则

Abstract:

A construction scheme of the changeable intruder model is proposed. By defining the concept of abstract terms and their operation rules. The changeable intruder model (CIM) can greatly reduce the complexity of algebraic operations for intruders. And the CIM defines the intruder action library and the attack rule selection algorithm, which enables the analysts construct a changeable intruder model according to different protocols. As the actions of the intruder are composable, the CIM is able to dynamically adjust the intruder models. Changeable intruder model ensures both efficiency and correctness of the protocol analysis for model checkers.

Key words: security protocols, intruder model, algebraic operations, rewrite rules