Considering Time in Formal Analysis of Security Protocols Using Colored Petri Nets

Timed factors are usually simplified or even omitted in model checking of cryptographic protocols, but they do have effects on implementations of security protocols. In this paper, we concentrate on the suitability of applying CPN Tools to considering time in the formal analysis of two kinds of protocols, time-sensitive and non-time-sensitive cryptographic protocols. We also propose two kinds of time expression, non-global clocks as timestamps and a global built-in time notion in CPNs, which are respectively applied to the specification and verification of these two kinds of protocols, using wide-mouthed frog (WMF) protocol and a simplified version of NS protocol as examples. Finally, we establish and discuss retransmission mechanisms for WMF based on several simulations.