Developing Security Protocols by Refinement
Event details
| Date | 17.06.2013 |
| Hour | 14:00 › 15:00 |
| Speaker | Prof. David Basin, ETH Zurich |
| Location | |
| Category | Conferences - Seminars |
We survey recent work of ours on developing security protocols by step-wise refinement. We present a refinement strategy that guides the transformation of abstract security goals into protocols that are secure when operating over an insecure channel controlled by a Dolev-Yao-style intruder. The refinement steps used successively introduce local states, an intruder, communication channels with security properties, and cryptographic operations realizing these channels. The abstractions used provide insights on how the protocols work and foster the development of families of protocols sharing a common structure and properties. In contrast to post-hoc verification methods, protocols are developed together with their correctness proofs. We have implemented our method in Isabelle/HOL and used it to develop a number of entity authentication and key transport protocols.
(Joint work with Christoph Sprenger, ETH Zurich)
(Joint work with Christoph Sprenger, ETH Zurich)
Links
Practical information
- General public
- Free
Organizer
- SuRI 2013
Contact
- Simone Muller