Paper 2010/645

A Timed Logic for Modeling and Reasoning about Security Protocols

Xinfeng Lei, Rui Xue, and Ting Yu

Abstract

Many logical methods are usually considered suitable to express the static properties of security protocols while unsuitable to model dynamic processes or properties. However, a security protocol itself is in fact a dynamic process over time, and sometimes it is important to be able to express time-dependent security properties of protocols. In this paper, we present a new timed logic based on predicate modal logic, in which time is explicitly expressed in parameters of predicates or modal operators. This makes it possible to model an agent's actions, knowledge and beliefs at different and exact time points, which enables us to model both protocols and their properties, especially time-dependent properties. We formalize semantics of the presented logic, and prove its soundness. We also present a modeling scheme for formalizing protocols and security properties of authentication and secrecy under the logic. The scheme provides a flexible and succinct framework to reason about security protocols, and essentially enhances the power of logical methods for protocol analysis. As a case study, we then analyze a timed-release protocol using this framework, and discover a new vulnerability that did not appear previously in the literature. We provide a further example to show additional advantages of the modeling scheme in the new logic.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published elsewhere. Unknown where it was published
Keywords
timed logicsecurity protocolsformal method
Contact author(s)
leixinfeng @ is iscas ac cn
History
2010-12-22: last of 2 revisions
2010-12-21: received
See all versions
Short URL
https://ia.cr/2010/645
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2010/645,
      author = {Xinfeng Lei and Rui Xue and Ting Yu},
      title = {A Timed Logic for Modeling and Reasoning about Security Protocols},
      howpublished = {Cryptology ePrint Archive, Paper 2010/645},
      year = {2010},
      note = {\url{https://eprint.iacr.org/2010/645}},
      url = {https://eprint.iacr.org/2010/645}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.