[Club2] Christoph Sprenger: A Monad-based Modeling and Verification Toolbox with Application to, Security Protocols

[Florian Haftmann]

Do 16. Aug 2007, 10:00, Konrad Zuse (01.11.018):

Christoph Sprenger, Information Security group, ETH Zurich:

A Monad-based Modeling and Verification Toolbox with Application to
Security Protocols

In this talk, I will present an advanced modeling and verification
toolbox for functional programs with state and exceptions. The toolbox
integrates an extensible, monad-based, component model, a monad-based
Hoare logic and weakest pre-condition calculus, and proof systems for
temporal logic and bisimilarity. It is implemented in Isabelle/HOL using
shallow embeddings and incorporates as much modeling and reasoning power
as possible from Isabelle/HOL. We have validated the toolbox's
usefulness in a substantial security protocol verification project,
which will serve as a running example to illustrate the various concepts.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: florian.haftmann.vcf
Type: text/x-vcard
Size: 654 bytes
Desc: not available
Url : https://mailmanbroy.informatik.tu-muenchen.de/mailman/private/club2/attachments/20070809/eb9d1665/attachment.vcf 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 185 bytes
Desc: OpenPGP digital signature
Url : https://mailmanbroy.informatik.tu-muenchen.de/mailman/private/club2/attachments/20070809/eb9d1665/attachment.pgp