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
Topics
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