Adjusted automata learning algorithm for security protocol adaptive model checking

Jing YANG; Dan FAN; Yu-qing ZHANG

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

您当前的位置：

首页 >

文章列表页 >

Adjusted automata learning algorithm for security protocol adaptive model checking

Academic communication | 更新时间：2024-06-05

- Adjusted automata learning algorithm for security protocol adaptive model checking
- Journal on Communications Vol. 36, Issue Z1, Pages: 266-276(2015)
- 作者机构：
  
  1. 西安电子科技大学综合业务网理论及关键技术国家重点实验室，陕西西安710071
  2. 中国科学院大学国家计算机网络入侵防范中心，北京 100190
  3. 中国科学院信息工程研究所信息安全国家重点实验室，北京 100093
- 作者简介：
- 基金信息：
  
  The Core Electronic Devices,High-end Generic Chips and Basic Software 1-4 “Analysis and Security Assessment of the Open Source Operating System Kernel”(2012ZX01039-004-65);The Open Project Program of the State Key Laboratory of Information Security(2014-12)
- DOI：10.11959/j.issn.1000-436x.2015308
  CLC： TP393.08
- Online First：2015-11，
  
  Published：25 November 2015
- 稿件说明：
移动端阅览
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：

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 .

Views

1575

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Research on certificateless anonymous authentication and key agreement scheme of vehicle network based on CPN

Survey on privacy protection indoor positioning

Formal modeling and security analysis method of security protocol based on CPN

Security analysis of security protocol Swift implementations based on computational model

SSMCI:verification mechanism for security protocols centered on the attacker

Related Author

SU Chunhua

FENG Tao

ZHENG Lu

Yanyan XU

Zhiheng WANG

Jinze DU

Tao FENG

Xiang GONG

Related Institution

School of Computer and Communication, Lanzhou University of Technology

Division of Computer Science, University of Aizu

State Key Laboratory of Information Engineering in Surveying Mapping and Remote Sensing, Wuhan University

College of Computer Science,South Central University For Nationalities

The Third College,PLA Information Engineering University

AI问答

⁰