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

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 prcondition calculus, and proof systems for temporal logic and bisimilarity. It is im-plemented 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