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:
- Messages.thy (Section 2.1)
- Unification2.thy (Section
2.2-2.3)
- Lemma 1: wf_subst_compose
- IntruderDeduction.thy
(Section 3)
- StrandsAndConstraints.thy
(Section 4.1-4.3)
- InfiniteChains.thy (Needed in
the completeness proof for the lazy intruder.)
- 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
- 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
- TLSExample.thy (Section 5.2)
- 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.