Modeling and Verifying Time Sensitive Security Protocols with Constraints

This paper researches the characteristic of time sensitive protocols and presents a method with simple operations to verify protocols with time stamps and avoid false attacks. Firstly, an extension of π calculus is given to model a time sensitive security protocol. And then, by appending linear arithmetic constraints to the Horn logic model, the extended Horn logic model of security protocols and the modified-version verification method with time constraints are represented. All operations and the strategy of verification are defined for our constraints system. Thirdly, a method is given to determine whether the constraints has a solution or not. Finally, as a result of an experiment, Denning-Sacco protocol with time stamps is verified. The experiment shows that our approach is an innovative and effective method on verifying time sensitive security protocols.