Affiliations: Logic and Security Laboratory, Department of Computer Engineering, Faculty of Engineering, King Mongkut's University of Technology Thonburi, Bangkok, Thailand. [email protected]
Note: [] We would like to thank anonymous reviewers for their helpful and constructive comments which lead to an improved version of the paper. The first author would like to thank Kurt Jensen and his group for the suggestion about the names of the on-the-fly trace generation and the textual trace analysis after his presentation at CPN'09 workshop. Also, the first author would like to thank Somsak Vanit-Anunchai for motivating discussion. Finally, the first author would like to acknowledge financial support from the Thailand Research Fund and the National Research Council of Thailand Address for correspondence: Department of Computer Engineering, Faculty of Engineering, King Mongkut's University of Technology Thonburi, 126 Pracha-Uthit Road, BangMod, ThungKhru, Bangkok 10140, Thailand
Note: [] We would like to thank anonymous reviewers for their helpful and constructive comments which lead to an improved version of the paper. The first author would like to thank Kurt Jensen and his group for the suggestion about the names of the on-the-fly trace generation and the textual trace analysis after his presentation at CPN'09 workshop. Also, the first author would like to thank Somsak Vanit-Anunchai for motivating discussion. Finally, the first author would like to acknowledge financial support from the Thailand Research Fund and the National Research Council of Thailand
Abstract: 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.
Keywords: Formal methods for cryptographic protocols, Model checking, Coloured Petri Nets, Petri Nets
