Show simple item record

dc.contributor.author
Basin, David A.
dc.contributor.author
Sprenger, Christoph
dc.date.accessioned
2017-07-20T13:48:25Z
dc.date.available
2017-06-10T17:57:48Z
dc.date.available
2017-07-20T13:48:25Z
dc.date.issued
2013
dc.identifier.uri
http://hdl.handle.net/20.500.11850/67931
dc.identifier.doi
10.3929/ethz-a-009900739
dc.description.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.
en_US
dc.language.iso
en
en_US
dc.publisher
ETH, Department of Computer Science, Institute of Information Security
en_US
dc.rights.uri
http://rightsstatements.org/page/InC-NC/1.0/
dc.subject
DATA SECURITY + DATA PROTECTION (OPERATING SYSTEMS)
en_US
dc.subject
NETWORK PROTOCOLS + COMMUNICATION PROTOCOLS (COMPUTER SYSTEMS)
en_US
dc.subject
Entity authentication
en_US
dc.subject
NETZWERKPROTOKOLLE + KOMMUNIKATIONSPROTOKOLLE (COMPUTERSYSTEME)
en_US
dc.subject
Security protocols
en_US
dc.subject
Key establishment
en_US
dc.subject
Correct-by-construction development
en_US
dc.subject
DATENSICHERHEIT + DATENSCHUTZ (BETRIEBSSYSTEME)
en_US
dc.subject
Stepwise refinement
en_US
dc.title
Developing Security Protocols by Refinement
en_US
dc.type
Report
dc.rights.license
In Copyright - Non-Commercial Use Permitted
dc.date.published
2013
ethz.journal.title
Technical Report / ETH Zurich, Department of Computer Science
ethz.journal.volume
787
en_US
ethz.size
52 p.
en_US
ethz.code.ddc
0 - Computer science, information & general works::004 - Data processing, computer science
en_US
ethz.code.ddc
0 - Computer science, information & general works::004 - Data processing, computer science
en_US
ethz.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.
en_US
ethz.identifier.nebis
009900739
ethz.publication.place
Zürich
en_US
ethz.publication.status
published
en_US
ethz.leitzahl
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science
en_US
ethz.leitzahl
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science::02660 - Institut für Informationssicherheit::03634 - Basin, David / Basin, David
en_US
ethz.leitzahl.certified
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science::02660 - Institut für Informationssicherheit::03634 - Basin, David / Basin, David
ethz.date.deposited
2017-06-10T17:59:30Z
ethz.source
ECOL
ethz.source
ECIT
ethz.identifier.importid
imp59366b3fe828070735
ethz.identifier.importid
imp593650aec6b6583516
ethz.ecolpid
eth:7081
ethz.ecitpid
pub:108010
ethz.eth
yes
en_US
ethz.availability
Open access
en_US
ethz.rosetta.installDate
2017-07-13T07:32:15Z
ethz.rosetta.lastUpdated
2018-11-05T15:08:28Z
ethz.rosetta.exportRequired
true
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.atitle=Developing%20Security%20Protocols%20by%20Refinement&rft.jtitle=Technical%20Report%20/%20ETH%20Zurich,%20Department%20of%20Computer%20Science&rft.date=2013&rft.volume=787&rft.au=Basin,%20David%20A.&Sprenger,%20Christoph&rft.genre=report&
 Search via SFX

Files in this item

Thumbnail

Publication type

Show simple item record