Email Gateway (Aug 22 2022 at 15:31): Email Gateway (Aug 22 2022 at 15:31):From: Tobias Nipkow <nipkow@in.tum.de>
Developing Security Protocols by Refinement
Christoph Sprenger and Ivano Somaini
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
messageless guard protocols and channel protocols communicating over channels
with security properties. These abstractions provide insights on why 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, including 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.
https://www.isa-afp.org/entries/Security_Protocol_Refinement.shtml
Enjoy!
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC