Verifying Timed Security Protocols
Nowadays, protocols often use time to provide better security. For instance, lifetime of critical credentials and latency of physical networks are often introduced as safety thresholds in system designs. However, using time correctly in protocol design is challenging, due to a lack of time related formal specification and verification techniques. Thus, we propose a comprehensive analysis framework to formally specify as well as automatically verify timed security protocols.
A parameterized method is introduced in our framework to handle flexible timing constants whose values cannot be decided in the protocol design stage. In this work, we first propose timed applied π-calculus as a formal specification language for timed protocols. It can express computation of continuous time as well as application of cryptographic functions. Then, we define its formal semantics based on timed logic rules, which facilitates efficient verification against various authentication and secrecy properties. Given a parameterized security protocol, the verification result either produces secure configuration methods of its parameters, or reports an attack that works for any parameter values.
The correctness of our verification algorithm has been formally proved. We evaluate our framework with multiple timed and untimed security protocols and successfully find a previously unknown timing attack in Kerberos V.
Papers and Supplementary Material
A Formal Specification and Verification Framework for Timed Security Protocols.
IEEE Trans. Software Eng. 44(8).
Tool and Models: Darwin-x86_64-v0.1.5.zip
Automated Verification of Timed Security Protocols with Clock Drift.
FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings.
Tool and Models: Darwin-x86_64-v0.1.4.zip
Verifying Parameterized Timed Security Protocols.
FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings.
Tool and Models: Darwin-x86_64-v0.0.9.zip
TAuth: Verifying Timed Security Protocols.
Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings.
Tool and Models: model.zip; Darwin-x86_64-v0.0.7.zip
People
