Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

11-2016

Abstract

Time is frequently used in security protocols to provide better security. For instance, critical credentials often have limited lifetime which improves the security against brute-force attacks. However, it is challenging to correctly use time in protocol design, due to the existence of clock drift in practice. In this work, we develop a systematic method to formally specify as well as automatically verify timed security protocols with clock drift. We first extend the previously proposed timed applied ππ -calculus as a formal specification language for timed protocols with clock drift. Then, we define its formal semantics based on timed logic rules, which facilitates efficient verification against various security properties. Clock drift is encoded as parameters in the rules. The verification result shows the constraints associated with clock drift that are required for the security of the protocol, e.g., the maximum drift should be less than some constant. We evaluate our method with multiple timed security protocols. We find a time-related security threat in the TESLA protocol, a complex time-related broadcast protocol for lossy channels, when the clocks used by different protocol participants do not share the same clock rate.

Keywords

Security Protocol, Clock Rate, Local Clock, Global Clock, Clock Drift

Discipline

Information Security | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 21st International Symposium Limassol, Cyprus, 2016 November 9–11

Volume

9995

First Page

513

Last Page

530

ISBN

9783319489889

Identifier

10.1007/978-3-319-48989-6_31

Publisher

Springer Link

City or Country

Limassol, Cyprus

Additional URL

https://doi.org/10.1007/978-3-319-48989-6_31

Download

Share

COinS