摘要
随着计算机网络的迅速发展,信息通信的安全问题变得越来越突出,越来越复杂,解决安全问题对许多网络应用来说具有重要意义。目前,网络通信安全问题的解决方案中,安全协议是最有效的手段之一。由于网络本身的开放性,使得网络中存在着各种安全威胁,攻击者可以采用多种方式对安全协议进行攻击,破坏其安全属性。分析安全协议中可能存在的缺陷很难完全由人工来识别,因此,需要借助形式化的分析方法和工具来完成。
安全协议的形式化分析过程包含安全协议系统建模、安全属性验证、以及攻击序列生成等。本文通过分析安全协议模型中攻击者的“任意”性行为和协议的多次并发会话问题,提出了一种改进的攻击者模型和多并发会话划分分析方法。针对安全属性验证和攻击序列生成问题,采用安全属性违背事件对不安全状态进行分类描述,提出基于安全属性违背事件生成攻击序列的两种方法：状态空间搜索法和on-the-fly生成方法。基于安全属性违背事件生成攻击序列的方法能够有效地控制搜索范围,提高搜索效率。最后通过分析安全协议中的数据特征,提取能够构成攻击的攻击策略,并依据攻击策略确定攻击目的,构建基于攻击目的的模型,选择生成攻击序列,有效地削减安全协议模型检测的状态空间。
本文的贡献和创新性工作如下：
(1)提出安全协议模型的多并发会话划分分析方法
针对带有攻击者模型的安全协议形式化模型的复杂运行特点,提出一种改进的攻击者模型。通过对Dolev-Yao攻击者模型进行分析,将攻击者的功能划分为分解和合成两个前后阶段。同时,分析带有攻击者的安全协议形式化模型时,往往需要考虑多次并发会话的情况下攻击是否成功的情况。文本针对这一特点,通过会话配置和会话顺序的设定,提出多并发会话划分分析方法,一次分析一种并发情况,能够有效地划分并削减模型验证的状态空间。
(2)提出基于安全属性违背事件的安全协议攻击序列生成方法
针对攻击序列生成需求,定义面向安全协议攻击序列生成的CP-nets模型(Attack Trace Generation Oriented CP-nets,ATG-CPN)。依据安全协议规范和模型的特点,给出安全属性的形式化定义,并将攻击状态采用安全属性违背事件进行分类描述。提出基于ATG-CPN模型的状态空间搜索方法,生成到达攻击状态的攻击序列,减少了状态空间中搜索的状态数,避免生成虚假攻击。同时提出基于ATGx-CPN模型的on-the-fly攻击序列生成方法,该方法不需要对整个状态空间进行广度或深度搜索,基于部分状态空间生成有效的攻击序列。
(3)提出一种基于攻击策略的攻击序列选择生成方法
利用攻击序列生成方法能够得到大量的攻击序列,为集中有限的资源对安全协议系统存在的攻击序列实施重点分析,需要进一步确定依据攻击策略的攻击事件,选择生成攻击序列,使生成的有限攻击序列充分覆盖攻击目的。
With the rapid development of the Internet, and increasing attention to the security of communication system, security protocols are widely deployed in the Internet. As the increasingly attacking capabilities and complexity of the applications, the design and analysis of security protocols are difficult to achieve. Model checking and attack trace generation method are major technologies to validate the correctness of security protocol.
The Security protocol analysis and validation include security protocol modeling, attack trace generation and selection. Major causes of complexity of security protocol execution are resulted by the Dolev-Yao based attacker model and protocol multi concurrent sessions. A new improved attacker model is introduced. A new session configuration based dividing analysis method is effectively controlled the number of concurrent session. Attack states are characterized by security properties voilation events in the non secure states. Two attack sequence generation approach based on security properties voilation events are proposed:state exploration method and on-the-fly generation method. The security properties voilation events based attack sequence generation approach can effectively control the exploration scope and improve efficiency. Finally, by analyzing the data features of the security protocols, extract the attack tactics capable of form a successful attack. Based on attak tactics, modeling attack purpose and generating attack traces generally can reduce the workload of searching the state space.
The main contributions of this dissertation are as follows:(1) A new multi concurrent session partition analysis method for security protocol model is presented.
We proposed a new improved attacker model without reduce the capability of the Dolev-Yao attacker. Attacker's function is divided into the decomposition and synthesis of two front and rear stages. Formal analysis of security protocol with an attacker needs to consider whether the attack was successful in the case of multiple concurrent sessions. By setting session configuration and session sequence, we proposed a multiple concurrent sessions partition analysis method, which is effectively reduce the state space of the model checking.
(2) New attack sequence generation methods based on the security property voilation events are proposed.
Attack Trace Generation Oriented CP-nets (ATG-CPN) is formally defined to model the security protocol with an attacker. Formal definition of security properties, including confidentiality property and authencation property, are given according to the security specification and formal model. Attack states are characterized by security property voilation events. Based on ATG-CPN models and security property voilation events, an attack sequence generation method is proposed. This novel CP-nets model based attack sequence generation approach improves the error coverage and avoids generating false attacks. A new CP-nets model based On-the-fly attack sequence generation method is also proposed, which does not need to explore the entire state space, so can effectively generate attack sequences.
(3) A method of attack tactics based attack sequence selection method is presented.
Using attack sequence generation method may generate a lot of attack sequences, to fit the model checking demand, a new attack tactics based attack sequence selection method is given. The limited attack sequences obtained after selection process meet coverage of attack trace generation purposes.
引文
[1]薛锐,冯登国.安全协议的形式化分析技术与方法.计算机学报[J],2006.29(1)：p.1-20.
[2]薛锐,雷新锋.安全协议：信息安全保障的灵魂——安全协议分析研究现状与发展趋势.中国科学院院刊[J],2011.26(3)：p.287-296.
[3]冯登国,范红.安全协议形式化分析理论与方法研究综述.中国科学院研究生院学报[J],2003.20(4)：p.389-406.
[4]Lowe G Some new attacks upon security protocols.Computer Security Foundations Workshop IEEE[C].1996:p.162-169.
[5]Armando A, Pellegrino G, Carbone R, et al. From model-checking to automated testing of security protocols:Bridging the gap. Tests and Proofs[J],2012:p.3-18.
[6]Lowe G Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Tools and Algorithms for the Construction and Analysis of Systems[J],1996:p.147-166.
[7]Mitchell J, Mitchell M, Stern U. Automated analysis of cryptographic protocols using Mur/spl phi. sp[J],1997:p.0141.
[8]Constant C, Jeron T, Marchand H, et al. Integrating formal verification and conformance testing for reactive systems. Software Engineering, IEEE Transactions on[J],2007.33(8):p.558-574.
[9]C. A. Petri. Kommunikationen Mit Automaten. [PhD Thesis].1962, University of Bonn. English translation:Technical Report RADC-TR-65-377, Vol.1, Suppl 1,Applied Data Research, Princeton, N.J.,
[10]林闯.随机Petri网的分解和压缩技术.软件学报[J],1997.8(007)：p.541-548.
[11]Wang J. Timed Petri nets:Theory and application[M]. Vol.39.1998:Kluwer Academic Publishers Norwell.
[12]孙宇霖.基于构造类别代数协议测试理论的研究.[硕士学士论文].2002,合肥：中国科学技术大学.
[13]孙宇霖,屈玉贵.一种通信协议测试序列生成的新方法.通信学报[J],2001.22(6)：p.122-127.
[14]Needham R M, Schroeder M D. Using encryption for authentication in large networks of computers. Communications of the ACM[J],1978.21(12):p.993-999.
[15]Dolev D Y A. On the security of public key protocols.Proceedings of the IEEE 22nd Annual Symposium on Foundations of Computer Science, Nashville, TN[C].1981. p.350-357.
[16]Dolev D, Yao A. On the security of public key protocols. Information Theory, IEEE Transactions on[J],1983.29(2):p.198-208.
[17]Burrows M, Abadi M, Needham R M. A logic of authentication. Proceedings of the Royal Society of London. A. Mathematical and Physical Sciences[J],1989.426(1871):p.233-271.
[18]Gong L, Needham R, Yahalom R. Reasoning about belief in cryptographic protocols.Research in Security and Privacy,1990. Proceedings.,1990 IEEE Computer Society Symposium on[C]. 1990:IEEE. p.234-248.
[19]Accorsi R, Basin D, Vigano L. Towards an awareness-based semantics for security protocol analysis. Electronic Notes in Theoretical Computer Science[J],2003.55(1):p.5-24.
[20]van Oorschot P. Extending cryptographic logics of belief to key agreement protocols.Proceedings of the 1st ACM Conference on Computer and Communications Security[C].1993:ACM. p.232-243.
[21]Syverson P F, Van Oorschot P C. On unifying some cryptographic protocol logics.Research in Security and Privacy,1994. Proceedings.,1994 IEEE Computer Society Symposium on[C]. 1994:IEEE. p.14-28.
[22]Paulson L C. The inductive approach to verifying cryptographic protocols. Journal of Computer Security[J],1998.6(1-2):p.85-128.
[23]Paulson L C. Proving properties of security protocols by induction.Computer Security Foundations Workshop,1997. Proceedings.,10th[C].1997:IEEE. p.70-83.
[24]Fabrega F J T, Herzog J C, Guttman J D. Strand spaces:Why is a security protocol correct?Security and Privacy,1998. Proceedings.1998 IEEE Symposium on[C].1998:IEEE. p. 160-171.
[25]Herzog J C. The Diffie-Hellman key-agreement scheme in the strand-space model.Computer Security Foundations Workshop,2003. Proceedings.16th IEEE[C].2003:IEEE. p.234-247.
[26]Ji Q, Qing S, Zhou Y, et al. Study on strand space model theory. Journal of Computer Science and Technology[J],2003.18(5):p.553-570.
[27]Li X, Wang Z, Chen L, et al. A multi-party contract signing protocol and its formal analysis in strand space model.Education Technology and Computer Science,2009. ETCS'09. First International Workshop on[C].2009:IEEE. p.556-559.
[28]Borgstrom J, Briais S, Nestmann U. Symbolic bisimulation in the spi calculus, CONCUR 2004-Concurrency Theory[M].2004, Springer, p.161-176.
[29]Abadi M, Gordon A D. A calculus for cryptographic protocols:The spi calculus.Proceedings of the 4th ACM conference on Computer and communications security[C].1997:ACM. p.36-47.
[30]Baldamus M, Parrow J, Victor B. Spi calculus translated to π-calculus preserving may-tests.Logic in Computer Science,2004. Proceedings of the 19th Annual EEEE Symposium on[C].2004:IEEE. p.22-31.
[31]李梦君,李舟军,陈火旺.基于进程代数安全协议验证的研究综述.计算机研究与发展[J],2004.41(7)：p.1097-1103.
[32]Haack C, Jeffrey A. Timed spi-calculus with types for secrecy and authenticity, CONCUR 2005-Concurrency Theory[M].2005, Springer, p.202-216.
[33]http://www.cl.cam.ac.cuk/research/hvg/Isabelle/LCPI.
[34]Milner R, Parrow J, Walker D.A calculus of mobile processes, i. Information and computation[J],1992.100(1):p.1-40.
[35]Abadi M. Secrecy by typing in security protocols. Journal of the ACM (JACM)[J],1999.46(5): p.749-786.
[36]Gordon A D, Jeffrey A. Authenticity by typing for security protocols. Journal of Computer Security[J],2003.11(4):p.451-520.
[37]Clarke E M, Grumberg O, Peled D. Model checking[M].1999:The MIT press.
[38]Meadows C.The NRL protocol analyzer:An overview. The Journal of Logic Programming[J], 1996.26(2):p.113-131.
[39]Millen J K, Clark S C, Freedman S B. The interrogator:Protocol secuity analysis. Software Engineering, IEEE Transactions on[J],1987(2):p.274-288.
[40]Vigano L. Automated security protocol analysis with the AVISPA tool. Electronic Notes in Theoretical Computer Science[J],2006.155:p.61-86.
[41]Blanchet B. An efficient cryptographic protocol verifier based on Prolog rules.Proceedings of the 14th IEEE workshop on Computer Security Foundations[C].2001. p.82.
[42]Maggi P, Sisto R. Using SPIN to verify security properties of cryptographic protocols. Model Checking Software[J],2002:p.85-87.
[43]Lowe G, Roscoe B. Using CSP to detect errors in the TMN protocol. Software Engineering, IEEE Transactions on[J],1997.23(10):p.659-669.
[44]Shmatikov V, Mitchell J C. Finite-state analysis of two contract signing protocols. Theoretical Computer Science[J],2002.283(2):p.419-450.
[45]Al-Azzoni Ⅰ, Down D, Khedri R. Modeling and verification of cryptographic protocols using coloured petri nets and design/CPN. Nordic Journal of Computing [J],2005.12(3):p.201-208.
[46]张超.安全协议攻击序列重构技术研究.[硕士学士论文].2008,解放军信息工程大学.
[47]Basagiannis S, Katsaros P, Pombortsis A. State Space Reduction with Message Inspection in Security Protocol Model Checking. arXiv preprint arXiv:0909.0174[J],2009:p.1-15.
[48]沈海峰,黄河燕,陈肇雄.串空间代数缺陷到实际攻击的转换.计算机科学[J],2005.32(7)：p.90-92.
[49]Steel G J. Discovering Attacks on Security Protocols by Refuting Incorrect Inductive Conjectures. [Thesis].2004, University of Edinburgh.
[50]Allamigeon X, Blanchet B. Reconstruction of attacks against cryptographic protocols.Computer Security Foundations,2005. CSFW-18 2005.18th IEEE Workshop[C].2005:IEEE. p.140-154.
[51]Lowe G. Towards a completeness result for model checking of security protocols. Journal of Computer Security[J],1999.7(2):p.89-146.
[52]Yorav K, Grumberg O. Static analysis for state-space reductions preserving temporal logics. Formal Methods in System Design[J],2004.25(1):p.67-96.
[53]Jensen K, Kristensen L. Coloured Petri Nets:Modeling and Validation of Concurrent Systems[M].2009:Springer-Verlag New York Inc.
[54]CPN Tools[EB/OL]:http://cpntools.org.
[55]Jensen K, Kristensen L M, Wells L. Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems. International Journal on Software Tools for Technology Transfer (STTT)[J],2007.9(3):p.213-254.
[56]Emerson E A, Halpern J Y. "Sometimes" and "not never" revisited:on branching versus linear time temporal logic. Journal of the ACM (JACM)[J],1986.33(1):p.151-178.
[57]Cheng A, Christensen S, Mortensen K H. Model checking coloured petri nets exploiting strongly connected components. DAIMI PB[J],1997.26(519):p.1-17.
[58]Jensen K. Coloured Petri nets and the invariant-method. Theoretical Computer Science[J],1981. 14(3):p.317-336.
[59]Ratzer A V, Wells L, Lassen H M, et al. CPN tools for editing, simulating, and analysing coloured Petri nets, Applications and Theory of Petri Nets 2003 [M].2003, Springer, p.450-462.
[60]Beaudouin-Lafon M, Mackay W E, Andersen P, et al. CPN/Tools:A post-WIMP interface for editing and simulating coloured Petri nets, Applications and Theory of Petri Nets 2001[M]. 2001, Springer.p.71-80.
[61]Jensen K, Kristensen L, Wells L. Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems. International Journal on Software Tools for Technology Transfer (STTT)[J],2007.9(3):p.213-254.
[62]Kristensen L, Petrucci L. An approach to distributed state space exploration for coloured Petri nets. Applications and Theory of Petri Nets 2004[J],2004:p.474-483.
[63]Billington J, Gallasch G E, Kristensen L M, et al. Exploiting equivalence reduction and the sweep-line method for detecting terminal states. Systems, Man and Cybernetics, Part A: Systems and Humans, IEEE Transactions on[J],2004.34(1):p.23-37.
[64]Jensen K. Special section on coloured Petri nets. International Journal of Software Tools for Technology Transfer[J],1998.2(2):p.95-191.
[65]Jensen K. Special section on coloured Petri nets. International Journal on Software Tools for Technology Transfer (STTT)[J],2007.9(3):p.209-212.
[66]Huber P, Jensen K, Shapiro R. Hierarchies in coloured Petri nets. Advances in Petri Nets 1990[J],1991:p.313-341.
[67]Jensen K. An introduction to the theoretical aspects of coloured Petri nets. A decade of Concurrency Reflections and Perspectives[J],1994:p.230-272.
[68]Billington J, Gupta A K. Effectiveness of coloured Petri nets for modelling and analysing the contract net protocol.Eighth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools[C].2007. p.49.
[69]Billington J, Gupta A, Gallasch G. Modelling and analysing the contract net protocol-extension using coloured petri nets. Formal Techniques for Networked and Distributed Systems-FORTE 2008[J],2008:p.169-184.
[70]Liu J, Ye X, Sun T. Towards Formal Modeling and Analysis of BitTorrent using Colored Petri Nets.Proceedings of the CPN Workshop 2009[C].2009. p.159-178.
[71]Boukredera D, Aknine S, Maamri R. Modeling Temporal Aspects of Contract Net Protocol Using Timed Colored Petri Nets.STAIRS[C].2012. p.83-94.
[72]Blanco M, Villapol M E. Analyzing the procedure for AMP enabled operation in Bluetooth 3.0 using Colored Petri Nets.Global Information Infrastructure and Networking Symposium (GIIS), 2012[C].2012:IEEE. p.1-8.
[73]Sun T, Ye X, Liu J. A Test Generation Method Based on Model Reduction for Parallel Software.Proceedings of the 2012 13th International Conference on Parallel and Distributed Computing, Applications and Technologies[C].2012:IEEE Computer Society, p.777-782.
[74]SUN T, YE X. A Model Reduction Method for Parallel Software Testing. Journal of Applied Mathematics[J],2013.
[75]Lee G-S, Lee J-S. Petri net based models for specification and analysis of cryptographic protocols. Journal of systems and software[J],1997.37(2):p.141-159.
[76]刘雪艳,吴慧欣,张强,et al基于面向对象时间Petri网的密码协议分析.计算机工程[J],2009.35(13)：p.156-159.
[77]Shao Y. Specification and analysis of Internet cryptographic protocols using a Petri net modeler[M].2000:Queen's University.
[78]Xu Y, Xie X. Modeling and analysis of security protocols using Colored Petri Nets. Journal of Computers[J],2011.6(1):p.19-27.
[79]Seifi Y, Suriadi S, Foo E, et al. Analysis of Object-Specific Authorization Protocol (OSAP) using Coloured Petri Nets. Information Security 2012[J],2012:p.47-58.
[80]Permpoontanalarp Y, Sornkhom P. A new coloured petri net methodology for the security analysis of cryptographic protocols.Proc.10th Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools[C].2009. p.81-100.
[81]Permpoontanalarp Y, Changkhanak A. On-the-Fly Trace Generation Approach to the Security Analysis of the TMN Protocol with Homomorphic Property:A Petri Nets-Based Method. IEICE TRANSACTIONS on Information and Systems[J],2012.95(1):p.215-229.
[82]Escobar S, Meadows C, Meseguer J. State space reduction in the Maude-NRL protocol analyzer. Computer Security-ESORICS 2008[J],2008:p.548-562.
[83]Song D X, Berezin S, Perrig A. Athena:a novel approach to efficient automatic security protocol analysis. Journal of Computer Security [J],2001.9(1/2):p.47-74.
[84]Armando A, Compagna L. An optimized intruder model for SAT-based model-checking of security protocols. Electronic Notes in Theoretical Computer Science[J],2005.125(1):p. 91-108.
[85]Rusinowitch M, Turuani M. Protocol insecurity with a finite number of sessions and composed keys is NP-complete. Theoretical Computer Science[J],2003.299(1):p.451-475.
[86]Lowe G. An attack on the Needham-Schroeder public-key authentication protocol. Information processing letters[J],1995.56(3):p.131-133.
[87]Tatebayashi M, Matsuzaki N, Newman Jr D B. Key distribution protocol for digital mobile communication systems.1989:Springer-Verlag New York, Inc.:p.324-334.
[88]Mitchell J C, Mitchell M, Stern U. Automated analysis of cryptographic protocols using Mur(?).Security and Privacy,1997. Proceedings.,1997 IEEE Symposium on[C].1997:IEEE. p. 141-151.
[89]Canetti R, Herzog J. Universally Composable Symbolic Security Analysis. Journal of cryptology[J],2011.24(1):p.83-147.
[90]Lowe G. A hierarchy of authentication specifications.Computer Security Foundations Workshop, 1997. Proceedings.,10th[C].1997:IEEE. p.31-43.
[91]Fernandez J-C, Mounier L, Pachon C. Property oriented test case generation. Formal Approaches to Software Testing[J],2004:p.1101-1102.
[92]刘靖.基于CP-nets模型的IOCO一致性测试方法研究.[博士学位论文],中国科学院计算技术研究所.2011,中国科学院研究生院：Beijing.
[93]Zhang Y-Q, Liu X-Y. An approach to the formal analysis of TMN protocol. KLUWER INTERNATIONAL SERIES IN ENGINEERING AND COMPUTER SCIENCE.[J],2004:p. 235-243.
[94]Permpoontanalarp Y. On-the-Fly trace generation and textual trace analysis and their applications to the analysis of cryptographic protocols, Formal Techniques for Distributed Systems[M].2010, Springer.p.201-215.
[95]Martins E, Morais A, Cavalli A. Generating attack scenarios for the validation of security protocol implementations.The 2nd Brazilian Workshop on Systematic and Automated Software Testing (SBES 2008-SAST)[C].2008. p.21-33.
[96]Basagiannis S, Katsaros P, Pombortsis A. Intrusion Attack Tactics for the model checking of e-commerce security guarantees. Computer Safety, Reliability, and Security[J],2007:p. 238-251.
[97]Basagiannis S, Katsaros P, Pombortsis A. Synthesis of attack actions using model checking for the verification of security protocols. Security and Communication Networks[J],2011.4(2):p. 147-161.