Authors: Yunli Bai; Xinming Ye
Addresses: College of Computer Science, Inner Mongolia University, Hohhot, China; College of Computer and Information Engineering, Inner Mongolia Agricultural University, Hohhot, China ' College of Computer Science, Inner Mongolia University, Hohhot, China
Abstract: In this paper, we propose a practical model checking methodology for the analysis of key exchange confidentiality property and authentication property of cryptographic protocols modelled by Coloured Petri Net (CPN); and propose a new attack trace generation algorithm based on the Observed Coloured Petri Net (OCPN), which is equipped with indicators that allow observation of the tokens in some of the places and/or observation of the firing of some of the transitions. Our methodology offers an efficient analysis of all attack traces for each found attack. In addition, we apply our method to TMN authenticated key exchanged protocol of mobile communication systems, and verified the effectiveness of our methodology.
Keywords: cryptographic protocols; TMN; CPN; observable; attack trace generation; coloured Petri nets; modelling; model checking; cryptography; key exchange confidentiality; authentication; security; attack traces; mobile communications.
International Journal of Wireless and Mobile Computing, 2013 Vol.6 No.1, pp.91 - 97
Received: 19 Dec 2011
Accepted: 05 Jan 2012
Published online: 03 Apr 2013 *