Research On The Theory Of Petri Net Based Analysis And Verification Of Security Policies

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.