Efficient analysis of cryptographic protocols in wireless communication systems

by Zhao, Weimin

Wireless Communications are becoming more prevdent in society, providing convenient, mobile telecommunications. However, due to the nature of the radio interface of wireless communications, security of the wireless link is a major concern. Crypt* graphic protocols can be used to address security issues in wireless communications, such as princy and authentication. Cryptographic protocols may contain flaws. EfEcient and effective means of analyzing these protocols are required. In this thesis, a methodology is presented for examining security properties of cryptographic protocols. Cryptographic protocols are modeled systematically using a formal method, namely, Coloured Petri Nets (CPNs). The CPN mode1 employed also includes an intruder, capable of intercepting and modifying messages, placed between protocol entities. Security properties of the CPN mode1 of a protocol are then determined using reachability analysis. A software program for the analysis has been developed to perform the reachability search. A method of reducing the complexity of the analysis, using so called stubborn sets, is proposed. The automated adysis not only verifies whether the analyzed protocol has flaws but also suggests how to repair it if flaws exist. Applying our methodology, the following protocols have been examined successfully: the Neuman-Stubblebine authent ication protocol, the MSAT terminal authentication protocol, and the IMT terminal identity confidentiality protocol. The results show a significant reduction in computation time and the number of states searched.