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

Additional URL

https://doi.org/10.1007/978-3-319-11737-9_20

Share

COinS