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

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

摘要/Abstract

摘要：

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

关键词: 安全协议, 自适应模型检测, 学习算法, 缺乏经验的教师, 符号自动机

Abstract:

Modifications and improvements for adjusted automata learning algorithms,which were enabled by recent developments.Adjusted automata learning algorithm L_a* 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.

Key words: security protocol, adaptive model checking, learning algorithm, inexperienced teacher, symbolic automata

杨京,范丹,张玉清. 改进的安全协议自适应分析算法[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.

图/表 20

图1

图2

图3

图4

图5

表1

图6

表2

表3

表4

表5

表6

图7

图8

图9

图10

图11

图12

图13

表7

参考文献 25

[1]	王亚弟, 束妮娜, 韩继红 , 等. 密码协议形式化分析[M]. 北京: 机械工业出版社, 2006. WANG Y D , SHU N N , HAN J H . Formal Analysis of Security Protocol[M]. Beijing: China Machine PressPress, 2006.
[2]	WOO T , LAM S S . A semantic model for authentication protocols[A]. Proceedings of IEEE symposium on security and privacy[C]. 1993. 178-194.
[3]	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.
[4]	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.
[5]	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.
[6]	HUI M L , GAVIN L . Fault-preserving simplifying transformations for security protocols[J]. Journal of Computer Security, 2001,9(1-2): 3-46.
[7]	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.
[8]	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.
[9]	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.
[10]	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.
[11]	张孝红 . 基于形式化方法的安全协议自动化验证算法的研究[D]. 湖南:湖南大学, 2010. ZHANG X H . Automated verification algorithm for security protocols based on formal methods[D]. Hunan:Hunan University, 2010.
[12]	ANGLUIN D . Learning regular sets from queries and counterexamples[J]. Information and computation, 1987,75(2): 87-106.
[13]	SHAHBAZ M , GROZ R . Inferring Mealy Machines[M]. FM 2009: Formal Methods.Springer Berlin HeidelbergPress, 2009. 207-222.
[14]	BOLLIG B , HABERMEHL P , KERN C , et al. Angluin-style learning of NFA[A]. IJCAI[C]. 2009. 1004-1009.
[15]	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.
[16]	Liu P , et al. 形式语言与自动机导论[M]. 北京: 机械工业出版社, 2005. Liu P , et al. An Introduction to Formal Languages and Automata[M]. Beijing: China Machine Press. 2005.
[17]	SALOMAA A . Formal Languages[M]. New York:Academic Press. 1973.
[18]	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.
[19]	ALECHA M , HERMO M . A learning algorithm for deterministic finite automata using JFLAP[J]. Electronic Notes in Theoretical Computer Science, 2009,248: 47-56.
[20]	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.
[21]	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.
[22]	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.
[23]	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.
[24]	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.
[25]	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.

T	λ	b
λ	-	?
b	?	?
ba	-	+
bab	+	+
a	-	?
bb	?	?
baa	-	+
baba	-	?
babb	+	+

T₀	λ
λ	0
a₀	0

T₁	λ
λ	0
a₀	0
a₁	1

T₂	λ
λ	0
a₁	1
a₀	0
a₁a₂	1

T₃	λ
λ	0
a₀	0
a₁	1
a₀a₄	0
a₁a₂	1
a₃	0