改进的安全协议自适应分析算法

杨京; 范丹; 张玉清

doi:10.11959/j.issn.1000-436x.2015308

您当前的位置：

首页 >

文章列表页 >

改进的安全协议自适应分析算法

学术通信 | 更新时间：2024-06-05

- 改进的安全协议自适应分析算法
- Adjusted automata learning algorithm for security protocol adaptive model checking
- 通信学报 2015年36卷第Z1期页码：266-276
- 作者机构：
  
  1. 西安电子科技大学综合业务网理论及关键技术国家重点实验室，陕西西安710071
  2. 中国科学院大学国家计算机网络入侵防范中心，北京 100190
  3. 中国科学院信息工程研究所信息安全国家重点实验室，北京 100093
- 作者简介：
  
  [ "杨京（1990-），女，河南新乡人，西安电子科技大学硕士生，主要研究方向为网络和协议安全。" ]
  [ "范丹（1982-），女，河北定州人，博士，中国科学院大学讲师，主要研究方向为网络和协议安全。" ]
  [ "张玉清（1966-），男，陕西宝鸡人，博士，中国科学院大学教授、博士生导师，主要研究方向为网络与信息系统安全。" ]
- 基金信息：
  
  核高基1-4“开源操作系统内核分析和安全性评估”基金资助项目(2012ZX01039-004-65);信息安全国家重点实验室开放基金资助项目(2014-12)
- DOI：10.11959/j.issn.1000-436x.2015308
  中图分类号： TP393.08
- 网络出版日期：2015-11，
  
  纸质出版日期：2015-11-25
- 稿件说明：
移动端阅览
杨京, 范丹, 张玉清. 改进的安全协议自适应分析算法[J]. 通信学报, 2015,36(Z1):266-276.

Jing YANG, Dan FAN, Yu-qing ZHANG. Adjusted automata learning algorithm for security protocol adaptive model checking[J]. Journal on communications, 2015, 36(Z1): 266-276.
杨京, 范丹, 张玉清. 改进的安全协议自适应分析算法[J]. 通信学报, 2015,36(Z1):266-276. DOI： 10.11959/j.issn.1000-436x.2015308.

Jing YANG, Dan FAN, Yu-qing ZHANG. Adjusted automata learning algorithm for security protocol adaptive model checking[J]. Journal on communications, 2015, 36(Z1): 266-276. DOI： 10.11959/j.issn.1000-436x.2015308.

摘要

提出一种改进的安全协议自适应分析算法，即修正学习算法 L

*，解决部分教师缺乏经验的问题，并将字符集扩展为大字符集。对提出的修正学习算法，进行了正确性证明和复杂度分析。该修正学习算法将有助于提高安全协议自适应模型检测的效率、降低分析和设计成本、缓解状态空间爆炸并增强协议本身对环境和各种攻击手段的防御能力。

Abstract

Modifications and improvements for adjusted automata learning algorithms

which were enabled by recent developments.Adjusted automata learning algorithm L

* is correct and efficient.It will be helpful to improve adaptive model checking efficiency

reduce the cost

solve state space explosion problem and resist many kinds of attack methods for security protocols.

关键词

Keywords

references

王亚弟 , 束妮娜 , 韩继红 , 等 . 密码协议形式化分析 [M ] . 北京 : 机械工业出版社 , 2006 .

WANG Y D , SHU N N , HAN J H . Formal Analysis of Security Protocol [M ] . Beijing : China Machine PressPress , 2006 .

WOO T , LAM S S . A semantic model for authentication protocols [A ] . Proceedings of IEEE symposium on security and privacy [C ] . 1993 . 178 - 194 .

CLARKE E M , JHA S , MARRERO W . Partial order reductions for security protocol verification [A ] . Tools and Algorithms for the Construction and Analysis of Systems [C ] . 2000 .

SHAMATIKOV V , STERN U . Efficient finite state analysis for large security protocols [A ] . Proceedings of 11th IEEE Computer Security Foundation Workshop [C ] . 1998 . 106 - 115 .

BROADFOOT P J , ROSCOE A W . Internalising agents in CSP protocol models [A ] . Proceedings of Workshop on Issues in the Theory of Security [C ] . 2002 .

HUI M L , GAVIN L . Fault-preserving simplifying transformations for security protocols [J ] . Journal of Computer Security , 2001 , 9 ( 1-2 ): 3 - 46 .

STOLLER S D . A Bound on Attacks on Authentication protocols [M ] . Foundations of Information Technology in the Era of Network and Mobile Computing . New Yorks Springer US , 2002 .

ROSCOE A W . Proving security protocols with model checkers by data independence techniques [A ] . Proceedings of 11th IEEE Computer Security Foundations Workshop [C ] . 1998 . 84 - 95 .

FAN D , ZHANG Y Q . An adaptive formal modeling and analysis schema for security protocols [A ] . Chinese Association for Cryptologic Research [C ] . ZhengZhou,China , 2014 .

MAZHARI S M , MONSEF H , FALAGHI H . A hybrid heuristic and learning automata-based algorithm for distribution substations siting,sizing and defining the associated service areas [J ] . International Transactions on Electrical Energy Systems , 2014 , 24 ( 3 ): 433 - 456 .

张孝红 . 基于形式化方法的安全协议自动化验证算法的研究 [D ] . 湖南:湖南大学 , 2010 .

ZHANG X H . Automated verification algorithm for security protocols based on formal methods [D ] . Hunan:Hunan University , 2010 .

ANGLUIN D . Learning regular sets from queries and counterexamples [J ] . Information and computation , 1987 , 75 ( 2 ): 87 - 106 .

SHAHBAZ M , GROZ R . Inferring Mealy Machines [M ] . FM 2009 : Formal Methods.Springer Berlin HeidelbergPress , 2009 . 207 - 222 .

BOLLIG B , HABERMEHL P , KERN C , et al . Angluin-style learning of NFA [A ] . IJCAI [C ] . 2009 . 1004 - 1009 .

PACHAROEN W , AOKI T , BHATTARAKOSOL P , et al . Active learning of nondeterministic finite state machines [J ] . Mathematical Problems in Engineering . 2013 . 2013 ( 8 ): 1 - 11 .

Liu P , et al . 形式语言与自动机导论 [M ] . 北京 : 机械工业出版社 , 2005 .

Liu P , et al . An Introduction to Formal Languages and Automata [M ] . Beijing : China Machine Press . 2005 .

SALOMAA A . Formal Languages [M ] . New York:Academic Press . 1973 .

CHEN Y F , FARZAN A , CLARKE E M , et al . Learning minimal separating DFA’s for compositional verification [A ] . Tools and Algorithms for the Construction and Analysis of Systems [C ] . Springer Berlin Heidelberg , 2009 .

ALECHA M , HERMO M . A learning algorithm for deterministic finite automata using JFLAP [J ] . Electronic Notes in Theoretical Computer Science , 2009 , 248 : 47 - 56 .

LEUCKER M , NEIDER D . Learning minimal deterministic automata from inexperienced teachers [A ] . Leveraging Applications of Formal Methods,Verification and Validation.Technologies for Mastering Change [C ] . Springer Berlin Heidelberg , 2012 .

MALER O , MENS I E . Learning regular languages over large alphabets [A ] . Tools and Algorithms for the Construction and Analysis of Systems [C ] . Springer Berlin Heidelberg , 2014 .

PAULL M C , UNGER S H . Minimizing the number of states in incompletely specified sequential switching functions [A ] . IRE Transitions on Electronic Computers EC-8 [C ] . 1959 . 356 - 366 .

NEEDHAM R M , SCHROEDER M D . Using encryption for authentication in large networks of computers [J ] . Communications of the ACM , 1978 , 21 ( 12 ): 993 - 999 .

CREMERS C J F . The scyther tool:verification,falsification,and analysis of security protocols [A ] . Computer Aided Verification [C ] . Springer Berlin Heidelberg , 2008 . 414 - 418 .

LOWE G . Breaking and fixing the needham-schroeder public-key protocol using FDR [A ] . Tools and Algorithms for the Construction and Analysis of Systems [C ] . Springer Berlin Heidelberg , 1996 . 147 - 166 .

浏览量

1082

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

基于CPN的车载网络无证书匿名认证和密钥协商方案研究

室内定位隐私保护综述

基于CPN的安全协议形式化建模及安全分析方法

基于计算模型的安全协议Swift语言实施安全性分析

SSMCI：以攻击者为中心的安全协议验证机制