A formal specification and verification framework for timed security protocols
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 technique...
Saved in:
Main Authors: | , , , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2018
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/4850 https://ink.library.smu.edu.sg/context/sis_research/article/5853/viewcontent/a_formal__PV.pdf |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Singapore Management University |
Language: | English |
id |
sg-smu-ink.sis_research-5853 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-58532020-01-23T07:12:58Z A formal specification and verification framework for timed security protocols LI, Li SUN, Jun LIU, Yang SUN, Meng DONG, Jin Song 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 p-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. 2018-08-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4850 info:doi/10.1109/TSE.2017.2712621 https://ink.library.smu.edu.sg/context/sis_research/article/5853/viewcontent/a_formal__PV.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Software Engineering |
institution |
Singapore Management University |
building |
SMU Libraries |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
SMU Libraries |
collection |
InK@SMU |
language |
English |
topic |
Software Engineering |
spellingShingle |
Software Engineering LI, Li SUN, Jun LIU, Yang SUN, Meng DONG, Jin Song A formal specification and verification framework for timed security protocols |
description |
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 p-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. |
format |
text |
author |
LI, Li SUN, Jun LIU, Yang SUN, Meng DONG, Jin Song |
author_facet |
LI, Li SUN, Jun LIU, Yang SUN, Meng DONG, Jin Song |
author_sort |
LI, Li |
title |
A formal specification and verification framework for timed security protocols |
title_short |
A formal specification and verification framework for timed security protocols |
title_full |
A formal specification and verification framework for timed security protocols |
title_fullStr |
A formal specification and verification framework for timed security protocols |
title_full_unstemmed |
A formal specification and verification framework for timed security protocols |
title_sort |
formal specification and verification framework for timed security protocols |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2018 |
url |
https://ink.library.smu.edu.sg/sis_research/4850 https://ink.library.smu.edu.sg/context/sis_research/article/5853/viewcontent/a_formal__PV.pdf |
_version_ |
1770575062987964416 |