Formal Analysis of Time-Dependent Cryptographic Protocols in Real-Time Maude

This paper investigates the suitability of applying the general-purpose real-time Maude tool to the formal specification and model checking analysis of time-dependent cryptographic protocols. We restrict the intruders so that they become non-Zeno, and propose a complete analysis method for finding attacks that are reachable from the initial state. Our method has been used on the benchmark wide-mouthed frog (WMF) and Kerberos protocols, on which we can find all the well known flaws in short time. We use the WMF protocol to illustrate formal specification and the use of our method to analyze timed authentication properties.