| As the Internet grows in size, so do the risks. To make secure the traffic over the Internet, several cryptographic protocols have emerged over the last few years. However, the security objectives of a cryptographic protocol cannot be assured even though its underlying algorithms are secure. Thus, a means of efficiently and effectively analyzing these protocols is required.; In this thesis, we model and analyze protocols based on the formal method called Coloured Petri Nets (CPNs). The reachability property of the CPN methodology is used to construct a reachability graph from a CPN system. By examining the terminal states of the reachability graph, whether or not the protocol violates its security objectives can be determined. The existence of insecure terminal states indicates that attacks can be performed by an intruder. A matrix equation analysis can then be adopted to discover an intruder-influenced path to identify possible attacks. The flawed protocol can be modified until no insecure terminal state remains in the reachability graph.; A graphical integrated simulation tool, namely, the Petri Net Modeler (PNM) is used for automatically modeling protocols and conducting reachability analysis. Exhaustive reachability search of the state space has been implemented and integrated into the PNM in this thesis. To reduce state space explosion and speed up analysis, a reduced reachability search based on the stubborn set theory has also been developed.; Applying our methodology, we have analyzed the OAKLEY protocol and the ONC (Open Network Computing) RPC (Remote Procedure Call) protocol. The analysis unveils some flaws in these protocols and modifications are proposed to fix, the flawed protocols. |
