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

The Construction of Changeable Intruder Model in Model Checking

作　　者：杨元原[1] 马文平[1] 刘维博[1] 

机构地区：[1]西安电子科技大学教育部计算机网络与信息安全重点实验室,西安710071

出　　处：《北京邮电大学学报》2011年第2期54-57,共4页Journal of Beijing University of Posts and Telecommunications

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

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

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

分 类 号：TP398[自动化与计算机技术—计算机应用技术]