Verifying parameterized timed security protocols
Quantitative timing is often explicitly used in systems for better security, e.g., the credentials for automatic website logon often has limited lifetime. Verifying timing relevant security protocols in these systems is very challenging as timing adds another dimension of complexity compared with th...
Saved in:
Main Authors: | , , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2015
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/4949 https://ink.library.smu.edu.sg/context/sis_research/article/5952/viewcontent/LNCS_9109___FM_2015__Formal_Methods.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-5952 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-59522020-02-27T03:20:20Z Verifying parameterized timed security protocols LI, Li SUN, Jun LIU, Yang DONG, Jin Song Quantitative timing is often explicitly used in systems for better security, e.g., the credentials for automatic website logon often has limited lifetime. Verifying timing relevant security protocols in these systems is very challenging as timing adds another dimension of complexity compared with the untimed protocol verification. In our previous work, we proposed an approach to check the correctness of the timed authentication in security protocols with fixed timing constraints. However, a more difficult question persists, i.e., given a particular protocol design, whether the protocol has security flaws in its design or it can be configured secure with proper parameter values? In this work, we answer this question by proposing a parameterized verification framework, where the quantitative parameters in the protocols can be intuitively specified as well as automatically analyzed. Given a security protocol, our verification algorithm either produces the secure constraints of the parameters, or constructs an attack that works for any parameter values. The correctness of our algorithm is formally proved. We implement our method into a tool called PTAuth and evaluate it with several security protocols. Using PTAuth, we have successfully found a timing attack in Kerberos V which is unreported before. 2015-06-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4949 info:doi/10.1007/978-3-319-19249-9_22 https://ink.library.smu.edu.sg/context/sis_research/article/5952/viewcontent/LNCS_9109___FM_2015__Formal_Methods.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 Security Protocol Guard Condition Protocol Session Secrecy Query Service Ticket Programming Languages and Compilers Software Engineering |
institution |
Singapore Management University |
building |
SMU Libraries |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
SMU Libraries |
collection |
InK@SMU |
language |
English |
topic |
Security Protocol Guard Condition Protocol Session Secrecy Query Service Ticket Programming Languages and Compilers Software Engineering |
spellingShingle |
Security Protocol Guard Condition Protocol Session Secrecy Query Service Ticket Programming Languages and Compilers Software Engineering LI, Li SUN, Jun LIU, Yang DONG, Jin Song Verifying parameterized timed security protocols |
description |
Quantitative timing is often explicitly used in systems for better security, e.g., the credentials for automatic website logon often has limited lifetime. Verifying timing relevant security protocols in these systems is very challenging as timing adds another dimension of complexity compared with the untimed protocol verification. In our previous work, we proposed an approach to check the correctness of the timed authentication in security protocols with fixed timing constraints. However, a more difficult question persists, i.e., given a particular protocol design, whether the protocol has security flaws in its design or it can be configured secure with proper parameter values? In this work, we answer this question by proposing a parameterized verification framework, where the quantitative parameters in the protocols can be intuitively specified as well as automatically analyzed. Given a security protocol, our verification algorithm either produces the secure constraints of the parameters, or constructs an attack that works for any parameter values. The correctness of our algorithm is formally proved. We implement our method into a tool called PTAuth and evaluate it with several security protocols. Using PTAuth, we have successfully found a timing attack in Kerberos V which is unreported before. |
format |
text |
author |
LI, Li SUN, Jun LIU, Yang DONG, Jin Song |
author_facet |
LI, Li SUN, Jun LIU, Yang DONG, Jin Song |
author_sort |
LI, Li |
title |
Verifying parameterized timed security protocols |
title_short |
Verifying parameterized timed security protocols |
title_full |
Verifying parameterized timed security protocols |
title_fullStr |
Verifying parameterized timed security protocols |
title_full_unstemmed |
Verifying parameterized timed security protocols |
title_sort |
verifying parameterized timed security protocols |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2015 |
url |
https://ink.library.smu.edu.sg/sis_research/4949 https://ink.library.smu.edu.sg/context/sis_research/article/5952/viewcontent/LNCS_9109___FM_2015__Formal_Methods.pdf |
_version_ |
1770575155898089472 |