On-the-fly Trace Generation Approach to the Security Analysis of Cryptographic Protocols: Coloured Petri Nets-based Method

Most Petri nets-based methods that have been developed to analyze cryptographic protocols provide the analysis of one attack trace only. Only a few of them offer the analysis of multiple attack traces, but they are rather inefficient. Analogously, the limitation of the analysis of one attack trace occurs in most model checking methods for cryptographic protocols. In this paper, we propose a very simple but practical Coloured Petri nets-based model checking method for the analysis of cryptographic protocols, which overcomes these limitations. Our method offers an efficient analysis of multiple attack traces. We apply our method to two case studies which are TMN authenticated key exchanged protocol and Micali's contract signing protocol. Surprisingly, our simple method is very efficient when the numbers of attack traces and states are large. Also, we find many new attacks in those protocols.