Abstract:


A monad-based modeling and verification toolbox 
with application to security protocols


Christoph Sprenger and David Basin



We 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.