Abstractions for security protocol verification
OPEN ACCESS
Author / Producer
Date
2014
Publication Type
Report
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
We present a large class of security protocol abstractions with the aim of improving the scope and efficiency of verification tools. We present type-based abstractions, which use a term’s type to uniformly select the kind of abstraction applied, as well as untyped abstractions, which enable the removal of atomic messages, variables, and redundant terms. We extend existing work in the area by supporting additional abstractions, 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 a set of realistic IETF protocol models, we achieve dramatic speedups and extend the scope of several modern security protocol analyzers.
Permanent link
Publication status
published
External links
Editor
Book title
Journal / series
Volume
Pages / Article No.
Publisher
ETH-Zürich
Event
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
VERIFICATION (SOFTWARE ENGINEERING); DATA SECURITY + DATA PROTECTION (OPERATING SYSTEMS); NETWORK PROTOCOLS + COMMUNICATION PROTOCOLS (COMPUTER SYSTEMS); NETZWERKPROTOKOLLE + KOMMUNIKATIONSPROTOKOLLE (COMPUTERSYSTEME); VERIFIKATION (SOFTWARE ENGINEERING); DATENSICHERHEIT + DATENSCHUTZ (BETRIEBSSYSTEME)
Organisational unit
03634 - Basin, David / Basin, David
02660 - Institut für Informationssicherheit / Institute of Information Security
02150 - Dep. Informatik / Dep. of Computer Science