BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Developing Security Protocols by Refinement
DTSTART:20130617T140000
DTEND:20130617T150000
DTSTAMP:20260407T163400Z
UID:af380994ccb2ac5ce66b41bd773e132b44e2af13951d4e1d7c711bb7
CATEGORIES:Conferences - Seminars
DESCRIPTION:Prof. David Basin\, ETH Zurich\nWe survey recent work of ours 
 on developing security protocols by step-wise refinement.  We present a r
 efinement strategy that guides the transformation of abstract security goa
 ls into protocols that are secure when operating over an insecure channel 
 controlled by a Dolev-Yao-style intruder.  The refinement steps used succ
 essively introduce local states\, an intruder\, communication channels wit
 h security properties\, and cryptographic operations realizing these chann
 els.  The abstractions used provide insights on how the protocols work an
 d foster the development of families of protocols sharing a common structu
 re and properties.  In contrast to post-hoc verification methods\, protoc
 ols are developed together with their correctness proofs.  We have implem
 ented our method in Isabelle/HOL and used it to develop a number of entity
  authentication and key transport protocols.\n(Joint work with Christoph S
 prenger\, ETH Zurich)
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR