| Since many people are using the Internet to transfer important and sensitive data, network security is a major concern. Cryptographic protocols can be used to address security issues in network communications to ensure privacy, integrity and authentication.;Cryptographic protocols may contain flaws. Efficient and effective means of analyzing these protocol are required. In this thesis, cryptographic protocols are modeled and analyzed using a Petri Net Modeler, an integrated tool which employs a graphical user interface and a set of analysis methods. The construction of the modeler is based on the theory of Coloured Petri Nets. In this thesis, some features and functions are added to the Petri Net Modeler which make it feasible to model and analyze complex cryptographic protocols.;The methods used in analyzing the security properties of the CPN model of a cryptographic protocol employed in this thesis are the Reachability Search method and Matrix Equation Solution method. Software programs have been developed to perform these automated analyses which are an integral part of the Petri Net Modeler. Also, techniques are applied to reduce the complexity of the analysis.;Three protocols have been examined successfully: the Internet Key Exchange Protocol (IKE), the Secure Socket Layer Protocol (SSL), and the Secure Electronic Transaction Protocol (SET). The automated analysis verifies that there is a weakness in IKE operated under aggressive mode, and a weakness in SSL with one-way authentication. Suggestions are made to repair these protocols. After modifying the original protocols, the analysis is done again, the results of which show that the weaknesses have been removed. |
