Formalizing and Proving a Typing Result for Security Protocols in Isabelle/HOL

This is subsumed by our work Andreas V. Hess, Sebastian A. Mödersheim and Achim D. Brucker: Stateful Protocol Composition., ESORICS 2018, Extended version available and Isabelle Formalization available.


Old version:

Andreas Viktor Hess and Sebastian Mödersheim
CSF 2017 Paper (pre-print)

Isabelle Source Codes:

These theories depend on the IsaFoR library v2.27. (Please download into the directory IsaFoR and move it to your Isabelle installation or change the path in the imports.)

We give the sources ordered by dependency with the correspondence of the sections of the paper and the names of the lemmas and theorems:
  1. Messages.thy (Section 2.1)
  2. Unification2.thy (Section 2.2-2.3)
    • Lemma 1: wf_subst_compose
  3. IntruderDeduction.thy (Section 3)
  4. StrandsAndConstraints.thy (Section 4.1-4.3)
  5. InfiniteChains.thy (Needed in the completeness proof for the lazy intruder.)
  6. LazyIntruder.thy (Section 4.4-4.5)
    • Lemma 2: LI_preserves_wellformedness
    • Theorem 1: LI_soundness
    • Lemma 3: LI_no_inifite_chain
    • Lemma 5: LI_completeness_single
    • Theorem 2: LI_completeness
  7. TypedModel.thy (Section 5)
    • Lemma 6: LI_preserves_welltypedness, LI_preserves_tfr
    • Lemma 7: wt_sat_if_simple
    • Theorem 3: wt_attack_if_tfr_attack
  8. TLSExample.thy (Section 5.2)
  9. ProtocolTransitionSystem.thy (Section 6)
    • Lemma 8: pts_symbolic_to_pts_symbolic_c_from_initial
    • Lemma 9: pts_symbolic_c_to_pts_symbolic_from_initial
    • Theorem 4: wt_attack_if_tfr_attack_pts
(Note: Lemma 4 is no longer part of the formalization since it is not needed for the typing result.)

All files as a zip archive.