Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

6-2015

Abstract

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.

Keywords

Security Protocol, Guard Condition, Protocol Session, Secrecy Query, Service Ticket

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 20th International Symposium on Formal Methods, FM 2015, Oslo, Norway, June 24-26

Volume

9109

First Page

342

Last Page

358

ISBN

9783319192499

Identifier

10.1007/978-3-319-19249-9_22

City or Country

Oslo, Norway

Additional URL

https://doi.org/10.1007/978-3-319-19249-9_22

Download

Share

COinS