### 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 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.

### License

GNU Lesser General Public License (LGPL)

### Topics

- Computer science/Security

### Session Security_Protocol_Refinement

- Infra
- Refinement
- Agents
- Keys
- Atoms
- Runs
- Channels
- Message
- s0g_secrecy
- a0n_agree
- a0i_agree
- m1_auth
- m2_auth_chan
- m2_confid_chan
- m3_sig
- m3_enc
- m1_keydist
- m1_keydist_iirn
- m1_keydist_inrn
- m1_kerberos
- m2_kerberos
- m3_kerberos_par
- m3_kerberos5
- m3_kerberos4
- m1_nssk
- m2_nssk
- m3_nssk_par
- m3_nssk
- m1_ds
- m2_ds
- m3_ds_par
- m3_ds

## Cite

×

Security_Protocol_Refinement-AFP

    @article{Security_Protocol_Refinement-AFP,
      author  = {Christoph Sprenger and Ivano Somaini},
      title   = {Developing Security Protocols by Refinement},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Security_Protocol_Refinement.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- May 25, 2017 : Isabelle2016-1