Please use this identifier to cite or link to this item: https://hdl.handle.net/10356/141485
Title: A formal specification and verification framework for timed security protocols
Authors: Li, Li
Sun, Jun
Liu, Yang
Sun, Meng
Dong, Jin-Song
Keywords: Engineering::Computer science and engineering
Issue Date: 2018
Source: Li, L., Sun, J., Liu, Y., Sun, M., & Dong, J.-S. (2018). A formal specification and verification framework for timed security protocols. IEEE Transactions on Software Engineering, 44(8), 725 - 746. doi:10.1109/TSE.2017.2712621
Journal: IEEE Transactions on Software Engineering
Abstract: Nowadays, protocols often use time to provide better security. For instance, critical credentials are often associated with expiry dates in system designs. However, using time correctly in protocol design is challenging, due to the 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 timing parameters whose values cannot be decided in the protocol design stage. In this work, we first propose timed applied π-calculus as a formal language for specifying timed security protocols. It supports modeling 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, our method either produces a constraint on the timing parameters which guarantees the security property satisfied by the protocol, or reports an attack that works for any parameter value. 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.
URI: https://hdl.handle.net/10356/141485
ISSN: 0098-5589
DOI: 10.1109/TSE.2017.2712621
Rights: © 2018 IEEE. All rights reserved.
Fulltext Permission: none
Fulltext Availability: No Fulltext
Appears in Collections:SCSE Journal Articles

SCOPUSTM   
Citations 20

3
Updated on Mar 2, 2021

PublonsTM
Citations 20

3
Updated on Mar 7, 2021

Page view(s)

125
Updated on May 18, 2022

Google ScholarTM

Check

Altmetric


Plumx

Items in DR-NTU are protected by copyright, with all rights reserved, unless otherwise indicated.