Considering Time in Formal Analysis of Security Protocols Using Colored Petri Nets
Timed foctors 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.
Meng Xu Guiping Su Yanlan Ding
School of Information Science and Engineering,Graduate University of Chinese Academy of Sciences,Beijing
国际会议
成都
英文
63-68
2008-01-01（万方平台首次上网日期，不代表论文的发表时间）