基于Petri网的安全策略分析与验证方法研究
|
摘要
伴随着科学技术的飞速发展,信息已成为推动社会前进的巨大动力。利用计算机和网络对信息进行收集、加工、存储以及交换等,越来越成为各行各业必不可少的手段,计算机已经渗透到了社会生活的各个方面,各种信息系统的建立和使用造成我们对计算机系统事实上的依赖。但是,由于各系统中存储的数据、网络上传输和交换的数据都是具有一定价值的信息,对这些信息的非法访问、窃取、篡改等行为必然导致计算机安全问题的出现。
当前,系统的庞大和复杂化使得系统安全性能分析与验证问题变得越来越复杂并越来越引起人们的重视。提供有效的数学理论工具、直观的模型描述方法和有效的模型分析方法以及实用的辅助分析软件,是系统安全性能分析与验证所面临的迫切需要解决的问题,这也正是基于Petri网的安全策略分析与验证技术的核心。
从计算机系统、Web服务以及安全协议的安全需求和现实基础出发,对相关理论、协议、关键技术以及具体实现进行了广泛深入的研究。主要研究工作包括以下几个方面:
保密性策略和完整性策略是重要的安全策略,在许多军用和商用系统中得到广泛的应用。其代表模型分别是Bell-LaPadula模型和Biba模型,这两个模型是数学上的对偶。保密性策略用于防止信息的非授权泄漏,而完整性策略则是防止信息被非授权更改。对采用了特定安全模型的具体实用系统需要一个严格有效的方法对其保密性和完整性进行分析和验证。安全策略研究的一个关键问题是:用易于理解的和精确的形式表达策略。因此,提出了利用Petri网对安全策略进行描述,Petri网不仅适合策略的表达,而且可用于系统分析,以确定所定义的机制是否符合策略定义。
对于一个安全策略,首先建立基于Petri网的形式化描述,然后就可以根据形式化的描述对实施了特定安全模型的进程或系统进行分析与验证。分别对Bell-LaPadula保密性模型和Biba完整性模型进行了描述。给出了这两个模型基于Petri网的形式化定义,并对实施了这两个安全模型的相应示例进程进行了分析和验证。显示出Petri网不仅能够用用易于理解的和精确的形式表达安全策略,而且可用于系统分析和验证。Petri网的覆盖图则在自动分析大型复杂系统方面很有用处。
为了对实施了中国墙模型的系统进行分析与验证,提出了一种基于有色Petri网的混合安全策略分析方法。中国墙模型是一种兼顾保密性和完整性的混合安全模型。中国墙模型的显著特征是自由选择和强制性访问控制的结合。首先,对中国墙模型进行了非形式化的描述,并且将中国墙模型与其他安全模型进行了比较。然后,给出了中国墙模型基于有色Petri网的形式化定义。其突出特征在于,引入了“控制库所”的概念以解决跟踪主体访问记录的问题。并且“控制库所”代替访问控制矩阵,与单个主体关联,不需要集中存储,更加适合在分布式环境下部署。最后,根据中国墙模型基于有色Petri网的定义,通过对一个实施了中国墙模型的示例进程进行分析与验证,阐述了如何通过基于有色Petri网的形式化定义和覆盖图分析和验证实施了中国墙模型的系统的行为。
当前的互联网正在经历着一些重要的变化,它已经成为了一个Web服务的载体,而不仅仅是一个信息的容器。Web服务提供了一个语言中立,连接松散,独立于平台的方式,使得散布在互联网上的各组织和企业内部的应用程序可以连接起来。Web服务合成可以让我们将许多现有的Web服务结合起来,形成一个新的,增值的Web服务。可靠的Web服务合成需要建模的技术和工具。因此,提出了一个基于有色Petri网的Web服务合成模型。这个模型为Web服务合成提供了充分的表达能力,能够直接变换为可执行的合成定义,并且独立于可执行的合成语言。基于Petri网的Web服务合成模型还可以利用Petri网的分析和验证能力对合成服务进行安全分析和验证。
首先,对Web服务建立了有色Petri网模型(服务网),然后在此定义的基础上给出了四种基本Web服务合成结构:顺序结构,并发结构,选择结构,和循环结构以及一种高级合成结构置换结构的形式化定义。并且还定义了一个具有封闭性的Web服务合成算法。最后,根据基于Petri网的形式化验证方法对此Web服务合成模型的可用性,保密性,完整性以及混合安全性进行了分析和验证,得出了一些有用的结论。
20年来,安全协议研究的进展十分可喜,取得了丰富的研究成果。特别是20世纪90年代以来,研究取得突破性进展,对安全协议若干本质性的问题有了更为深刻的认识。但是,这一领域还有许多问题有待解决。特别是形式化分析领域。因此,提出了一种基于有色Petri网的安全协议分析验证方法,该方法分为4个步骤:建立安全协议的Petri模型,建立入侵模型,找出不安全状态,验证不安全状态的可达性。并且通过对STS协议在特定攻击模式下的分析演示了该方法的工作原理和流程。
With the rapidly development of science and technology, information technology has had an influence on the way we work and on society in general. Information technology is more and more becoming the requisite tools for gathering, processing, storing and exchanging information with computers. We are more and more relying on computer systems. However, the data stored in systems, transferred and exchanged on networks is valuable. When the information is unauthorized accessed, intercepted or modified, the problems of computer security are coming out.
Nowadays, huge and complex systems make the security analysis and verification become more complex and get more concerned. Security analyzing and verifying systems needs available mathematical tools, visual model describing and analyzing methods and practical assistant software. And that is the core element for the security analysis and verification technology based on Petri nets.
Based on realistic requirements and foundations, this thesis engaged in extensive research on some relevant theories, protocols and key technologies. The main contributions are as follows:
Confidentiality policy and integrity policy are important security policies, implemented in many militarily and commercial systems. Bell-LaPadula model and Biba model are mathematical dual. A confidentiality policy prevents the unauthorized disclosure of information, and an integrity policy prevents the unauthorized modification of information. Both security models and practical systems need an available method to conduct security analysis and verification. One of the most important issues in security policies research is: to describe the policies in precise and easily understand form.
Thus, this thesis proposes a method to describe security policies by Petri nets. Petri nets are not only good for define policies, but also well for system analysis to verify that the system mechanisms are corresponding with the definitions. For a security policy, firstly build the Petri net-based model and formal definitions of the model, and then The Petri net-based definitions and the coverability graph allow one to analyze and verify the security policy in Petri net model of a system. In this thesis, the Petri net-based definitions of Bell-LaPadula model and Biba Model are formally described in detail. Subsequently, examples of the confidentiality policy and integrity policy are illustrated and the conclusions show that Petri net is not only a concise graphic analysis method, but also suited to formal verification.
For analyzing and verifying systems implemented with Chinese Wall policy, this thesis proposes a Petri net-based method to analyze hybrid policy. The Chinese Wall model is a model of a security policy that refers equally to confidentiality and integrity. The important feature of the Chinese Wall policy is the combination of discretionary access control and mandatory access control. Firstly, the Chinese Wall policy is informally described, and compared with other security policies. And then, the Petri net-based formal definitions are given. The main contribution of the definitions is the concept of "control place", which is used to trace the access record of subjects. The access control matrix is replaced by control place, which is associated with single subject and suited for implementation in distributed environment. Finally, the analysis and verification of the Chinese Wall policy by the method are addressed through a sample system.
The Internet is going through several major changes. It has become a vehicle of Web services rather than just a repository of Information. Web services provide a language-neutral, loosely coupled, and platform-independent way for linking applications within organizations or enterprises across the Internet. Web services composition allows us to combine a number of existing Web services into a new, value-added Web service.
Therefore, there is a need for modeling techniques and tools for reliable Web service composition. This thesis proposes a Colored Petri net-based model for Web service composition. This model is sufficiently expressive for Web service composition, can be transformed to directly executable composition specification; and is independent of the executable composition languages. Firstly, we model web service as colored Petri net (service net), based on which four basic composition construct and one advance composition construct are formally defined. Subsequently, we present the algebra that allows the creation of new value-add Web services using existing ones as building blocks. Finally, the colored Petri net-based web service composition model is verified on availability, confidentiality and integrity, and reaches some useful conclusions.
In recent twenty years, the research on security protocols has made great achievements. Especially from 1990's, some breakthroughs made us better understand several essential issues of security protocols. However, many problems need to be solved in this field, especially in formal analysis. Thus, this thesis proposes a Petri net-based method to analyze and verify security protocols. There are 4 steps: describe the protocol in a colored Petri net form, describe the intruder model, find the insecure states and verify the reachability of the insecure states. The theory and work flow of the method are illustrated by analysis of STS security protocol.
当前,系统的庞大和复杂化使得系统安全性能分析与验证问题变得越来越复杂并越来越引起人们的重视。提供有效的数学理论工具、直观的模型描述方法和有效的模型分析方法以及实用的辅助分析软件,是系统安全性能分析与验证所面临的迫切需要解决的问题,这也正是基于Petri网的安全策略分析与验证技术的核心。
从计算机系统、Web服务以及安全协议的安全需求和现实基础出发,对相关理论、协议、关键技术以及具体实现进行了广泛深入的研究。主要研究工作包括以下几个方面:
保密性策略和完整性策略是重要的安全策略,在许多军用和商用系统中得到广泛的应用。其代表模型分别是Bell-LaPadula模型和Biba模型,这两个模型是数学上的对偶。保密性策略用于防止信息的非授权泄漏,而完整性策略则是防止信息被非授权更改。对采用了特定安全模型的具体实用系统需要一个严格有效的方法对其保密性和完整性进行分析和验证。安全策略研究的一个关键问题是:用易于理解的和精确的形式表达策略。因此,提出了利用Petri网对安全策略进行描述,Petri网不仅适合策略的表达,而且可用于系统分析,以确定所定义的机制是否符合策略定义。
对于一个安全策略,首先建立基于Petri网的形式化描述,然后就可以根据形式化的描述对实施了特定安全模型的进程或系统进行分析与验证。分别对Bell-LaPadula保密性模型和Biba完整性模型进行了描述。给出了这两个模型基于Petri网的形式化定义,并对实施了这两个安全模型的相应示例进程进行了分析和验证。显示出Petri网不仅能够用用易于理解的和精确的形式表达安全策略,而且可用于系统分析和验证。Petri网的覆盖图则在自动分析大型复杂系统方面很有用处。
为了对实施了中国墙模型的系统进行分析与验证,提出了一种基于有色Petri网的混合安全策略分析方法。中国墙模型是一种兼顾保密性和完整性的混合安全模型。中国墙模型的显著特征是自由选择和强制性访问控制的结合。首先,对中国墙模型进行了非形式化的描述,并且将中国墙模型与其他安全模型进行了比较。然后,给出了中国墙模型基于有色Petri网的形式化定义。其突出特征在于,引入了“控制库所”的概念以解决跟踪主体访问记录的问题。并且“控制库所”代替访问控制矩阵,与单个主体关联,不需要集中存储,更加适合在分布式环境下部署。最后,根据中国墙模型基于有色Petri网的定义,通过对一个实施了中国墙模型的示例进程进行分析与验证,阐述了如何通过基于有色Petri网的形式化定义和覆盖图分析和验证实施了中国墙模型的系统的行为。
当前的互联网正在经历着一些重要的变化,它已经成为了一个Web服务的载体,而不仅仅是一个信息的容器。Web服务提供了一个语言中立,连接松散,独立于平台的方式,使得散布在互联网上的各组织和企业内部的应用程序可以连接起来。Web服务合成可以让我们将许多现有的Web服务结合起来,形成一个新的,增值的Web服务。可靠的Web服务合成需要建模的技术和工具。因此,提出了一个基于有色Petri网的Web服务合成模型。这个模型为Web服务合成提供了充分的表达能力,能够直接变换为可执行的合成定义,并且独立于可执行的合成语言。基于Petri网的Web服务合成模型还可以利用Petri网的分析和验证能力对合成服务进行安全分析和验证。
首先,对Web服务建立了有色Petri网模型(服务网),然后在此定义的基础上给出了四种基本Web服务合成结构:顺序结构,并发结构,选择结构,和循环结构以及一种高级合成结构置换结构的形式化定义。并且还定义了一个具有封闭性的Web服务合成算法。最后,根据基于Petri网的形式化验证方法对此Web服务合成模型的可用性,保密性,完整性以及混合安全性进行了分析和验证,得出了一些有用的结论。
20年来,安全协议研究的进展十分可喜,取得了丰富的研究成果。特别是20世纪90年代以来,研究取得突破性进展,对安全协议若干本质性的问题有了更为深刻的认识。但是,这一领域还有许多问题有待解决。特别是形式化分析领域。因此,提出了一种基于有色Petri网的安全协议分析验证方法,该方法分为4个步骤:建立安全协议的Petri模型,建立入侵模型,找出不安全状态,验证不安全状态的可达性。并且通过对STS协议在特定攻击模式下的分析演示了该方法的工作原理和流程。
With the rapidly development of science and technology, information technology has had an influence on the way we work and on society in general. Information technology is more and more becoming the requisite tools for gathering, processing, storing and exchanging information with computers. We are more and more relying on computer systems. However, the data stored in systems, transferred and exchanged on networks is valuable. When the information is unauthorized accessed, intercepted or modified, the problems of computer security are coming out.
Nowadays, huge and complex systems make the security analysis and verification become more complex and get more concerned. Security analyzing and verifying systems needs available mathematical tools, visual model describing and analyzing methods and practical assistant software. And that is the core element for the security analysis and verification technology based on Petri nets.
Based on realistic requirements and foundations, this thesis engaged in extensive research on some relevant theories, protocols and key technologies. The main contributions are as follows:
Confidentiality policy and integrity policy are important security policies, implemented in many militarily and commercial systems. Bell-LaPadula model and Biba model are mathematical dual. A confidentiality policy prevents the unauthorized disclosure of information, and an integrity policy prevents the unauthorized modification of information. Both security models and practical systems need an available method to conduct security analysis and verification. One of the most important issues in security policies research is: to describe the policies in precise and easily understand form.
Thus, this thesis proposes a method to describe security policies by Petri nets. Petri nets are not only good for define policies, but also well for system analysis to verify that the system mechanisms are corresponding with the definitions. For a security policy, firstly build the Petri net-based model and formal definitions of the model, and then The Petri net-based definitions and the coverability graph allow one to analyze and verify the security policy in Petri net model of a system. In this thesis, the Petri net-based definitions of Bell-LaPadula model and Biba Model are formally described in detail. Subsequently, examples of the confidentiality policy and integrity policy are illustrated and the conclusions show that Petri net is not only a concise graphic analysis method, but also suited to formal verification.
For analyzing and verifying systems implemented with Chinese Wall policy, this thesis proposes a Petri net-based method to analyze hybrid policy. The Chinese Wall model is a model of a security policy that refers equally to confidentiality and integrity. The important feature of the Chinese Wall policy is the combination of discretionary access control and mandatory access control. Firstly, the Chinese Wall policy is informally described, and compared with other security policies. And then, the Petri net-based formal definitions are given. The main contribution of the definitions is the concept of "control place", which is used to trace the access record of subjects. The access control matrix is replaced by control place, which is associated with single subject and suited for implementation in distributed environment. Finally, the analysis and verification of the Chinese Wall policy by the method are addressed through a sample system.
The Internet is going through several major changes. It has become a vehicle of Web services rather than just a repository of Information. Web services provide a language-neutral, loosely coupled, and platform-independent way for linking applications within organizations or enterprises across the Internet. Web services composition allows us to combine a number of existing Web services into a new, value-added Web service.
Therefore, there is a need for modeling techniques and tools for reliable Web service composition. This thesis proposes a Colored Petri net-based model for Web service composition. This model is sufficiently expressive for Web service composition, can be transformed to directly executable composition specification; and is independent of the executable composition languages. Firstly, we model web service as colored Petri net (service net), based on which four basic composition construct and one advance composition construct are formally defined. Subsequently, we present the algebra that allows the creation of new value-add Web services using existing ones as building blocks. Finally, the colored Petri net-based web service composition model is verified on availability, confidentiality and integrity, and reaches some useful conclusions.
In recent twenty years, the research on security protocols has made great achievements. Especially from 1990's, some breakthroughs made us better understand several essential issues of security protocols. However, many problems need to be solved in this field, especially in formal analysis. Thus, this thesis proposes a Petri net-based method to analyze and verify security protocols. There are 4 steps: describe the protocol in a colored Petri net form, describe the intruder model, find the insecure states and verify the reachability of the insecure states. The theory and work flow of the method are illustrated by analysis of STS security protocol.
引文
[1] C. A. Petri. Kommunikation mit Automaten. PhD thesis, Institut für instrumentelle Mathematik der Universit?t Bonn, 1962
[2] C. A. Petri. State Transition Structures in Physics and in Computation. International Journal of Theoretical Physics, Vol. 21(12): 979~992, 1982
[3] C. A. Petri. Nets, Time and Space. Theoretical Computer Science, Vol. 153(1-2): 3~48, 1996
[4] T. Murata. Petri Nets: Properties, Analysis and Applications. Proceedings of the IEEE, 77(4): 541~580, 1989
[5] C. Girault, R. Valk. Petri Nets for System Engineering: A Guide to Modeling, Verification and Application. Springer-Verlag, 2003
[6]袁崇义. Petri网原理与应用.北京:电子工业出版社. 2005
[7] K. Jensen. An Introduction to the Theoretical Aspects of Colored Petri Nets. A Decade of Concurrency, LNCS 803. New York, USA: Springer Verlag. 230~272, 1994
[8] K. Jensen. Colored Petri Nets: A High-level Language for System Design and Analysis. In: G. Rozenberg (ed.): Advances in Petri Nets 1990, LNCS 483, Springer-Verlag. 342~416, 1991
[9] K. Jensen. Colored Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Vol. 1: Basic Concepts, 1992. Vol. 2: Analysis Methods, 1994. Vol. 3: Practical Use, 1997. Monographs in Theoretical Computer Science, Springer-Verlag
[10] J. L. Peterson. Petri Nets Theory and the Modeling of Systems. Eaglewood Cliffs, NJ: Prentice-Hall, Inc., 1981
[11] W. Reisig, Petri Nets, EATCS Monographs on Theoretical Computer Science, Vol. 4. New York: Springer-Verlag, 1985
[12] ISO/IEC 15909-1: 2004 Software and system engineering - High-level Petri nets - Part 1: Concepts, definitions and graphical notation. 2004
[13] D. Bell and L. LaPadula. Secure Computer Systems: Mathematical Foundations. Technical Report MTR-2547, Vol. I, MITRE Corporation, Bedford, MA. 1973
[14] D. Bell and L. LaPadula. Secure Computer System: Unified Exposition and Multics Interpretation. Technical Report MTR-2997, Rev. 1, MITRE Corporation, Bedford, MA. 1975
[15] Department of Defense. Trusted Computer System Evaluation Criteria, DOD 5200.28-STD. 1985
[16] S. Jajodia and R. Sandhu. Towards a Multilevel Secure Relational Data Model. Proceedings of the ACM-SIGMOD Conference, 50~59, 1991
[17] C. Landwehr, C. Heitmeyer and J. Mclean. A Security Model for Military Message Systems. ACM Transactions on Computer Systems 2(2): 198~222, 1984
[18] L. Dion. A Complete Protection Model. Proceedings of the 1981 IEEE Symposium on Security and Privacy, 49~55, 1981
[19] D. Sidhu and M. Gasser. A Multilevel Secure Local Area Network. Proceedings of the 1982 IEEE Symposium on Security and Privacy, 137~143, 1982
[20] S. Lipner. Non-Discretionary Controls for Commercial Applications. Proceedings of the 1982 Symposium on Privacy and Security, 2~10, 1982
[21] K. Biba. Integrity Considerations for Secure Computer Systems. Technical Report MTR-3153, MITRE Corporation, Bedford, MA. 1977
[22] M. Pozzo and T. Gray. A Model for the Containment of Computer Viruses. Proceedings of the AIAA/ASIS/DODCI 2nd Aerospace Computer Security Conference, 11~18, 1986
[23] M. Pozzo and T. Gray. An Approach to Containing Computer Viruses. Computers and Security 6(4): 321~331, 1987
[24] G. Popek and B. Walker. The LOCUS Distributed System Architecture. The MITPress, Cambridge, MA, 1985
[25] M. Huth and M. Ryan. Logic in Computer Science: Modeling and Reasoning About Systems. Cambridge University Press, Cambridge, UK, 2000
[26] M. Burrows, M. Abadi and R. Needham. A Logic of Authentication. ACM Transactions on Computer Systems 8(1): 18~36, 1990
[27] J. McLean. Twenty Years of Formal Methods. Proceedings of the 1999 IEEE Symposium on Security and Privacy, 115~116, 1999
[28] B. Snow. The Future Is Not Assured– But It Should Be. Proceedings of the 1999 IEEE Symposium on Security and Privacy, 240~241, 1999
[29] J. Wing. A Symbiotic Relationship between Formal Methods and Security. Proceedings of Computer Security, Dependability, and Assurance: From Needs to Solutions, 26~38, 1998
[30] J. Bowen and H. Hinchley. Ten Commandments of Formal Methods. IEEE Computer 28(4): 56~63, 1995
[31] J. Bowen and H. Hinchley. Seven More Myths of Formal Methods. IEEE Software 12(4): 34~41, 1995
[32] M. Kaufmann and J. Moore. ACL2: An Industrial Strength Version of Nqthm. Proceedings of the 11th Annual Conference on Computer Assurance, 23~34, 1996
[33] K. Turner (eds.). Using Formal Description Techniques: An Introduction to Estelle, LOTOS and SDL. John Wiley and Sons, Chichester, UK, 1993
[34] M. Gordon and T. Melham (eds.). Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge, UK, 1993
[35] T. Bolognesi and E. Brinksma. Introduction to the ISO Specification Language LOTOS. Computer Networks 14(1): 25~59, 1988
[36] A. Diller. Z: An Introduction to Formal Methods. Wiley, Chichester, UK, 1990
[37] M. Ardis, J. Chaves, L. Jagadeesan, P. Mataga, C. Puchol, M. Staskauskas and J. vonOlnhausen. A Framework for Evaluating Specification Methods for Reactive Systems Experience Report. IEEE Transactions on Software Engineering 22(6): 378~389, 1996
[38] S. Atkinson and D. Scholefield. Transformational vs. Reactive Refinement in Real-Time Systems. Information Processing Letters 55(4): 201~210, 1995
[39] M. Cheheyl, M. Gasser, G. Huff and J. Millen. Verifying Security. Computing Surveys 13(3): 279~339, 1981
[40] P. Neumann, R. Feiertag, L. Robinson and K. Levitt. Software Development and Proofs of Multi-Level Security. Proceedings of the 2nd International Conference on Software Engineering, 421~428, 1976
[41] S. Owre, J. Rushby and N. Shankar. PVS: A Prototype Verification System. Proceedings of the 11th International Conference on Automated Deduction, 748~752, 1992
[42] J. Burch, E. Clarke, K. McMillan, D. Dill and L. Hwang. Symbolic Model Checking: 1020 States and Beyond. Information and Computation 98(2): 142~170, 1992
[43] E. Clarke, E. Emerson and A. Sistla. Axiomatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Language and Systems 1(2): 244~263, 1986
[44] J. Burch, E. Calrke, D. Long, K. McMillan and D. Dill. Symbolic Model Checking for Sequential Circuit Verification. IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems 13(4): 401~424, 1994
[45] S. Campos, E. Clarke and M. Minea. Symbolic Technique for Formally Verifying Industrial Systems. Science of Computer Programming 29(1-2): 79~98, 1997
[46] E. Clarke, S. Jha and W. Marrero. Using State Space Exploration and a Natural Deduction Style Message Derivation Engine to Verify Security Protocols. Proceedings of the IFIP Working Conference on Programming Concepts and Methods, 87~106, 1998
[47] S. Campos, E. Clarke, W. Marrero and M. Minea. Verus: A Tool for Quantitative Analysis of Finite-State Real-Time Systems. Proceedings of the ACM SIGPLAN 1995 Workshop on Language, Compilers and Tools for Real-Time Systems, 70~78, 1995
[48] G. Holzmann. The Model Checker SPIN. IEEE Transactions on Software Engineering 23(5): 1~17, 1997
[49] A. Roscoe. Modeling and Verifying Key-Exchange Protocols Using CSP and FDR. Proceedings of the 8th IEEE Computer Security Foundations Workshop, 98~107, 1995
[50] S. Berezin and A. Groce. SyMP: The User’s Guide. Computer Sience Dept., Carnegie Mellon University, 2000
[51] C. Meadows. The NRL Protocol Analyzer: An Overview. Journal of Logic Programming 26(2): 113~131, 1996
[52] W. Clocksin and C. Mellish. Programming in Prolog. Springer-Verlag, New York, NY, 1981
[53] D. Dolev and A. Yao. On the Security of Public Key Protocols. IEEE Transactions on Information Theory 29(2): 198~208, 1983
[54] C. Meadows. Analysis of the Internet Key Exchange Protocol Using the NRL Protocol Analyzer. Proceedings of the 1999 IEEE Symposium on Security and Privacy, 216~231, 1999
[55] C. Meadows. Analyzing the Needham-Schroeder Public Key Protocol: A Comparison of Two Approaches. Proceedings of the 4th European Symposium on Research in Computer Security, 351~364, 1996
[56] Commission of the European Communities. Information Technology Security Evaluation Criteria, Version 1.2, 1991
[57] National Institute of Standards and Technology, Common Criteria for Information Technology Security Evaluation, Part 1: Introduction and General Model, Version2.1, CCIMB-99-031, 1999
[58] National Institute of Standards and Technology, Common Criteria for Information Technology Security Evaluation, Part 2: Security Function Requirement, Version 2.1, CCIMB-99-031, 1999
[59] National Institute of Standards and Technology, Common Criteria for Information Technology Security Evaluation, Part 3: Security Assurance Requirements, Version 2.1, CCIMB-99-031, 1999
[60] Canadian System Security Center. The Canadian Trusted Computer Product Evaluation Criteria, Version 3.0e, 1993
[61] National Institute of Standards and Technology and National Security Agency. Federal Criteria for Information Technology Security, Version 1.0, 1992
[62] K. Cutler and F. Jones. Commercial International Security Requirements, draft, 1991
[63] National Institute of Standards and Technology. Security Requirements for Cryptographic Modules. FIPS PUB 140-2, 2001
[64] IBM Web Services Architecture Team. Web Services architecture overview. The next stage of evolution for e-business. New York, USA: IBM Corporation, 2000
[65] J. P. Thomas, M. Tomas and G. Ghinea. Modeling of Web Services Flow. IEEE International Conference on E-Commerce. California, USA: IEEE Press, 391~398, 2003
[66] C. Szyperski. Component Software. New York, USA: Addison-Wesley, 1998
[67] A. Rettberg and W. Thronicke. Embedded System Design Based on Web Services. Proceedings of Design, Automation and Test in Europe Conference and Exhibition. Paris, France: Le Palais des Congres, 232~237, 2002
[68] Sun Haiyan, Wang Xiaodong, Zhou Bin, et al. Research and Implementation of Dynamic Web Services Composition. Lecture Notes in Computer Science 2834: 457~466, 2003
[69] D. Chakraborty and A. Joshi. Dynamic Service Composition: State of the Art andResearch Directions. Department of Computer Science and Electrical Engineering, University of Maryland, USA, 2001
[70] D. Chakraborty, F. Perich, A. Joshi, et al. A Reactive Service Composition Architecture for Pervasive Computing Environments. Proceedings of the IFIP TC6/WG6.8 Working Conference on Personal Wireless Communications, 53~62, 2002
[71] W. Aalst, M. Dumas and A. Hofsted. Web Service Composition Languages: Old Wine in New Bottles. Proceedings of the 29th EUROMNICRO Conference“New Waves in System Architecture”, 298~307, 2003
[72] P. F. Pires, M. R. Benevides and M. Mattoso. Building Reliable Web Services Compositions. Lecture Notes in Computer Science 2593: 59~72, 2003
[73] S. McIlraith and T. C. Son. Adapting Golog for Composition of Semantic Web Services. Proceedings of KRR, 482~493, 2002
[74] B. Limthanmaphon, Y. Zhang. Web Service Composition with Case-based Reasoning. Proceedings of the 14th Australasian Database Conference. Adelaide, Australia: Australian Computer Society, 201~208, 2003
[75] N. Milanovic and M. Malek. Current solutions for Web service composition. IEEE Internet Computing 8(6): 51~59, 2004
[76] Yang Jian and M. P. Papazoglou. Web Component: A Substrate for Web Service Reuse and Composition. Lecture Notes in Computer Science 2348: 21~36, 2002
[77] Chun Soon Ae, Lee Yugyung and Geller James. Ontological and Pragmatic Knowledge Management for Web Service Composition. Lecture Notes in Computer Science 2973: 365~373, 2004
[78]岳昆,王晓玲,周傲英. Web服务核心支撑技术:研究综述.软件学报15(3): 428~442, 2004
[79] Hamadi R., Benatallah B. A Petri Net-Based Model for Web Service Composition. Proceedings of the 14th Australasian Database Conference. Adelaide, Australia:Australian Computer Society, 191~200, 2003
[80] Tan Z., Lin C., Yin H., Hong Y., Zhu G. Approximate Performance Analysis of Web Services Flow Using Stochastic Petri Net. Proceedings of Grid and Cooperative Computing (GCC 2004), LNCS 3251. Berlin Heidelberg: Springer Verlag, 193~200, 2004
[81] Schuster H., Georgakopoulos D., Cichocki A., Baker D. Modeling and Composing Service-based and Reference Process-based Multi-enterprise Processes. Advanced Information Systems Engineering, 12th International Conference CAiSE 2000, LNCS 1789. Stockholm, Sweden: Springer Verlag, 247~263, 2000
[82] Narayanan S., McIlraith S. Analysis and simulation of Web Services. Computer Networks, 2003, 42(5): 675~693
[83] D. Brewer and M. Nash. The Chinese Wall Security Policy. Proceedings of the 1989 IEEE Symposium on Security and Privacy, 206~214, 1989
[84] C. Meadows. Extending the Brewer-Nash Model to a Multilevel Context. Proceedings of the 1990 IEEE Symposium on Research in Security and Privacy, 95~102, 1990
[85] T. Lin. Chinese Wall Security Policy– An Aggressive Model. Proceedings of the 5th Annual Computer Security Conference, 282~289, 1989
[86] D. Clark and D. Wilson. A Comparison of Commercial and Military Security Policies. Proceedings of the 1987 IEEE Symposium on Security and Privacy, 184~194, 1987
[87]卿斯汉.安全协议20年研究进展.软件学报, 14(10): 1740~1752, 2003
[88] R. Needham and M. Schroeder. Using Encryption for Authentication in Large Networks of Computers. Communications of the ACM, 21(12):993~999, 1978
[89] J. Clark and J. Jacob. A Survey of Authentication Protocol Literature: Version 1.0. 1997. http://www-users.cs.york.ac.uk/~jac/under the link \Security Protocols Review
[90] S. Gritzalis, D. Spinellis, and P. Georgiadis. Security protocols over open networksand distributed systems: Formal methods for their analysis, design, and verification. Computer Communications, 22(8):695~707, May 1999
[91] I. Cervesato, N. Durgin, P. Lincoln and J. Mitchell. A Meta-notation for Protocol Analysis. Proceedings of the 1999 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 55~69, 1999
[92] J. Millen. The Interrogator Model. Proceedings of the 1995 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 251~260, 1995
[93] R. Kemmerer, C. Meadows and J. Millen. Three Systems for Cryptographic Protocol Analysis. Journal of Cryptology, 7(2): 251~260, 1994
[94] L. C. Paulson. Mechanized Proofs for a Recursive Authentication Protocol. Proceedings of the 10th IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 84~94, 1997
[95] L. C. Paulson. The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security, (6):85~128, 1998
[96] W. Diffie and M. Hellman. New directions in cryptography. IEEE Transactions on Information Theory, vol. 22(6), 644~654, 1976
[97] W. Diffie, P. van Oorschot and M. Wiener. Authentication and Authenticated Key Exchange. Designs, Codes and Cryptography, 2, 107~125, 1992
[98] G. Lowe. Some New Attacks upon Security Protocols. Proceedings of the 9th IEEE Computer Security Foundations Workshop. IEEE Press, 162~169, 1996
[2] C. A. Petri. State Transition Structures in Physics and in Computation. International Journal of Theoretical Physics, Vol. 21(12): 979~992, 1982
[3] C. A. Petri. Nets, Time and Space. Theoretical Computer Science, Vol. 153(1-2): 3~48, 1996
[4] T. Murata. Petri Nets: Properties, Analysis and Applications. Proceedings of the IEEE, 77(4): 541~580, 1989
[5] C. Girault, R. Valk. Petri Nets for System Engineering: A Guide to Modeling, Verification and Application. Springer-Verlag, 2003
[6]袁崇义. Petri网原理与应用.北京:电子工业出版社. 2005
[7] K. Jensen. An Introduction to the Theoretical Aspects of Colored Petri Nets. A Decade of Concurrency, LNCS 803. New York, USA: Springer Verlag. 230~272, 1994
[8] K. Jensen. Colored Petri Nets: A High-level Language for System Design and Analysis. In: G. Rozenberg (ed.): Advances in Petri Nets 1990, LNCS 483, Springer-Verlag. 342~416, 1991
[9] K. Jensen. Colored Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Vol. 1: Basic Concepts, 1992. Vol. 2: Analysis Methods, 1994. Vol. 3: Practical Use, 1997. Monographs in Theoretical Computer Science, Springer-Verlag
[10] J. L. Peterson. Petri Nets Theory and the Modeling of Systems. Eaglewood Cliffs, NJ: Prentice-Hall, Inc., 1981
[11] W. Reisig, Petri Nets, EATCS Monographs on Theoretical Computer Science, Vol. 4. New York: Springer-Verlag, 1985
[12] ISO/IEC 15909-1: 2004 Software and system engineering - High-level Petri nets - Part 1: Concepts, definitions and graphical notation. 2004
[13] D. Bell and L. LaPadula. Secure Computer Systems: Mathematical Foundations. Technical Report MTR-2547, Vol. I, MITRE Corporation, Bedford, MA. 1973
[14] D. Bell and L. LaPadula. Secure Computer System: Unified Exposition and Multics Interpretation. Technical Report MTR-2997, Rev. 1, MITRE Corporation, Bedford, MA. 1975
[15] Department of Defense. Trusted Computer System Evaluation Criteria, DOD 5200.28-STD. 1985
[16] S. Jajodia and R. Sandhu. Towards a Multilevel Secure Relational Data Model. Proceedings of the ACM-SIGMOD Conference, 50~59, 1991
[17] C. Landwehr, C. Heitmeyer and J. Mclean. A Security Model for Military Message Systems. ACM Transactions on Computer Systems 2(2): 198~222, 1984
[18] L. Dion. A Complete Protection Model. Proceedings of the 1981 IEEE Symposium on Security and Privacy, 49~55, 1981
[19] D. Sidhu and M. Gasser. A Multilevel Secure Local Area Network. Proceedings of the 1982 IEEE Symposium on Security and Privacy, 137~143, 1982
[20] S. Lipner. Non-Discretionary Controls for Commercial Applications. Proceedings of the 1982 Symposium on Privacy and Security, 2~10, 1982
[21] K. Biba. Integrity Considerations for Secure Computer Systems. Technical Report MTR-3153, MITRE Corporation, Bedford, MA. 1977
[22] M. Pozzo and T. Gray. A Model for the Containment of Computer Viruses. Proceedings of the AIAA/ASIS/DODCI 2nd Aerospace Computer Security Conference, 11~18, 1986
[23] M. Pozzo and T. Gray. An Approach to Containing Computer Viruses. Computers and Security 6(4): 321~331, 1987
[24] G. Popek and B. Walker. The LOCUS Distributed System Architecture. The MITPress, Cambridge, MA, 1985
[25] M. Huth and M. Ryan. Logic in Computer Science: Modeling and Reasoning About Systems. Cambridge University Press, Cambridge, UK, 2000
[26] M. Burrows, M. Abadi and R. Needham. A Logic of Authentication. ACM Transactions on Computer Systems 8(1): 18~36, 1990
[27] J. McLean. Twenty Years of Formal Methods. Proceedings of the 1999 IEEE Symposium on Security and Privacy, 115~116, 1999
[28] B. Snow. The Future Is Not Assured– But It Should Be. Proceedings of the 1999 IEEE Symposium on Security and Privacy, 240~241, 1999
[29] J. Wing. A Symbiotic Relationship between Formal Methods and Security. Proceedings of Computer Security, Dependability, and Assurance: From Needs to Solutions, 26~38, 1998
[30] J. Bowen and H. Hinchley. Ten Commandments of Formal Methods. IEEE Computer 28(4): 56~63, 1995
[31] J. Bowen and H. Hinchley. Seven More Myths of Formal Methods. IEEE Software 12(4): 34~41, 1995
[32] M. Kaufmann and J. Moore. ACL2: An Industrial Strength Version of Nqthm. Proceedings of the 11th Annual Conference on Computer Assurance, 23~34, 1996
[33] K. Turner (eds.). Using Formal Description Techniques: An Introduction to Estelle, LOTOS and SDL. John Wiley and Sons, Chichester, UK, 1993
[34] M. Gordon and T. Melham (eds.). Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge, UK, 1993
[35] T. Bolognesi and E. Brinksma. Introduction to the ISO Specification Language LOTOS. Computer Networks 14(1): 25~59, 1988
[36] A. Diller. Z: An Introduction to Formal Methods. Wiley, Chichester, UK, 1990
[37] M. Ardis, J. Chaves, L. Jagadeesan, P. Mataga, C. Puchol, M. Staskauskas and J. vonOlnhausen. A Framework for Evaluating Specification Methods for Reactive Systems Experience Report. IEEE Transactions on Software Engineering 22(6): 378~389, 1996
[38] S. Atkinson and D. Scholefield. Transformational vs. Reactive Refinement in Real-Time Systems. Information Processing Letters 55(4): 201~210, 1995
[39] M. Cheheyl, M. Gasser, G. Huff and J. Millen. Verifying Security. Computing Surveys 13(3): 279~339, 1981
[40] P. Neumann, R. Feiertag, L. Robinson and K. Levitt. Software Development and Proofs of Multi-Level Security. Proceedings of the 2nd International Conference on Software Engineering, 421~428, 1976
[41] S. Owre, J. Rushby and N. Shankar. PVS: A Prototype Verification System. Proceedings of the 11th International Conference on Automated Deduction, 748~752, 1992
[42] J. Burch, E. Clarke, K. McMillan, D. Dill and L. Hwang. Symbolic Model Checking: 1020 States and Beyond. Information and Computation 98(2): 142~170, 1992
[43] E. Clarke, E. Emerson and A. Sistla. Axiomatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Language and Systems 1(2): 244~263, 1986
[44] J. Burch, E. Calrke, D. Long, K. McMillan and D. Dill. Symbolic Model Checking for Sequential Circuit Verification. IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems 13(4): 401~424, 1994
[45] S. Campos, E. Clarke and M. Minea. Symbolic Technique for Formally Verifying Industrial Systems. Science of Computer Programming 29(1-2): 79~98, 1997
[46] E. Clarke, S. Jha and W. Marrero. Using State Space Exploration and a Natural Deduction Style Message Derivation Engine to Verify Security Protocols. Proceedings of the IFIP Working Conference on Programming Concepts and Methods, 87~106, 1998
[47] S. Campos, E. Clarke, W. Marrero and M. Minea. Verus: A Tool for Quantitative Analysis of Finite-State Real-Time Systems. Proceedings of the ACM SIGPLAN 1995 Workshop on Language, Compilers and Tools for Real-Time Systems, 70~78, 1995
[48] G. Holzmann. The Model Checker SPIN. IEEE Transactions on Software Engineering 23(5): 1~17, 1997
[49] A. Roscoe. Modeling and Verifying Key-Exchange Protocols Using CSP and FDR. Proceedings of the 8th IEEE Computer Security Foundations Workshop, 98~107, 1995
[50] S. Berezin and A. Groce. SyMP: The User’s Guide. Computer Sience Dept., Carnegie Mellon University, 2000
[51] C. Meadows. The NRL Protocol Analyzer: An Overview. Journal of Logic Programming 26(2): 113~131, 1996
[52] W. Clocksin and C. Mellish. Programming in Prolog. Springer-Verlag, New York, NY, 1981
[53] D. Dolev and A. Yao. On the Security of Public Key Protocols. IEEE Transactions on Information Theory 29(2): 198~208, 1983
[54] C. Meadows. Analysis of the Internet Key Exchange Protocol Using the NRL Protocol Analyzer. Proceedings of the 1999 IEEE Symposium on Security and Privacy, 216~231, 1999
[55] C. Meadows. Analyzing the Needham-Schroeder Public Key Protocol: A Comparison of Two Approaches. Proceedings of the 4th European Symposium on Research in Computer Security, 351~364, 1996
[56] Commission of the European Communities. Information Technology Security Evaluation Criteria, Version 1.2, 1991
[57] National Institute of Standards and Technology, Common Criteria for Information Technology Security Evaluation, Part 1: Introduction and General Model, Version2.1, CCIMB-99-031, 1999
[58] National Institute of Standards and Technology, Common Criteria for Information Technology Security Evaluation, Part 2: Security Function Requirement, Version 2.1, CCIMB-99-031, 1999
[59] National Institute of Standards and Technology, Common Criteria for Information Technology Security Evaluation, Part 3: Security Assurance Requirements, Version 2.1, CCIMB-99-031, 1999
[60] Canadian System Security Center. The Canadian Trusted Computer Product Evaluation Criteria, Version 3.0e, 1993
[61] National Institute of Standards and Technology and National Security Agency. Federal Criteria for Information Technology Security, Version 1.0, 1992
[62] K. Cutler and F. Jones. Commercial International Security Requirements, draft, 1991
[63] National Institute of Standards and Technology. Security Requirements for Cryptographic Modules. FIPS PUB 140-2, 2001
[64] IBM Web Services Architecture Team. Web Services architecture overview. The next stage of evolution for e-business. New York, USA: IBM Corporation, 2000
[65] J. P. Thomas, M. Tomas and G. Ghinea. Modeling of Web Services Flow. IEEE International Conference on E-Commerce. California, USA: IEEE Press, 391~398, 2003
[66] C. Szyperski. Component Software. New York, USA: Addison-Wesley, 1998
[67] A. Rettberg and W. Thronicke. Embedded System Design Based on Web Services. Proceedings of Design, Automation and Test in Europe Conference and Exhibition. Paris, France: Le Palais des Congres, 232~237, 2002
[68] Sun Haiyan, Wang Xiaodong, Zhou Bin, et al. Research and Implementation of Dynamic Web Services Composition. Lecture Notes in Computer Science 2834: 457~466, 2003
[69] D. Chakraborty and A. Joshi. Dynamic Service Composition: State of the Art andResearch Directions. Department of Computer Science and Electrical Engineering, University of Maryland, USA, 2001
[70] D. Chakraborty, F. Perich, A. Joshi, et al. A Reactive Service Composition Architecture for Pervasive Computing Environments. Proceedings of the IFIP TC6/WG6.8 Working Conference on Personal Wireless Communications, 53~62, 2002
[71] W. Aalst, M. Dumas and A. Hofsted. Web Service Composition Languages: Old Wine in New Bottles. Proceedings of the 29th EUROMNICRO Conference“New Waves in System Architecture”, 298~307, 2003
[72] P. F. Pires, M. R. Benevides and M. Mattoso. Building Reliable Web Services Compositions. Lecture Notes in Computer Science 2593: 59~72, 2003
[73] S. McIlraith and T. C. Son. Adapting Golog for Composition of Semantic Web Services. Proceedings of KRR, 482~493, 2002
[74] B. Limthanmaphon, Y. Zhang. Web Service Composition with Case-based Reasoning. Proceedings of the 14th Australasian Database Conference. Adelaide, Australia: Australian Computer Society, 201~208, 2003
[75] N. Milanovic and M. Malek. Current solutions for Web service composition. IEEE Internet Computing 8(6): 51~59, 2004
[76] Yang Jian and M. P. Papazoglou. Web Component: A Substrate for Web Service Reuse and Composition. Lecture Notes in Computer Science 2348: 21~36, 2002
[77] Chun Soon Ae, Lee Yugyung and Geller James. Ontological and Pragmatic Knowledge Management for Web Service Composition. Lecture Notes in Computer Science 2973: 365~373, 2004
[78]岳昆,王晓玲,周傲英. Web服务核心支撑技术:研究综述.软件学报15(3): 428~442, 2004
[79] Hamadi R., Benatallah B. A Petri Net-Based Model for Web Service Composition. Proceedings of the 14th Australasian Database Conference. Adelaide, Australia:Australian Computer Society, 191~200, 2003
[80] Tan Z., Lin C., Yin H., Hong Y., Zhu G. Approximate Performance Analysis of Web Services Flow Using Stochastic Petri Net. Proceedings of Grid and Cooperative Computing (GCC 2004), LNCS 3251. Berlin Heidelberg: Springer Verlag, 193~200, 2004
[81] Schuster H., Georgakopoulos D., Cichocki A., Baker D. Modeling and Composing Service-based and Reference Process-based Multi-enterprise Processes. Advanced Information Systems Engineering, 12th International Conference CAiSE 2000, LNCS 1789. Stockholm, Sweden: Springer Verlag, 247~263, 2000
[82] Narayanan S., McIlraith S. Analysis and simulation of Web Services. Computer Networks, 2003, 42(5): 675~693
[83] D. Brewer and M. Nash. The Chinese Wall Security Policy. Proceedings of the 1989 IEEE Symposium on Security and Privacy, 206~214, 1989
[84] C. Meadows. Extending the Brewer-Nash Model to a Multilevel Context. Proceedings of the 1990 IEEE Symposium on Research in Security and Privacy, 95~102, 1990
[85] T. Lin. Chinese Wall Security Policy– An Aggressive Model. Proceedings of the 5th Annual Computer Security Conference, 282~289, 1989
[86] D. Clark and D. Wilson. A Comparison of Commercial and Military Security Policies. Proceedings of the 1987 IEEE Symposium on Security and Privacy, 184~194, 1987
[87]卿斯汉.安全协议20年研究进展.软件学报, 14(10): 1740~1752, 2003
[88] R. Needham and M. Schroeder. Using Encryption for Authentication in Large Networks of Computers. Communications of the ACM, 21(12):993~999, 1978
[89] J. Clark and J. Jacob. A Survey of Authentication Protocol Literature: Version 1.0. 1997. http://www-users.cs.york.ac.uk/~jac/under the link \Security Protocols Review
[90] S. Gritzalis, D. Spinellis, and P. Georgiadis. Security protocols over open networksand distributed systems: Formal methods for their analysis, design, and verification. Computer Communications, 22(8):695~707, May 1999
[91] I. Cervesato, N. Durgin, P. Lincoln and J. Mitchell. A Meta-notation for Protocol Analysis. Proceedings of the 1999 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 55~69, 1999
[92] J. Millen. The Interrogator Model. Proceedings of the 1995 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 251~260, 1995
[93] R. Kemmerer, C. Meadows and J. Millen. Three Systems for Cryptographic Protocol Analysis. Journal of Cryptology, 7(2): 251~260, 1994
[94] L. C. Paulson. Mechanized Proofs for a Recursive Authentication Protocol. Proceedings of the 10th IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 84~94, 1997
[95] L. C. Paulson. The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security, (6):85~128, 1998
[96] W. Diffie and M. Hellman. New directions in cryptography. IEEE Transactions on Information Theory, vol. 22(6), 644~654, 1976
[97] W. Diffie, P. van Oorschot and M. Wiener. Authentication and Authenticated Key Exchange. Designs, Codes and Cryptography, 2, 107~125, 1992
[98] G. Lowe. Some New Attacks upon Security Protocols. Proceedings of the 9th IEEE Computer Security Foundations Workshop. IEEE Press, 162~169, 1996