کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
423601 | 685262 | 2008 | 16 صفحه PDF | دانلود رایگان |

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.
Journal: Electronic Notes in Theoretical Computer Science - Volume 212, 30 April 2008, Pages 103-118