Re: [isabelle] Advertise your work on the mailing list

Hi all,

Now it's your turn!

here is another one:

Developing Security Protocols by Refinement
Christoph Sprenger and David Basin

Proceedings of the 17th ACM Conference on Computer and Communications Security (CCS)
Chicago, IL, USA, October 4-8, 2010, pp. 361--374

Abstract--- We propose a development method for security protocols based on stepwise refinement. Our refinement strategy 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 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 different entity authentication and key transport protocols.

Best wishes,

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.