Open access
Date
2013Type
- Report
ETH Bibliography
yes
Altmetrics
Abstract
We propose a development method for security protocols based on stepwise refinement. Our refinement strategy transforms abstract security goals into protocols that are secure when operating over an insecure channel controlled by a Dolev-Yao-style intruder. As intermediate levels of abstraction, we employ message-less guard protocols and channel protocols communicating over channels with security properties. These abstractions provide insights on why the protocols are secure and foster the development of families of protocols sharing common structure and properties. We have implemented our method in Isabelle/HOL and used it to develop different entity authentication and key establishment protocols. These protocols include realistic features such as key confirmation, replay caches, and encrypted tickets. Our development highlights that guard protocols and channel protocols provide fundamental abstractions for bridging the gap between security properties and standard protocol descriptions based on cryptographic messages. It also shows that our refinement approach scales to protocols of nontrivial size and complexity. Show more
Permanent link
https://doi.org/10.3929/ethz-a-009900739Publication status
publishedJournal / series
Technical Report / ETH Zurich, Department of Computer ScienceVolume
Publisher
ETH, Department of Computer Science, Institute of Information SecuritySubject
DATA SECURITY + DATA PROTECTION (OPERATING SYSTEMS); NETWORK PROTOCOLS + COMMUNICATION PROTOCOLS (COMPUTER SYSTEMS); Entity authentication; NETZWERKPROTOKOLLE + KOMMUNIKATIONSPROTOKOLLE (COMPUTERSYSTEME); Security protocols; Key establishment; Correct-by-construction development; DATENSICHERHEIT + DATENSCHUTZ (BETRIEBSSYSTEME); Stepwise refinementOrganisational unit
02150 - Dep. Informatik / Dep. of Computer Science03634 - Basin, David / Basin, David
Notes
Technical Reports D-Infk. See also http://e-citations.ethbib.ethz.ch/view/pub:108010. See also http://e-citations.ethbib.ethz.ch/view/pub:113613.More
Show all metadata
ETH Bibliography
yes
Altmetrics