Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
5-2014
Abstract
Quantitative timing is often relevant to the security of systems, like web applications, cyber-physical systems, etc. Verifying timed security protocols is however challenging as both arbitrary attacking behaviors and quantitative timing may lead to undecidability. In this work, we develop a service framework to support intuitive modeling of the timed protocol, as well as automatic verification with an unbounded number of sessions. The partial soundness and completeness of our verification algorithms are formally defined and proved. We implement our method into a tool called TAuth and the experiment results show that our approach is efficient and effective in both finding security flaws and giving proofs.
Keywords
False Alarm, Timing Constraint, Service Composition, Service Basis, Authentication Protocol
Discipline
Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
Proceedings of the 16th International Conference on Formal Engineering Methods, ICFEM 2014, Luxembourg, November 3–5
First Page
300
Last Page
315
ISBN
9783319117362
Identifier
10.1007/978-3-319-11737-9_20
Publisher
Springer Link
City or Country
Luxembourg
Citation
LI, Li; SUN, Jun; LIU, Yang; and DONG, Jin Song.
TAuth: Verifying timed security protocols. (2014). Proceedings of the 16th International Conference on Formal Engineering Methods, ICFEM 2014, Luxembourg, November 3–5. 300-315.
Available at: https://ink.library.smu.edu.sg/sis_research/4987
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1007/978-3-319-11737-9_20