Title: Attack trace generation of cryptographic protocols based on coloured Petri nets model

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.

DOI: 10.1504/IJWMC.2013.053028

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: 11 Oct 2014 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article