A Logic to Model Time in Cryptographic Protocols

A number of logics have been proposed to analyze the cryptographic protocols, but most of them cannot explicitly express time factor which plays an important role in protocols. In this paper, we present a logic to model the time in cryptographic protocols. Our logic is based on the predicate modal logic, so, the time factor can be expressed by invoking a time variable as a parameter of predicate and modal operators. Then, by associating specific time points to each protocol statement, time is considered in analyzing protocols. This makes it possible to model each agent¿s actions, knowledge and belief at different time. Our logic provides a facilitate method for analyzing the cryptographic protocols, especially the time-dependent cryptographic protocols.