Timed and Parameterised Security Protocol Verification

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

  • L. Li, J. Sun, Y. Liu, M. Sun, and J. S. Dong. A Formal Specification and Verification Framework for Timed Security Protocols. Under submission.
    [PDF] [Bibtex] Tool and Models: Darwin-x86_64-v0.1.5.zip
    @inproceedings{Li-Sun-Liu-Sun-Dong16a,
    author = {Li Li and Jun Sun and Yang Liu and Meng Sun and Jin Song Dong},
    title = {A Formal Specification and Verification Framework for Timed Security Protocols},
    year = {2016},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/09/TSE-draft.pdf},
    note = {Under submission},
    }

  • L. Li, J. Sun, and J. S. Dong. Automated verification of timed security protocols with clock drift. In Proc. International Symposium on Formal Methods (FM 2016), LNCS-FM, Springer, 2016.
    [PDF] [Bibtex] Tool and Models: Darwin-x86_64-v0.1.4.zip
    @inproceedings{Li-Sun-Dong16a,
    author = {Li Li and Jun Sun and Jin Song Dong},
    title = {Automated Verification of Timed Security Protocols with Clock Drift},
    booktitle = {{Proc. International Symposium on Formal Methods (FM 2016)}},
    series = {LNCS-FM},
    publisher = {Springer},
    year = {2016},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/Li-Sun-Dong.FM_.2016.pdf},
    note = {To appear},
    }

  • L. Li, J. Sun, Y. Liu, and J. S. Dong. Verifying parameterized timed security protocols. In Proc. International Symposium on Formal Methods (FM 2015), volume 9109, LNCS, Springer, 2015, pp. 342-359.
    [PDF] [DOI] [Bibtex] Tool and Models: Darwin-x86_64-v0.0.9.zip
    @inproceedings{Li-Sun-Liu-Dong15a,
    author = {Li Li and
    Jun Sun and
    Yang Liu and
    Jin Song Dong},
    title = {Verifying Parameterized Timed Security Protocols},
    booktitle = {{Proc. International Symposium on Formal Methods (FM 2015)}},
    pages = {342--359},
    series = {LNCS},
    volume = {9109},
    publisher = {Springer},
    year = {2015},
    doi = {10.1007/978-3-319-19249-9_22},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/Li-Sun-Liu-Dong15a.pdf},
    }

  • L. Li, J. Sun, Y. Liu, and J. S. Dong. TAuth: verifying timed security protocols. In Proc. International Conference on Formal Engineering Methods (ICFEM 2014), volume 8829, LNCS, Springer, 2014, pp. 300-315.
    [PDF] [DOI] [Bibtex] Model / Experiments: model.zip; Tool Version: Darwin-x86_64-v0.0.7.zip
    @inproceedings{Li-Sun-Liu-Dong14a,
    author = {Li Li and
    Jun Sun and
    Yang Liu and
    Jin Song Dong},
    title = {{TAuth}: Verifying Timed Security Protocols},
    booktitle = {{Proc. International Conference on Formal Engineering Methods (ICFEM 2014)}},
    pages = {300--315},
    series = {LNCS},
    volume = {8829},
    publisher = {Springer},
    year = {2014},
    doi = {10.1007/978-3-319-11737-9_20},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/Li-Sun-Liu-Dong14a.pdf},
    }

Contacts

LI Li and SUN Jun.