Back to Search
Start Over
Modeling and Verifying Time Sensitive Security Protocols with Constraints.
- Source :
- ENTCS: Electronic Notes in Theoretical Computer Science; Apr2008, Vol. 212, p103-118, 16p
- Publication Year :
- 2008
-
Abstract
- Abstract: 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. [Copyright &y& Elsevier]
Details
- Language :
- English
- ISSN :
- 15710661
- Volume :
- 212
- Database :
- Supplemental Index
- Journal :
- ENTCS: Electronic Notes in Theoretical Computer Science
- Publication Type :
- Periodical
- Accession number :
- 32087827
- Full Text :
- https://doi.org/10.1016/j.entcs.2008.04.056