| With the great expansion of our communication system over the last decade, cellular phone and Internet users are demanding better mechanisms to provide privacy and authentication. Cryptographic protocols are being applied to protect these sensitive areas of communications. The design of these protocols must be done error-free and resistant to attacks.;Formal analysis methods have been developed to verify the security properties of these cryptographic protocols. This thesis applies coloured Petri nets (CPN) to model protocols and intruders. From the resulting model, a security analysis may be conducted to determine the reachability of an undesirable end state from an initial state. As the reachability analysis is not feasible manually, automated analysis has been implemented.;An integrated software tool has been developed with the Java programming language to ensure that security objectives of cryptographic protocols are met. The tool has a graphical user interface as a front-end, rendering it user-friendly. This formal analysis tool permits a cryptographic protocol designer to specify a protocol using a drawing tool, to conduct a detailed security analysis, and to graphically simulate the operation of the protocol or its weaknesses.;To confirm that the software tool functions properly, security analysis was conducted on two authentication protocols: the Unique Challenge/Response protocol of the IS-41C standard and the Needham-Schroeder protocol. The published weaknesses for both protocols were confirmed by the software tool through analysis and interactive simulation.;After specifying a cryptographic protocol with a CPN diagram, the software tool succeeded in verifying the security properties of the protocol simply and quickly. |
