| A methodology for the specification and analysis of cryptographic protocols originated from previous work at Queen's University. It involves representing the structure and behaviour of a cryptographic protocol using a Coloured Petri net. The structure of each legitimate protocol entity and the intruder is encapsulated using an element called a Petri Net Object (PNO). The intruder is an entity with some degree of control over the traffic in the communication channels, and represents the threat to a cryptographic protocol. It attempts to subvert the objectives of a protocol by storing, redirecting, passing and blocking messages, and constructing new ones to inject into the message flow. The Intruder PNO models this activity explicitly. Hand analysis is performed on the Coloured Petri net, examining each reachable system state, to find whether the modelled cryptographic protocol can withstand the attacks of the specified intruder.;This thesis extends the methodology. In most cases, hand analysis is not practical because of the large number of actions the intruder can pursue. Software has been developed to perform automated state-reachability analysis. With the software, exhaustive state analysis on a modern workstation is feasible for many protocols. Also, proposed techniques reduce the complexity of the analysis effort.;Changing the approach used to construct the Intruder PNO has strengthened the methodology by allowing it to model multiple iteration and parallel session attacks. In particular, our approach is able to show that a reflection attack can be executed on a single one-way authentication protocol. The prevention of the reflection attack is demonstrated through a slight modification of the protocol. The following protocols have also been examined: the handset authentication protocol used in CT2 and CT2Plus, a three-pass mutual authentication protocol from a proposal to ISO, and the Temporary Mobile Terminal Identity establishment protocol from the recommendations for FPLMTS. |
