(2018) Abstractions for security protocol verification.
Journal of Computer Security.
(In Press)
Full text not available from this repository.
Abstract
We present a large class of security protocol abstractions with the aim of improving the scope and efficiency of verification tools. We propose abstractions that transform a term’s structure based on its type as well as abstractions that remove atomic messages, variables, and redundant terms. Our theory improves on previous work by supporting rewrite theories with the finite-variant property, user-defined types, and untyped variables to cover type flaw attacks. We prove soundness results for an expressive property language that includes secrecy and authentication. Applying our abstractions to realistic IETF protocol models, we achieve dramatic speedups and extend the scope of several modern security protocol analyzers.
| Item Type: | Article |
|---|---|
| Depositing User: | Cas Cremers |
| Date Deposited: | 25 Sep 2018 13:26 |
| Last Modified: | 18 Jul 2019 12:09 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/2652 |
Actions
Actions (login required)
 |
View Item |