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

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.