
Open access
Date
2015Type
- Report
ETH Bibliography
yes
Altmetrics
Abstract
We present a large class of security protocol abstractions with the aim of improving the scope and efficiency of verification tools. We propose typed abstractions, which transform a term's structure based on its type, and untyped abstractions, which remove atomic messages, variables, and redundant terms. Our theory improves on previous work by supporting a useful subclass of shallow subterm-convergent rewrite theories, 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. Show more
Permanent link
https://doi.org/10.3929/ethz-a-010347780Publication status
publishedExternal links
Search via swisscovery
Publisher
ETH-ZürichSubject
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
02660 - Institut für Informationssicherheit02150 - Dep. Informatik / Dep. of Computer Science
03634 - Basin, David / Basin, David
Funding
256980 - Network of Excellence on Engineering Secure Future Internet Software Services and Systems (EC)
More
Show all metadata
ETH Bibliography
yes
Altmetrics