Developing Security Protocols by Refinement

Below are the links to our entries in the Archive of Formal Proofs (AFP) where you can find the Isabelle/HOL sources for our correct-by-construction security protocol development frameworks based on refinement.

The first AFP entry is described in our CCS 2010 and CSF 2012 conference papers, which are subsumed by our JCS 2018 journal paper. The second AFP entry accompanies our EuroS&P 2017 conference paper.

You can find links to these papers on our publications pages.