This paper extends the Petri net methodology for the specification and analysis of cryptographic protocols. In particular, software to perform automated state-reachability analysis has been developed. The intruder and each legitimate protocol entity is modeled by a Petri Net Object (PNO). The goal of the analysis is to determien whether a cryptographic protocol can withstand the attacks of the specified intruder. hand analysis is not practical in most cases because of the large number of actions the intruder may pursue. However, exhaustive state analysis on a modern work-station is feasible for many protocols. Previous work is extended to model multiple iteration and parallel session attacks. The following protocols have been examined: a simple one-way authentication protocol, 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.
展开▼
