scyther-proof 0.6.0.0 → 0.8.0.0
raw patch · 16 files changed
+2394/−387 lines, 16 filesdep ~cmdargsdep ~mtlnew-uploader
Dependency ranges changed: cmdargs, mtl
Files
- CHANGES +3/−0
- README.md +5/−5
- data/examples/Makefile +11/−8
- data/examples/iso9798/isabelle-proofs/isoiec-9798_cert_auto.thy +675/−0
- data/examples/iso9798/isoiec-9798.spthy +1619/−0
- data/isabelle/README +5/−5
- data/isabelle/src/ESPLogic/Hints.thy +6/−9
- data/isabelle/src/ESPLogic/Unify.thy +3/−3
- data/isabelle/src/ESPLogic/WeakTyping.thy +12/−0
- data/isabelle/src/ESPLogic/espl_definitions.ML +21/−25
- data/isabelle/src/ESPLogic/espl_methods.ML +5/−8
- data/isabelle/src/ESPLogic/espl_utils.ML +10/−11
- data/isabelle/src/Tutorial.thy +0/−295
- scyther-proof.cabal +3/−3
- src/Main.hs +15/−14
- src/System/Isabelle.hs +1/−1
CHANGES view
@@ -1,3 +1,6 @@+* 0.8.0.0+ - upgraded dependency on Isabelle to Isabelle-2013-2+ * 0.6.0.0 - ported to Isabelle-2013 by Andreas Lochbihler - removed buggy isabelle timout support
README.md view
@@ -3,7 +3,7 @@ Authors: Simon Meier <iridcode@gmail.com> Creation Date: 2011-05-13-Last Updated: 2013-02-27 by Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>+Last Updated: 2014-01-31 by Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch> 1. Introduction ===============@@ -55,10 +55,10 @@ 2.2 Installing the Isabelle/HOL theories ---------------------------------------- -Download and install full Isabelle2013 according to the installation+Download and install full Isabelle2013-2 according to the installation instructions at - http://isabelle.in.tum.de/website-Isabelle2013/download_x86-linux.html+ http://isabelle.in.tum.de/website-Isabelle2013-2/ The first time you call `scyther-proof` with the `--isabelle` flag it will build the logic image of the Isabelle/HOL theories formalizing the security@@ -178,6 +178,6 @@ `Happy Proving :)` -In case of questions do not hesistate to contact Simon Meier at-iridcode@gmail.com.+In case of questions do not hesistate to contact Andreas Lochbihler+(andreas.lochbihler@inf.ethz.ch) or Simon Meier (iridcode@gmail.com).
data/examples/Makefile view
@@ -32,27 +32,30 @@ # - newest scyther-proof with Isabelle support # (build according to: https://svn.inf.ethz.ch/svn/basin/infsec/trunk/projects/FOSSP/espl/README) +ISO_SAME_KEY = iso9798/isoiec-9798-2-bdkey.spthy iso9798/isoiec-9798-2-udkey.spthy iso9798/isoiec-9798-3.spthy iso9798/isoiec-9798-4-bdkey.spthy iso9798/isoiec-9798-4-udkey.spthy+ISO_ALL = iso9798/isoiec-9798.spthy $(ISO_SAME_KEY)+ iso9798-generate-proofs:- scyther-proof iso9798/*.spthy --shortest -Oiso9798/isabelle-proofs --ASCII+ scyther-proof $(ISO_ALL) --shortest -Oiso9798/isabelle-proofs --ASCII iso9798-generate-and-check-proofs:- scyther-proof iso9798/*.spthy --shortest -Oiso9798/isabelle-proofs --isabelle+ scyther-proof $(ISO_ALL) --shortest -Oiso9798/isabelle-proofs --isabelle iso9798-generate-check-and-visualize-proofs:- scyther-proof iso9798/*.spthy --shortest -Oiso9798/proofs-visualized --isabelle --html+ scyther-proof $(ISO_ALL) --shortest -Oiso9798/proofs-visualized --isabelle --html iso9798-visualize-proofs:- scyther-proof iso9798/*.spthy --shortest -Oiso9798/proofs-visualized --html+ scyther-proof $(ISO_ALL) --shortest -Oiso9798/proofs-visualized --html iso9798-generate-parallel-proofs:- scyther-proof iso9798/*.spthy --compose-parallel --shortest -Oiso9798/isabelle-parallel-proofs --ASCII+ scyther-proof $(ISO_ALL) --compose-parallel --shortest -Oiso9798/isabelle-parallel-proofs --ASCII iso9798-generate-and-check-parallel-proofs:- scyther-proof iso9798/*.spthy --compose-parallel --shortest -Oiso9798/isabelle-parallel-proofs --isabelle+ scyther-proof $(ISO_SAME_KEY) --compose-parallel --shortest -Oiso9798/isabelle-parallel-proofs --isabelle iso9798-generate-check-and-visualize-parallel-proofs:- scyther-proof iso9798/*.spthy --compose-parallel --shortest -Oiso9798/parallel-proofs-visualized --isabelle --html+ scyther-proof $(ISO_SAME_KEY) --compose-parallel --shortest -Oiso9798/parallel-proofs-visualized --isabelle --html iso9798-visualize-parallel-proofs:- scyther-proof iso9798/*.spthy --compose-parallel --shortest -Oiso9798/parallel-proofs-visualized --html+ scyther-proof $(ISO_ALL) --compose-parallel --shortest -Oiso9798/parallel-proofs-visualized --html
+ data/examples/iso9798/isabelle-proofs/isoiec-9798_cert_auto.thy view
@@ -0,0 +1,675 @@+theory "isoiec-9798_cert_auto"+imports+ "ESPLogic"+begin++role A+where "A =+ [ Recv ''1'' <| sMV ''B'', sAV ''A'', sMV ''Rb'', sMV ''Text1'' |>+ , Recv ''text2'' ( sMV ''Text2'' )+ , Send ''2'' <| sAV ''A'', sAV ''P'', sN ''Ra'', sMV ''Rb'', sMV ''B'',+ sMV ''Text2''+ |>+ , Recv ''3'' <| sAV ''P'', sAV ''A'', sMV ''Text5'',+ PEnc <| sC ''isoiec_9798_2_6_enc_3_1'', sN ''Ra'', sMV ''Kab'',+ sMV ''B'', sMV ''Text4''+ |>+ ( sK ''A'' ''P'' ),+ sMV ''TokenPA_for_B''+ |>+ , Recv ''text4'' <| sMV ''Text6'', sMV ''Text7'' |>+ , Send ''4'' <| sAV ''A'', sMV ''B'', sMV ''Text7'', sAV ''P'',+ sMV ''TokenPA_for_B'',+ PEnc <| sC ''isoiec_9798_2_6_enc_4'', sN ''Rpa'', sMV ''Rb'',+ sMV ''Text6''+ |>+ ( sMV ''Kab'' )+ |>+ , Recv ''5'' <| sMV ''B'', sAV ''A'', sMV ''Text9'',+ PEnc <| sC ''isoiec_9798_2_6_enc_5'', sMV ''Rb'', sN ''Rpa'',+ sMV ''Text8''+ |>+ ( sMV ''Kab'' )+ |>+ ]"++role Abd+where "Abd =+ [ Recv ''1'' <| sMV ''Bbd'', sAV ''Abd'', sMV ''Rb'', sMV ''Text1'' |>+ , Recv ''text2'' ( sMV ''Text2'' )+ , Send ''2'' <| sAV ''Abd'', sAV ''Pbd'', sN ''Ra'', sMV ''Rb'',+ sMV ''Bbd'', sMV ''Text2''+ |>+ , Recv ''3'' <| sAV ''Pbd'', sAV ''Abd'', sMV ''Text5'',+ PEnc <| sC ''isoiec_9798_2_6_enc_3_1'', sN ''Ra'', sMV ''Kab'',+ sAV ''Abd'', sMV ''Bbd'', sMV ''Text4''+ |>+ ( sKbd (AVar ''Abd'') (AVar ''Pbd'') ),+ sMV ''TokenPA_for_B''+ |>+ , Recv ''text4'' <| sMV ''Text6'', sMV ''Text7'' |>+ , Send ''4'' <| sAV ''Abd'', sMV ''Bbd'', sMV ''Text7'', sAV ''Pbd'',+ sMV ''TokenPA_for_B'',+ PEnc <| sC ''isoiec_9798_2_6_enc_4'', sN ''Rpa'', sMV ''Rb'',+ sMV ''Text6''+ |>+ ( sMV ''Kab'' )+ |>+ , Recv ''5'' <| sMV ''Bbd'', sAV ''Abd'', sMV ''Text9'',+ PEnc <| sC ''isoiec_9798_2_6_enc_5'', sMV ''Rb'', sN ''Rpa'',+ sMV ''Text8''+ |>+ ( sMV ''Kab'' )+ |>+ ]"++role B+where "B =+ [ Recv ''text1'' ( sMV ''Text1'' )+ , Send ''1'' <| sAV ''B'', sAV ''A'', sN ''Rb'', sMV ''Text1'' |>+ , Recv ''4'' <| sAV ''A'', sAV ''B'', sMV ''Text7'', sMV ''P'',+ PEnc <| sC ''isoiec_9798_2_6_enc_3_2'', sN ''Rb'', sMV ''Kab'',+ sAV ''A'', sMV ''Text3''+ |>+ ( PSymK ( sAV ''B'' ) ( sMV ''P'' ) ),+ PEnc <| sC ''isoiec_9798_2_6_enc_4'', sMV ''Rpa'', sN ''Rb'',+ sMV ''Text6''+ |>+ ( sMV ''Kab'' )+ |>+ , Recv ''text5'' <| sMV ''Text8'', sMV ''Text9'' |>+ , Send ''5'' <| sAV ''B'', sAV ''A'', sMV ''Text9'',+ PEnc <| sC ''isoiec_9798_2_6_enc_5'', sN ''Rb'', sMV ''Rpa'',+ sMV ''Text8''+ |>+ ( sMV ''Kab'' )+ |>+ ]"++role Bbd+where "Bbd =+ [ Recv ''text1'' ( sMV ''Text1'' )+ , Send ''1'' <| sAV ''Bbd'', sAV ''Abd'', sN ''Rb'', sMV ''Text1'' |>+ , Recv ''4'' <| sAV ''Abd'', sAV ''Bbd'', sMV ''Text7'', sMV ''Pbd'',+ PEnc <| sC ''isoiec_9798_2_6_enc_3_2'', sN ''Rb'', sMV ''Kab'',+ sAV ''Abd'', sAV ''Bbd'', sMV ''Text3''+ |>+ ( sKbd (AVar ''Bbd'') (MVar ''Pbd'') ),+ PEnc <| sC ''isoiec_9798_2_6_enc_4'', sMV ''Rpa'', sN ''Rb'',+ sMV ''Text6''+ |>+ ( sMV ''Kab'' )+ |>+ , Recv ''text5'' <| sMV ''Text8'', sMV ''Text9'' |>+ , Send ''5'' <| sAV ''Bbd'', sAV ''Abd'', sMV ''Text9'',+ PEnc <| sC ''isoiec_9798_2_6_enc_5'', sN ''Rb'', sMV ''Rpa'',+ sMV ''Text8''+ |>+ ( sMV ''Kab'' )+ |>+ ]"++role P+where "P =+ [ Recv ''2'' <| sMV ''A'', sAV ''P'', sMV ''Ra'', sMV ''Rb'', sMV ''B'',+ sMV ''Text2''+ |>+ , Recv ''text3'' <| sMV ''Text3'', sMV ''Text4'', sMV ''Text5'' |>+ , Send ''3'' <| sAV ''P'', sMV ''A'', sMV ''Text5'',+ PEnc <| sC ''isoiec_9798_2_6_enc_3_1'', sMV ''Ra'', sN ''Kab'',+ sMV ''B'', sMV ''Text4''+ |>+ ( PSymK ( sMV ''A'' ) ( sAV ''P'' ) ),+ PEnc <| sC ''isoiec_9798_2_6_enc_3_2'', sMV ''Rb'', sN ''Kab'',+ sMV ''A'', sMV ''Text3''+ |>+ ( PSymK ( sMV ''B'' ) ( sAV ''P'' ) )+ |>+ ]"++role Pbd+where "Pbd =+ [ Recv ''2'' <| sMV ''Abd'', sAV ''Pbd'', sMV ''Ra'', sMV ''Rb'',+ sMV ''Bbd'', sMV ''Text2''+ |>+ , Recv ''text3'' <| sMV ''Text3'', sMV ''Text4'', sMV ''Text5'' |>+ , Send ''3'' <| sAV ''Pbd'', sMV ''Abd'', sMV ''Text5'',+ PEnc <| sC ''isoiec_9798_2_6_enc_3_1'', sMV ''Ra'', sN ''Kab'',+ sMV ''Abd'', sMV ''Bbd'', sMV ''Text4''+ |>+ ( sKbd (MVar ''Abd'') (AVar ''Pbd'') ),+ PEnc <| sC ''isoiec_9798_2_6_enc_3_2'', sMV ''Rb'', sN ''Kab'',+ sMV ''Abd'', sMV ''Bbd'', sMV ''Text3''+ |>+ ( sKbd (MVar ''Bbd'') (AVar ''Pbd'') )+ |>+ ]"++protocol isoiec_9798_2_6+where "isoiec_9798_2_6 = { A, Abd, B, Bbd, P, Pbd }"++locale restricted_isoiec_9798_2_6_state = isoiec_9798_2_6_state++type_invariant typing_2_6 for isoiec_9798_2_6+where "typing_2_6 = mk_typing+ [ ((P, ''A''), (KnownT P_2))+ , ((Pbd, ''Abd''), (KnownT Pbd_2))+ , ((A, ''B''), (KnownT A_1))+ , ((P, ''B''), (KnownT P_2))+ , ((Abd, ''Bbd''), (KnownT Abd_1))+ , ((Pbd, ''Bbd''), (KnownT Pbd_2))+ , ((A, ''Kab''), (SumT (KnownT A_3) (NonceT P ''Kab'')))+ , ((Abd, ''Kab''), (SumT (KnownT Abd_3) (NonceT Pbd ''Kab'')))+ , ((B, ''Kab''), (SumT (KnownT B_4) (NonceT P ''Kab'')))+ , ((Bbd, ''Kab''), (SumT (KnownT Bbd_4) (NonceT Pbd ''Kab'')))+ , ((B, ''P''), (KnownT B_4))+ , ((Bbd, ''Pbd''), (KnownT Bbd_4))+ , ((P, ''Ra''), (KnownT P_2))+ , ((Pbd, ''Ra''), (KnownT Pbd_2))+ , ((A, ''Rb''), (KnownT A_1))+ , ((Abd, ''Rb''), (KnownT Abd_1))+ , ((P, ''Rb''), (KnownT P_2))+ , ((Pbd, ''Rb''), (KnownT Pbd_2))+ , ((B, ''Rpa''),+ (SumT (KnownT B_4) (SumT (NonceT A ''Rpa'') (NonceT Abd ''Rpa''))))+ , ((Bbd, ''Rpa''),+ (SumT (KnownT Bbd_4) (SumT (NonceT A ''Rpa'') (NonceT Abd ''Rpa''))))+ , ((A, ''Text1''), (KnownT A_1))+ , ((Abd, ''Text1''), (KnownT Abd_1))+ , ((B, ''Text1''), (KnownT B_text1))+ , ((Bbd, ''Text1''), (KnownT Bbd_text1))+ , ((A, ''Text2''), (KnownT A_text2))+ , ((Abd, ''Text2''), (KnownT Abd_text2))+ , ((P, ''Text2''), (KnownT P_2))+ , ((Pbd, ''Text2''), (KnownT Pbd_2))+ , ((B, ''Text3''), (KnownT B_4))+ , ((Bbd, ''Text3''), (KnownT Bbd_4))+ , ((P, ''Text3''), (KnownT P_text3))+ , ((Pbd, ''Text3''), (KnownT Pbd_text3))+ , ((A, ''Text4''), (KnownT A_3))+ , ((Abd, ''Text4''), (KnownT Abd_3))+ , ((P, ''Text4''), (KnownT P_text3))+ , ((Pbd, ''Text4''), (KnownT Pbd_text3))+ , ((A, ''Text5''), (KnownT A_3))+ , ((Abd, ''Text5''), (KnownT Abd_3))+ , ((P, ''Text5''), (KnownT P_text3))+ , ((Pbd, ''Text5''), (KnownT Pbd_text3))+ , ((A, ''Text6''), (KnownT A_text4))+ , ((Abd, ''Text6''), (KnownT Abd_text4))+ , ((B, ''Text6''), (KnownT B_4))+ , ((Bbd, ''Text6''), (KnownT Bbd_4))+ , ((A, ''Text7''), (KnownT A_text4))+ , ((Abd, ''Text7''), (KnownT Abd_text4))+ , ((B, ''Text7''), (KnownT B_4))+ , ((Bbd, ''Text7''), (KnownT Bbd_4))+ , ((A, ''Text8''), (KnownT A_5))+ , ((Abd, ''Text8''), (KnownT Abd_5))+ , ((B, ''Text8''), (KnownT B_text5))+ , ((Bbd, ''Text8''), (KnownT Bbd_text5))+ , ((A, ''Text9''), (KnownT A_5))+ , ((Abd, ''Text9''), (KnownT Abd_5))+ , ((B, ''Text9''), (KnownT B_text5))+ , ((Bbd, ''Text9''), (KnownT Bbd_text5))+ , ((A, ''TokenPA_for_B''), (KnownT A_3))+ , ((Abd, ''TokenPA_for_B''), (KnownT Abd_3))+ ]"++sublocale isoiec_9798_2_6_state < typing_2_6_state+proof -+ have "(t,r,s) : approx typing_2_6"+ proof(cases rule: reachable_in_approxI_ext+ [OF typing_2_6.monoTyp, completeness_cases_rule])+ case (A_1_B t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (A_1_Rb t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (A_1_Text1 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (A_3_Kab t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ proof(sources! "+ Enc {| LC ''isoiec_9798_2_6_enc_3_1'', LN ''Ra'' tid0,+ s(MV ''Kab'' tid0), s(MV ''B'' tid0), s(MV ''Text4'' tid0)+ |}+ ( K ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ")+ qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)?+ next+ case (A_3_Text4 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ proof(sources! "+ Enc {| LC ''isoiec_9798_2_6_enc_3_1'', LN ''Ra'' tid0,+ s(MV ''Kab'' tid0), s(MV ''B'' tid0), s(MV ''Text4'' tid0)+ |}+ ( K ( s(AV ''A'' tid0) ) ( s(AV ''P'' tid0) ) ) ")+ qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)?+ next+ case (A_3_Text5 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (A_3_TokenPA_for_B t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (A_text4_Text6 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (A_text4_Text7 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (A_5_Text8 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ proof(sources! "+ Enc {| LC ''isoiec_9798_2_6_enc_5'', s(MV ''Rb'' tid0), LN ''Rpa'' tid0,+ s(MV ''Text8'' tid0)+ |}+ ( s(MV ''Kab'' tid0) ) ")+ qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)?+ next+ case (A_5_Text9 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (Abd_1_Bbd t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (Abd_1_Rb t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (Abd_1_Text1 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (Abd_3_Kab t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ proof(sources! "+ Enc {| LC ''isoiec_9798_2_6_enc_3_1'', LN ''Ra'' tid0,+ s(MV ''Kab'' tid0), s(AV ''Abd'' tid0), s(MV ''Bbd'' tid0),+ s(MV ''Text4'' tid0)+ |}+ ( Kbd ( s(AV ''Abd'' tid0) ) ( s(AV ''Pbd'' tid0) ) ) ")+ qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)?+ next+ case (Abd_3_Text4 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ proof(sources! "+ Enc {| LC ''isoiec_9798_2_6_enc_3_1'', LN ''Ra'' tid0,+ s(MV ''Kab'' tid0), s(AV ''Abd'' tid0), s(MV ''Bbd'' tid0),+ s(MV ''Text4'' tid0)+ |}+ ( Kbd ( s(AV ''Abd'' tid0) ) ( s(AV ''Pbd'' tid0) ) ) ")+ qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)?+ next+ case (Abd_3_Text5 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (Abd_3_TokenPA_for_B t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (Abd_text4_Text6 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (Abd_text4_Text7 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (Abd_5_Text8 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ proof(sources! "+ Enc {| LC ''isoiec_9798_2_6_enc_5'', s(MV ''Rb'' tid0), LN ''Rpa'' tid0,+ s(MV ''Text8'' tid0)+ |}+ ( s(MV ''Kab'' tid0) ) ")+ qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)?+ next+ case (Abd_5_Text9 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (B_4_Kab t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ proof(sources! "+ Enc {| LC ''isoiec_9798_2_6_enc_3_2'', LN ''Rb'' tid0,+ s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(MV ''Text3'' tid0)+ |}+ ( K ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ")+ qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)?+ next+ case (B_4_P t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (B_4_Rpa t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ proof(sources! "+ Enc {| LC ''isoiec_9798_2_6_enc_4'', s(MV ''Rpa'' tid0), LN ''Rb'' tid0,+ s(MV ''Text6'' tid0)+ |}+ ( s(MV ''Kab'' tid0) ) ")+ qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)?+ next+ case (B_4_Text3 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ proof(sources! "+ Enc {| LC ''isoiec_9798_2_6_enc_3_2'', LN ''Rb'' tid0,+ s(MV ''Kab'' tid0), s(AV ''A'' tid0), s(MV ''Text3'' tid0)+ |}+ ( K ( s(AV ''B'' tid0) ) ( s(MV ''P'' tid0) ) ) ")+ qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)?+ next+ case (B_4_Text6 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ proof(sources! "+ Enc {| LC ''isoiec_9798_2_6_enc_4'', s(MV ''Rpa'' tid0), LN ''Rb'' tid0,+ s(MV ''Text6'' tid0)+ |}+ ( s(MV ''Kab'' tid0) ) ")+ qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)?+ next+ case (B_4_Text7 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (B_text5_Text8 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (B_text5_Text9 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (Bbd_4_Kab t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ proof(sources! "+ Enc {| LC ''isoiec_9798_2_6_enc_3_2'', LN ''Rb'' tid0,+ s(MV ''Kab'' tid0), s(AV ''Abd'' tid0), s(AV ''Bbd'' tid0),+ s(MV ''Text3'' tid0)+ |}+ ( Kbd ( s(AV ''Bbd'' tid0) ) ( s(MV ''Pbd'' tid0) ) ) ")+ qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)?+ next+ case (Bbd_4_Pbd t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (Bbd_4_Rpa t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ proof(sources! "+ Enc {| LC ''isoiec_9798_2_6_enc_4'', s(MV ''Rpa'' tid0), LN ''Rb'' tid0,+ s(MV ''Text6'' tid0)+ |}+ ( s(MV ''Kab'' tid0) ) ")+ qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)?+ next+ case (Bbd_4_Text3 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ proof(sources! "+ Enc {| LC ''isoiec_9798_2_6_enc_3_2'', LN ''Rb'' tid0,+ s(MV ''Kab'' tid0), s(AV ''Abd'' tid0), s(AV ''Bbd'' tid0),+ s(MV ''Text3'' tid0)+ |}+ ( Kbd ( s(AV ''Bbd'' tid0) ) ( s(MV ''Pbd'' tid0) ) ) ")+ qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)?+ next+ case (Bbd_4_Text6 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ proof(sources! "+ Enc {| LC ''isoiec_9798_2_6_enc_4'', s(MV ''Rpa'' tid0), LN ''Rb'' tid0,+ s(MV ''Text6'' tid0)+ |}+ ( s(MV ''Kab'' tid0) ) ")+ qed (insert facts, ((fastforce intro: event_predOrdI split: if_splits))+)?+ next+ case (Bbd_4_Text7 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (Bbd_text5_Text8 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (Bbd_text5_Text9 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (P_2_A t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (P_2_B t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (P_2_Ra t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (P_2_Rb t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (P_2_Text2 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (P_text3_Text3 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (P_text3_Text4 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (P_text3_Text5 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (Pbd_2_Abd t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (Pbd_2_Bbd t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (Pbd_2_Ra t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (Pbd_2_Rb t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (Pbd_2_Text2 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (Pbd_text3_Text3 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (Pbd_text3_Text4 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ next+ case (Pbd_text3_Text5 t r s tid0) note facts = this+ then interpret state: typing_2_6_state t r s+ by unfold_locales auto+ show ?case using facts+ by (fastforce intro: event_predOrdI split: if_splits)+ qed+ thus "typing_2_6_state t r s" by unfold_locales auto+qed++text{* Prove secrecy of long-term keys. *}+context isoiec_9798_2_6_state begin++ (* This rule is unsafe in general, but OK here, + as we are only reasoning about static compromise. + *)+ lemma static_longterm_key_reveal[dest!]:+ "predOrd t (LKR a) e ==> RLKR a : reveals t"+ by (auto intro: compr_predOrdI)++ lemma longterm_private_key_secrecy:+ assumes facts:+ "SK m : knows t"+ "RLKR m ~: reveals t"+ shows "False"+ using facts by (sources "SK m")++ lemma longterm_sym_ud_key_secrecy:+ assumes facts:+ "K m1 m2 : knows t"+ "RLKR m1 ~: reveals t"+ "RLKR m2 ~: reveals t"+ shows "False"+ using facts by (sources "K m1 m2")++ lemma longterm_sym_bd_key_secrecy:+ assumes facts:+ "Kbd m1 m2 : knows t"+ "RLKR m1 ~: reveals t"+ "RLKR m2 ~: reveals t"+ "m1 : Agent"+ "m2 : Agent"+ shows "False"+ proof -+ from facts + have "KShr (agents {m1, m2}) : knows t"+ by (auto simp: Kbd_def)+ thus ?thesis using facts+ proof (sources "KShr (agents {m1, m2})")+ qed (auto simp: agents_def Agent_def)+ qed++ lemmas ltk_secrecy =+ longterm_sym_ud_key_secrecy+ longterm_sym_ud_key_secrecy[OF in_knows_predOrd1]+ longterm_sym_bd_key_secrecy+ longterm_sym_bd_key_secrecy[OF in_knows_predOrd1]+ longterm_private_key_secrecy+ longterm_private_key_secrecy[OF in_knows_predOrd1]++end++end
+ data/examples/iso9798/isoiec-9798.spthy view
@@ -0,0 +1,1619 @@+// All protocols in a single file to test their parallel composition.+// Author: Simon Meier <iridcode@gmail.com>+// Created: 2013-03-21+//+// Note that we have to specially deal with the 2_5 and 2_6 protocols, as+// their automatically computed type invariants are not sound. We therefore+// compose them manually and use a manual type invariant, which we derived+// from the automatically computed one. These two manually composed protocols+// can be found at the end of this file.+//+// Note also our proof checking automation that we implemented in Isabelle+// suffers from a scaling problem when verifying the proof script resutling+// ceritfying the correctness of the parallel composition of all protocols in+// this file. We therefore do not include checking this file in the+// regressions tests.+theory isoiec_9798 begin++/*++// %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+// 2 - bdkey+// %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++/*+ * Modeled from ISO/IEC 9798-2+ * Modeler: Cas Cremers, Dec. 2010+ * Ported to scyther-proof: Simon Meier, Feb. 2011+ *+ * Modeling notes:+ * - Variant of ISO/IEC 9798-2 with bidirectional keys k[A,B].+ * - time-variant-parameters, time-stamps, and sequence numbers are+ * modeled by nonces leaked to the adversary at the start of a role.+ * - The TextX fields are chosen by the adversary.+ */+++/******************************************************************************+ * Protocol 1+ ******************************************************************************+ *+ * symmetric+ * one-pass+ * unilateral+ *+ * Note: the identity B may be ommitted, if+ * (a) the environment disallows such attacks, or+ * (b) a unidirectional key is used+ * (This formulation directly stems from the standard.)+ */+protocol isoiec_9798_2_1_bdkey+{+ leak_A. A -> : TNA++ text_1. -> A: Text1, Text2+ 1. A -> B: A, B, Text2, {'isoiec_9798_2_1_enc_1', TNA, B, Text1 }k[A,B]+}++// Here we dont get any injective agreement, as there could be two B thread+// receiving the same message from one A.+property (of isoiec_9798_2_1_bdkey)+ B_non_injective_agreement:+ niagree(B_1[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A, B})+++/******************************************************************************+ * Protocol 2+ ******************************************************************************+ *+ * symmetric+ * two-pass+ * unilateral+ *+ * Note: the identity B may be ommitted, if+ * (a) the environment disallows such attacks, or+ * (b) a unidirectional key is used+ */+protocol isoiec_9798_2_2_bdkey+{+ text_1. -> B: Text1+ 1. B -> A: B, A, RB, Text1++ text_2. -> A: Text2, Text3+ 2. A -> B: A, B, Text3, {'isoiec_9798_2_2_enc_2', RB, B, Text2}k[B,A]+}++property (of isoiec_9798_2_2_bdkey)+ B_injective_agreement:+ iagree(B_2[A,B,RB,Text2] -> A_2[A,B,RB,Text2], {A, B})++++/******************************************************************************+ * Protocol 3+ ******************************************************************************+ *+ * symmetric+ * two-pass+ * mutual+ *+ * Note: the identities inside the encryptions may be ommitted, if+ * (a) the environment disallows such attacks, or+ * (b) a unidirectional key is used+ */+protocol isoiec_9798_2_3_bdkey+{+ leak_A. A -> : TNA+ leak_B. B -> : TNB++ text_1. -> A: Text1, Text2+ 1. A -> B: A, B, Text2, {'isoiec_9798_2_3_enc_1', TNA, B, Text1 }k[A,B]++ text_2. -> B: Text3, Text4+ 2. B -> A: B, A, Text4, {'isoiec_9798_2_3_enc_2', TNB, A, Text3 }k[B,A]+}++// NOTE: We do not get injective agreement here, in neither direction. The+// problem is the same as in isoiec_9798_2_1_bdkey. However, we are missing+// the opportunity to strengthen the property for A, as we could just embed+// TNA in the message sent from B.+properties (of isoiec_9798_2_3_bdkey)+ A_non_injective_agreement:+ niagree(A_2[A,B,TNB,Text3] -> B_2[A,B,TNB,Text3], {A, B})++ B_non_injective_agreement:+ niagree(B_1[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A, B})+++/******************************************************************************+ * Protocol 4+ ******************************************************************************+ *+ * symmetric+ * three-pass+ * mutual+ *+ * Note: the identity B inside the encryption may be ommitted, if+ * (a) the environment disallows such attacks, or+ * (b) a unidirectional key is used+ *+ */+protocol isoiec_9798_2_4_bdkey+{+ text_1. -> B: Text1+ 1. B -> A: B, A, RB, Text1++ text_2. -> A: Text2, Text3+ 2. A -> B: A, B, Text3, {'isoiec_9798_2_4_enc_1', RA, RB, B, Text2 }k[A,B]++ text_3. -> B: Text4, Text5+ 3. B -> A: B, A, Text5, {'isoiec_9798_2_4_enc_2', RB, RA, Text4 }k[A,B]+}++properties (of isoiec_9798_2_4_bdkey)+ A_injective_agreement:+ iagree(A_3[A,B,RA,RB,Text2,Text4] -> B_3[A,B,RA,RB,Text2,Text4], {A, B})++ B_injective_agreement:+ iagree(B_2[A,B,RA,RB,Text2] -> A_2[A,B,RA,RB,Text2], {A, B})++++/******************************************************************************+ * Protocol 5 (with the assumption that the TTP does not play other roles)+ ******************************************************************************+ *+ * symmetric+ * ttp+ * four-pass+ * mutual+ *+ * Modeling notes:+ * - The use of TNb in message 4, as specified by the ISO standard, is+ * different from other models, in which it was TNa.+ * - We MUST assume that the trusted third party does not execute the A role.+ * Otherwise, some authentication properties break (see below).+ * - We send identity P in Step 3 in order for B to be able to lookup key k[B,P]+ */+protocol isoiec_9798_2_5_special_TTP_bdkey+{+ leak_A. A -> : TVPa, TNa+ leak_B. B -> : TNb+ leak_P. P -> : TNp++ text_1. -> A: Text1+ 1. A -> P: A, P, TVPa, B, Text1++ text_2. -> P: Text2, Text3, Text4+ 2. P -> : P, A, Text4, { 'isoiec_9798_2_5_special_TTP_enc_2_1', TVPa, Kab, B, Text3 }k[A,P]+ , { 'isoiec_9798_2_5_special_TTP_enc_2_2', TNp , Kab, A, Text2 }k[B,P]+ -> A: P, A, Text4, { 'isoiec_9798_2_5_special_TTP_enc_2_1', TVPa, Kab, B, Text3 }k[A,P]+ , TokenPA_for_B++ text_3. -> A: Text5, Text6+ 3. A -> : A, B, Text6, P, TokenPA_for_B+ , { 'isoiec_9798_2_5_special_TTP_enc_3', TNa, B, Text5 }Kab+ -> B: A, B, Text6, P, { 'isoiec_9798_2_5_special_TTP_enc_2_2', TNp, Kab, A, Text2 }k[B,P]+ , { 'isoiec_9798_2_5_special_TTP_enc_3', TNa, B, Text5 }Kab++ text_4. -> B: Text7, Text8+ 4. B -> A: B, A, Text8, { 'isoiec_9798_2_5_special_TTP_enc_4', TNb, A, Text7 }Kab+}++axiom (of isoiec_9798_2_5_special_TTP_bdkey) different_actors_A_P:+ premises+ "role(0) = A"+ "role(1) = P"+ "A#0 = P#1"+ imply+ "False"++properties (of isoiec_9798_2_5_special_TTP_bdkey)+ P_secret_Kab: secret(P, -, Kab, {A, B, P})+ A_secret_Kab: secret(A, 2, Kab, {A, B, P})+ B_secret_Kab: secret(B, 3, Kab, {A, B, P})++ // Agreement properties strengthened with respect to Cas Cremers' models:+ // (a) we also verify agreement on the freshness data TNa, TNb+ // (b) we also verify agreement with the trusted third party+ //+ // Note: If no axiom dependency is noted for a property below, then it can+ // be proven without the axiom.++ A_injective_agreement_B:+ iagree(A_4[A,B,P,Kab,TNa,Text5,TNb,Text7] -> B_4[A,B,P,Kab,TNa,Text5,TNb,Text7], {A, B, P})++ // Depends on 'different_actors_A_P'+ //+ // NO injective agreement can be proven. There may be several B-threads+ // communicating with the same A-thread! Checking the 'TNb' timestamp in+ // later steps could be used to remove this problem, up to the clock+ // resolution.+ B_non_injective_agreement_A:+ niagree(B_3[A,B,P,Kab,TNa,Text5] -> A_3[A,B,P,Kab,TNa,Text5], {A, B, P})++ // depends on 'different_actors_A_P'+ A_injective_agreement_P:+ iagree(A_2[A,B,P,Kab,TVPa,Text3] -> P_2[A,B,P,Kab,TVPa,Text3], {A, B, P})++ // No injective agreement, as the TTP does not receive any message from 'B'.+ B_non_injective_agreement_P:+ niagree(B_3[A,B,P,Kab,TNp,Text2] -> P_2[A,B,P,Kab,TNp,Text2], {A, B, P})+++/******************************************************************************+ * Protocol 6 (with the assumption that the TTP does not play other roles)+ ******************************************************************************+ *+ * symmetric+ * ttp+ * five-pass+ * mutual+ *+ * Modeling notes:+ * - We send identity P in Step 4 in order for B to be able to lookup key k[B,P]+ * - We MUST assume that the trusted third party does not execute any of the+ * other roles. Otherwise, some authentication properties break (see below).+ *+ * MPA Attack reported by Mathuria:+ * - Type flaw MPA when in parallel with Abadi-Needham protocol.+ */+protocol isoiec_9798_2_6_special_TTP_bdkey+{+ text_1. -> B: Text1+ 1. B -> A: B, A, Rb, Text1++ text_2. -> A: Text2+ 2. A -> P: A, P, Ra, Rb, B, Text2++ text_3. -> P: Text3, Text4, Text5+ 3. P -> : P, A, Text5, {'isoiec_9798_2_6_special_TTP_enc_3_1', Ra, Kab, B, Text4}k[A,P]+ , {'isoiec_9798_2_6_special_TTP_enc_3_2', Rb, Kab, A, Text3}k[B,P]+ -> A: P, A, Text5, {'isoiec_9798_2_6_special_TTP_enc_3_1', Ra, Kab, B, Text4}k[A,P]+ , TokenPA_for_B++ text_4. -> A: Text6, Text7+ 4. A -> : A, B, Text7, P, TokenPA_for_B+ , {'isoiec_9798_2_6_special_TTP_enc_4', Rpa, Rb, Text6}Kab+ -> B: A, B, Text7, P, {'isoiec_9798_2_6_special_TTP_enc_3_2', Rb, Kab, A, Text3}k[B,P]+ , {'isoiec_9798_2_6_special_TTP_enc_4', Rpa, Rb, Text6}Kab++ text_5. -> B: Text8, Text9+ 5. B -> A: B, A, Text9, {'isoiec_9798_2_6_special_TTP_enc_5', Rb, Rpa, Text8}Kab+}++axiom (of isoiec_9798_2_6_special_TTP_bdkey) different_actors_A_P:+ premises+ "role(0) = A"+ "role(1) = P"+ "A#0 = P#1"+ imply+ "False"++axiom (of isoiec_9798_2_6_special_TTP_bdkey) different_actors_B_P:+ premises+ "role(0) = B"+ "role(1) = P"+ "B#0 = P#1"+ imply+ "False"++properties (of isoiec_9798_2_6_special_TTP_bdkey)+ P_secret_Kab: secret(P, -, Kab, {A, B, P})+ A_secret_Kab: secret(A, 3, Kab, {A, B, P})+ B_secret_Kab: secret(B, 4, Kab, {A, B, P})++ // Agreement properties strengthened with respect to Cas Cremers' models:+ // (a) we also verify agreement on the freshness data+ // (b) we also verify agreement with the trusted third party+ //+ // Note: If no axiom dependency is noted for a property below, then it can+ // be proven without the axiom.++ // depends on 'different_actors_B_P' and 'different_actors_A_P'+ A_injective_agreement_B:+ iagree(A_5[A,B,P,Kab,Rpa,Rb,Text6,Text8] -> B_5[A,B,P,Kab,Rpa,Rb,Text6,Text8], {A, B, P})++ // depends on 'different_actors_B_P' and 'different_actors_A_P'+ B_injective_agreement_A:+ iagree(B_4[A,B,P,Kab,Rpa,Rb,Text6] -> A_4[A,B,P,Kab,Rpa,Rb,Text6], {A, B, P})++ // depends on 'different_actors_A_P+ A_injective_agreement_P:+ iagree(A_3[A,B,P,Ra,Kab,Text4] -> P_3[A,B,P,Ra,Kab,Text4], {A, B, P})++ // depends on 'different_actors_B_P+ B_injective_agreement_P:+ iagree(B_4[A,B,P,Rb,Kab,Text3] -> P_3[A,B,P,Rb,Kab,Text3], {A, B, P})++// %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+// 2 - udkey+// %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++/*+ * Modeled from ISO/IEC 9798-2+ * Modeler: Cas Cremers, Dec. 2010+ * Ported to scyther-proof: Simon Meier, Feb. 2011+ *+ * Modeling notes:+ * - Variant of ISO/IEC 9798-2 with unidirectional keys k(A,B) and all+ * optional identities dropped.+ * - time-variant-parameters, time-stamps, and sequence numbers are+ * modeled by nonces leaked to the adversary at the start of a role.+ * - The TextX fields are chosen by the adversary.+ */+++/******************************************************************************+ * Protocol 1+ ******************************************************************************+ *+ * symmetric+ * one-pass+ * unilateral+ *+ * Note: the identity B is ommitted because a unidirectional key is used+ */+protocol isoiec_9798_2_1_udkey+{+ leak_A. A -> : TNA++ text_1. -> A: Text1, Text2+ 1. A -> B: A, B, Text2, {'isoiec_9798_2_1_enc_1', TNA, Text1 }k(A,B)+}++// Here we dont get any injective agreement, as there could be two B thread+// receiving the same message from one A.+property (of isoiec_9798_2_1_udkey)+ B_non_injective_agreement:+ niagree(B_1[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A, B})+++/******************************************************************************+ * Protocol 2+ ******************************************************************************+ *+ * symmetric+ * two-pass+ * unilateral+ *+ * Note: the identity is ommitted because a unidirectional key is used+ */+protocol isoiec_9798_2_2_udkey+{+ text_1. -> B: Text1+ 1. B -> A: B, A, RB, Text1++ text_2. -> A: Text2, Text3+ 2. A -> B: A, B, Text3, {'isoiec_9798_2_2_enc_2', RB, Text2}k(A,B)+}++property (of isoiec_9798_2_2_udkey)+ B_injective_agreement:+ iagree(B_2[A,B,RB,Text2] -> A_2[A,B,RB,Text2], {A, B})++++/******************************************************************************+ * Protocol 3+ ******************************************************************************+ *+ * symmetric+ * two-pass+ * mutual+ *+ * Note: the identities are ommitted because a unidirectional key is used+ */+protocol isoiec_9798_2_3_udkey+{+ leak_A. A -> : TNA+ leak_B. B -> : TNB++ text_1. -> A: Text1, Text2+ 1. A -> B: A, B, Text2, {'isoiec_9798_2_3_enc_1', TNA, Text1 }k(A,B)++ text_2. -> B: Text3, Text4+ 2. B -> A: B, A, Text4, {'isoiec_9798_2_3_enc_2', TNB, Text3 }k(B,A)+}++// NOTE: We do not get injective agreement here, in neither direction. The+// problem is the same as in isoiec_9798_2_1_bdkey. However, we are missing+// the opportunity to strengthen the property for A, as we could just embed+// TNA in the message sent from B.+properties (of isoiec_9798_2_3_udkey)+ A_non_injective_agreement:+ niagree(A_2[A,B,TNB,Text3] -> B_2[A,B,TNB,Text3], {A, B})++ B_non_injective_agreement:+ niagree(B_2[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A, B})++++/******************************************************************************+ * Protocol 4+ ******************************************************************************+ *+ * symmetric+ * three-pass+ * mutual+ *+ * Note: the identities are ommitted because a unidirectional key is used+ *+ * In case (b), modeled here, the second key is reversed and the identities are+ * omitted in the ciphertexts.+ */+protocol isoiec_9798_2_4_udkey+{+ text_1. -> B: Text1+ 1. B -> A: B, A, RB, Text1++ text_2. -> A: Text2, Text3+ 2. A -> B: A, B, Text3, {'isoiec_9798_2_4_enc_1', RA, RB, Text2 }k(A,B)++ text_3. -> B: Text4, Text5+ 3. B -> A: B, A, Text5, {'isoiec_9798_2_4_enc_2', RB, RA, Text4 }k(B,A)+}++properties (of isoiec_9798_2_4_udkey)+ A_injective_agreement:+ iagree(A_3[A,B,RA,RB,Text2,Text4] -> B_3[A,B,RA,RB,Text2,Text4], {A, B})++ B_injective_agreement:+ iagree(B_2[A,B,RA,RB,Text2] -> A_2[A,B,RA,RB,Text2], {A, B})++++// %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+// 3+// %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++/*+ * Modeled from ISO/IEC 9798+ * Modeler: Cas Cremers, Dec. 2010+ * Adapted for scyther-proof: Simon Meier, Feb. 2011+ *+ * Modeling notes:+ * - We allow the adversary to choose the content of all TextX fields.+ * - time-variant-parameters, time-stamps, and sequence numbers are+ * modeled by nonces leaked to the adversary at the start of a role.+ * - Given some pattern 'pkA', then the signature pattern 'sign{m}pkA' is+ * translated to the message '(m, {m}inv(pkA))' upon execution.+ */++/****************************************************************************+ * Protocol 1+ ****************************************************************************+ *+ * signature+ * one-pass+ * unilateral+ *+ * Modeling notes:+ * - we assume that pk(A) is already known to B+ */+++protocol isoiec_9798_3_1+{+ leak_A. A -> : TNA++ text_1. -> A: Text1, Text2+ 1. A -> B: A, B, Text2,+ sign{'isoiec_9798_3_1_sig_1', TNA, B, Text1 }pk(A)+}++// No injective agreement here.+properties (of isoiec_9798_3_1)+ B_non_injective_agreement:+ niagree(B_1[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A})+++/****************************************************************************+ * Protocol 2+ ****************************************************************************+ *+ * signature+ * two-pass+ * unilateral+ *+ * Modeling notes:+ * - we assume that pk(A) is already known to B+ */+protocol isoiec_9798_3_2+{+ text_1. -> B: Text1+ 1. B -> A: B, A, Rb, Text1++ text_2. -> A: Text2, Text3+ 2. A -> B: A, B, Text3,+ sign{'isoiec_9798_3_2_sig_2', Ra, Rb, B, Text2 }pk(A)+}++properties (of isoiec_9798_3_2)+ B_injective_agreement:+ iagree(B_2[A,B,Ra,Rb,Text2] -> A_2[A,B,Ra,Rb,Text2], {A})+++/****************************************************************************+ * Protocol 3+ ****************************************************************************+ *+ * signature+ * two-pass+ * mutual+ * parallel+ *+ * Modeling notes:+ * - Here we only verify a sequential model of the protocol.+ * - We assume that the public keys are already predistributed.+ */+protocol isoiec_9798_3_3+{+ leak_A. A -> : TNA+ leak_B. B -> : TNB++ text_1. -> A: Text1, Text2+ 1. A -> B: A, B, Text2,+ sign{'isoiec_9798_3_3_sig_1', TNA, B, Text1 }pk(A)++ text_2. -> B: Text3, Text4+ 2. B -> A: A, B, Text4,+ sign{'isoiec_9798_3_3_sig_2', TNB, A, Text3 }pk(B)+}++// No injective agreement. It requires a forth and back message, which does+// not exist for role B. For role 'A', we miss an opportunity for injective+// authentication, as we could include 'TNA' in the second message exchange.+properties (of isoiec_9798_3_3)+ A_non_injective_agreement:+ niagree(A_2[A,B,TNB,Text3] -> B_2[A,B,TNB,Text3], {B})++ B_non_injective_agreement:+ niagree(B_1[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A})+++/****************************************************************************+ * Protocol 4+ ****************************************************************************+ *+ * signature+ * three-pass+ * mutual+ *+ * Modeling notes:+ * - We assume that the public keys are already predistributed.+ */+protocol isoiec_9798_3_4+{+ text_1. -> B: Text1+ 1. B -> A: B, A, RB, Text1++ text_2. -> A: Text2, Text3+ 2. A -> B: A, B, Text3,+ sign{'isoiec_9798_3_4_sig_1', RA, RB, B, Text2 }pk(A)++ text_3. -> B: Text4, Text5+ 3. B -> A: B, A, Text5,+ sign{'isoiec_9798_3_4_sig_2', RB, RA, A, Text4 }pk(B)+}++properties (of isoiec_9798_3_4)+ // The identity A in Step 3 is required for this property to hold.+ A_injective_agreement:+ iagree(A_3[A,B,RA,RB,Text2,Text4] -> B_3[A,B,RA,RB,Text2,Text4], {A,B})++ // The identity B in Step 2 is required for this property to hold.+ B_injective_agreement:+ iagree(B_2[A,B,RA,RB,Text2] -> A_2[A,B,RA,RB,Text2], {A})+++/****************************************************************************+ * Protocol 5+ ****************************************************************************+ *+ * signature+ * two-pass+ * mutual+ * parallel+ *+ * Modeling notes:+ * - unnecessary sequentialization in the model.+ * - we assume that the public keys are already predistributed.+ */+protocol isoiec_9798_3_5+{+ text_1. -> A: Text1+ 1. A -> B: A, B, RA, Text1++ text_2. -> B: Text2+ 2. B -> A: B, A, RB, Text2++ text_3. -> B: Text5, Text6+ 3. B -> A: B, A, Text6,+ sign{'isoiec_9798_3_5_sig_1', RB, RA, A, Text5 }pk(B)++ text_4. -> A: Text3, Text4+ 4. A -> B: A, B, Text4,+ sign{'isoiec_9798_3_5_sig_2', RA, RB, B, Text3 }pk(A)+}++properties (of isoiec_9798_3_5)+ // The identity A in Step 3 is required for this property to hold.+ A_injective_agreement:+ iagree(A_3[A,B,RA,RB,Text5] -> B_3[A,B,RA,RB,Text5], {B})++ // The identity B in Step 4 is required for this property to hold.+ B_injective_agreement:+ iagree(B_4[A,B,RA,RB,Text3,Text5] -> A_4[A,B,RA,RB,Text3,Text5], {A,B})+++/****************************************************************************+ * Protocol 6 (Option 1)+ ****************************************************************************+ *+ * signature+ * ttp+ * five-pass+ * mutual+ *+ * A initiates and also communicates with T+ *+ * Modeling notes:+ * - We model the case where T sends the public keys instead of just verifying+ * the certificates; i.e., 'ResA = (A, pk(A))' and 'ResB = (B, pk(B))'.+ * - Option 1 and Option 2 must not share tags!+ */+protocol isoiec_9798_3_6_1+{+ text_1. -> A: Text1+ 1. A -> B: A, B, Ra, Text1++ text_2. -> B: Text2, Text3+ 2. B -> : A, B, Ra, Rb, Text3,+ sign{'isoiec_9798_3_6_opt_1_sig_2', B, Ra, Rb, A, Text2}pk(B)++ -> A: A, B, Ra, Rb, Text3,+ TokenBA++ text_3. -> A: Text4+ 3. A -> T: A, T, Rpa, Rb, B, Text4++ text_4. -> T: Text5, Text6, Text7+ 4. T -> : T, A, Text7, A, pk(A), B, pk(B),+ sign{'isoiec_9798_3_6_opt_1_sig_4_1', Rpa, B, pk(B), Text6}pk(T),+ sign{'isoiec_9798_3_6_opt_1_sig_4_2', Rb, A, pk(A), Text5}pk(T)++ -> A: T, A, Text7, A, pk(A), B, pkB,+ sign{'isoiec_9798_3_6_opt_1_sig_4_1', Rpa, B, pkB, Text6}pk(T),+ TokenTA_for_B++ // Here, A checks TokenBA against the public key pkB received from T.+ // As we lack support for additionally checked equalities, A sends a message+ // to itself encrypted with a fresh nonce to emulate the equality check.+ check_4_out. A -> : {'check_4',+ TokenBA+ }check_nonce_4+ check_4_in. -> A: {'check_4',+ sign{'isoiec_9798_3_6_opt_1_sig_2', B, Ra, Rb, A, Text2}pkB+ }check_nonce_4++ // Note: we additionally send T such that B knows which key to use for+ // checking TokenTA_for_B+ text_5. -> A: Text8, Text9+ 5. A -> : A, B, Text9, T,+ TokenTA_for_B,+ sign{'isoiec_9798_3_6_opt_1_sig_5', Rb, Ra, B, A, Text8}pk(A)++ -> B: A, B, Text9, T,+ sign{'isoiec_9798_3_6_opt_1_sig_4_2', Rb, A, pkA, Text5}pk(T),+ sign{'isoiec_9798_3_6_opt_1_sig_5', Rb, Ra, B, A, Text8}pkA+}++// All properties except hold injectively. NOTE: Investigate this+// authentication "flaw" between Ra5 and Ra in role 'B'.+properties (of isoiec_9798_3_6_1)+ A_injective_agreement:+ iagree(A_5[A,B,Ra,Rb,Text2] -> B_2[A,B,Ra,Rb,Text2], {B, T})++ B_injective_agreement:+ iagree(B_5[A,B,Ra,Rb,Text8] -> A_5[A,B,Ra,Rb,Text8], {A, T})++ // We additionally verify agreement of A and B with the TTP T.+ A_injective_agreement_T:+ iagree(A_5[B,T,Rpa,pkB ,Text6] ->+ T_4[B,T,Rpa,pk(B),Text6], {T})++ B_injective_agreement_T:+ iagree(B_5[A,T,Rb,pkA ,Text5] ->+ T_4[A,T,Rb,pk(A),Text5], {T})++++/****************************************************************************+ * Protocol 6 (Option 2)+ ****************************************************************************+ *+ * signature+ * ttp+ * five-pass+ * mutual+ *+ * A initiates and also communicates with T+ *+ * Modeling notes:+ * - Option 1 and Option 2 must not share tags!+ * - We model the case where T sends the public keys instead of just verifying+ * the certificates; i.e., 'ResA = (A, pk(A))' and 'ResB = (B, pk(B))'.+ * - Our model might perform a few equality checks more than what is strictly+ * required by the standard. All of them are practically feasible and we+ * advise to implement them. We do not verify whether we the security+ * properties also hold with fewer equality checks.+ */+protocol isoiec_9798_3_6_2+{+ text_1. -> A: Text1+ 1. A -> B: A, B, Ra, Text1++ text_2. -> B: Text2, Text3+ 2. B -> : A, B, Ra, Rb, Text3,+ sign{'isoiec_9798_3_6_opt_2_sig_2', B, Ra, Rb, A, Text2}pk(B)++ -> A: A, B, Ra, Rb, Text3,+ TokenBA++ text_3. -> A: Text4+ 3. A -> T: A, T, Rpa, Rb, B, Text4++ // Note: Text6 is not used in Option 2+ text_4. -> T: Text5, Text7+ 4. T -> : T, A, Text7, A, pk(A), B, pk(B),+ sign{ 'isoiec_9798_3_6_opt_2_sig_4',+ Rpa, Rb, A, pk(A), B, pk(B), Text5 }pk(T)+ -> A: T, A, Text7, A, pk(A), B, pkB,+ TokenTA++ // Here, A first checks TokenTA and then checks TokenBA against the public+ // key received from T. As we lack support for additionally checked+ // equalities, A sends a message to itself encrypted with a fresh nonce to+ // emulate the equality check.+ check_4_out. A -> : {'check_4',+ TokenTA,+ TokenBA+ }check_nonce_4+ check_4_in. -> A: {'check_4',+ sign{'isoiec_9798_3_6_opt_2_sig_4',+ Rpa, Rb, A, pkA, B, pkB, Text5 }pk(T),+ sign{'isoiec_9798_3_6_opt_2_sig_2', B, Ra, Rb, A, Text2}pkB+ }check_nonce_4++ // Note: we additionally send T such that B knows which key to use for+ // checking TokenTA+ text_5. -> A: Text8, Text9+ 5. A -> : A, B, Rpa, Text9, T,+ TokenTA,+ sign{'isoiec_9798_3_6_opt_2_sig_5', Rb, Ra, B, A, Text8}pk(A)++ -> B: A, B, Rpa, Text9, T,+ sign{'isoiec_9798_3_6_opt_2_sig_4',+ Rpa, Rb, A, pkA, B, pkB, Text5 }pk(T),+ sign{'isoiec_9798_3_6_opt_2_sig_5', Rb, Ra, B, A, Text8}pkA+}++properties (of isoiec_9798_3_6_2)+ // Note that we do not get agreement on T!+ A_injective_agreement:+ iagree(A_5[A,B,Ra,Rb,Text2] -> B_2[A,B,Ra,Rb,Text2], {B, T})++ B_injective_agreement:+ iagree(B_5[A,B,Ra,Rb,Text8] -> A_5[A,B,Ra,Rb,Text8], {A, T})++ // We additionally verify agreement of A and B with the TTP T+ A_injective_agreement_T:+ iagree(A_5[A,B,T,Rpa,Rb,pkA ,pkB ,Text5] ->+ T_4[A,B,T,Rpa,Rb,pk(A),pk(B),Text5], {T})++ B_injective_agreement_T:+ iagree(B_5[A,B,T,Rpa,Rb,pkA ,pkB ,Text5] ->+ T_4[A,B,T,Rpa,Rb,pk(A),pk(B),Text5], {T})++++/****************************************************************************+ * Protocol 7 (Option 1)+ ****************************************************************************+ *+ * signature+ * ttp+ * five-pass+ * mutual+ *+ * B initiates and A communicates with T+ *+ * Modeling notes:+ * - Option 1 and Option 2 must not share tags!+ * - We model the case where T sends the public keys instead of just verifying+ * the certificates; i.e., 'ResA = (A, pk(A))' and 'ResB = (B, pk(B))'.+ * - Our model might perform a few equality checks more than what is strictly+ * required by the standard. All of them are practically feasible and we+ * advise to implement them. We do not verify whether we the security+ * properties also hold with fewer equality checks.+ */+protocol isoiec_9798_3_7_1+{+ text_1. -> B: Text1+ 1. B -> A: B, A, Rb, Text1++ text_2. -> A: Text2+ 2. A -> T: A, T, Rpa, Rb, A, B, Text2++ text_3. -> T: Text3, Text4, Text5+ 3. T -> : T, A, Text5, A, pk(A), B, pk(B),+ sign{ 'isoiec_9798_3_7_opt_1_sig_3_1', Rpa, B, pk(B), Text4 }pk(T),+ sign{ 'isoiec_9798_3_7_opt_1_sig_3_2', Rb, A, pk(A), Text3 }pk(T)+ -> A: T, A, Text5, A, pk(A), B, pkB,+ sign{ 'isoiec_9798_3_7_opt_1_sig_3_1', Rpa, B, pkB, Text4 }pk(T),+ TokenTA_for_B++ // Note: we additionally send T such that B knows which key to use for+ // checking TokenTA+ text_4. -> A: Text6, Text7+ 4. A -> : A, B, Rpa, Text7, T,+ TokenTA_for_B,+ sign{'isoiec_9798_3_7_opt_1_sig_4', Rb, Ra, B, A, Text6}pk(A)++ -> B: A, B, Rpa, Text9, T,+ sign{'isoiec_9798_3_7_opt_1_sig_3_2', Rb, A, pkA, Text3}pk(T),+ sign{'isoiec_9798_3_7_opt_1_sig_4', Rb, Ra, B, A, Text6}pkA++ text_5. -> B: Text8, Text9+ 5. B -> : A, B, Ra, Rb, Text9,+ sign{'isoiec_9798_3_7_opt_1_sig_5', Ra, Rb, A, B, Text8}pk(B)++ -> A: A, B, Ra, Rb, Text9,+ sign{'isoiec_9798_3_7_opt_1_sig_5', Ra, Rb, A, B, Text8}pkB++}++properties (of isoiec_9798_3_7_1)+ // Note that we do not get agreement on T!+ A_injective_agreement:+ iagree(A_5[A,B,Ra,Rb,Text8] -> B_5[A,B,Ra,Rb,Text8], {B, T})++ B_injective_agreement:+ iagree(B_4[A,B,Ra,Rb,Text6] -> A_4[A,B,Ra,Rb,Text6], {A, T})++ // We additionally verify agreement of A and B with the TTP T+ A_injective_agreement_T:+ iagree(A_3[B,T,Rpa,pkB,Text4] -> T_3[B,T,Rpa,pk(B),Text4], {T})+ B_injective_agreement_T:+ iagree(B_4[A,T,Rb,pkA,Text3] -> T_3[A,T,Rb,pk(A),Text3], {T})++++/****************************************************************************+ * Protocol 7 (Option 2)+ ****************************************************************************+ *+ * signature+ * ttp+ * five-pass+ * mutual+ *+ * B initiates and A communicates with T+ *+ * Modeling notes:+ * - Option 1 and Option 2 must not share tags!+ * - We model the case where T sends the public keys instead of just verifying+ * the certificates; i.e., 'ResA = (A, pk(A))' and 'ResB = (B, pk(B))'.+ * - Our model might perform a few equality checks more than what is strictly+ * required by the standard. All of them are practically feasible and we+ * advise to implement them. We do not verify whether we the security+ * properties also hold with fewer equality checks.+ */+protocol isoiec_9798_3_7_2+{+ text_1. -> B: Text1+ 1. B -> A: B, A, Rb, Text1++ text_2. -> A: Text2+ 2. A -> T: A, T, Rpa, Rb, A, B, Text2++ // Note: Text4 is not used in Option 2+ text_3. -> T: Text3, Text5+ 3. T -> : T, A, Text5, A, pk(A), B, pk(B),+ sign{ 'isoiec_9798_3_7_opt_2_sig_3',+ Rpa, Rb, A, pk(A), B, pk(B), Text3 }pk(T)+ -> A: T, A, Text5, A, pk(A), B, pkB,+ TokenTA++ // Here, A checks TokenTA. As we lack support for additionally checked+ // equalities, A sends a message to itself encrypted with a fresh nonce to+ // emulate the equality check.+ check_3_out. A -> : {'check_4',+ TokenTA+ }check_nonce_4+ check_3_in. -> A: {'check_4',+ sign{'isoiec_9798_3_7_opt_2_sig_3',+ Rpa, Rb, A, pkA, B, pkB, Text3 }pk(T)+ }check_nonce_4++ // Note: we additionally send T such that B knows which key to use for+ // checking TokenTA+ text_4. -> A: Text6, Text7+ 4. A -> : A, B, Rpa, Text7, T,+ TokenTA,+ sign{'isoiec_9798_3_7_opt_2_sig_4', Rb, Ra, B, A, Text6}pk(A)++ -> B: A, B, Rpa, Text9, T,+ sign{'isoiec_9798_3_7_opt_2_sig_3',+ Rpa, Rb, A, pkA, B, pkB, Text3 }pk(T),+ sign{'isoiec_9798_3_7_opt_2_sig_4', Rb, Ra, B, A, Text6}pkA++ text_5. -> B: Text8, Text9+ 5. B -> : A, B, Ra, Rb, Text9,+ sign{'isoiec_9798_3_7_opt_2_sig_5', Ra, Rb, A, B, Text8}pk(B)++ -> A: A, B, Ra, Rb, Text9,+ sign{'isoiec_9798_3_7_opt_2_sig_5', Ra, Rb, A, B, Text8}pkB++}++properties (of isoiec_9798_3_7_2)+ A_injective_agreement:+ iagree(A_5[A,B,Ra,Rb,Text8] -> B_5[A,B,Ra,Rb,Text8], {B, T})++ B_injective_agreement:+ iagree(B_4[A,B,Ra,Rb,Text6] -> A_4[A,B,Ra,Rb,Text6], {A, T})++ // We additionally verify agreement of A and B with the TTP T+ A_injective_agreement_T:+ iagree(A_4[A,B,T,Rpa,Rb,pkA ,pkB ,Text3] ->+ T_3[A,B,T,Rpa,Rb,pk(A),pk(B),Text3], {T})++ B_injective_agreement_T:+ iagree(B_4[A,B,T,Rpa,Rb,pkA ,pkB ,Text3] ->+ T_3[A,B,T,Rpa,Rb,pk(A),pk(B),Text3], {T})+++++// %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+// 4 - bdkey+// %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++/*+ * Modeled from ISO/IEC 9798-4+ * Modeler: Cas Cremers, Dec. 2010, Feb. 2011.+ * Ported to scyther-proof: Simon Meier, Feb. 2011.+ *+ * Modeling notes:+ * - Variant of ISO/IEC 9798-4 with bidirectional keys k[A,B].+ * - time-variant-parameters, time-stamps, and sequence numbers are+ * modeled by nonces leaked to the adversary at the start of a role.+ * - The TextX fields are chosen by the adversary.+ * - The keyed CCF (f_kab(x)) is modeled as h(('CCF', k[a,b]), x)+ *+ */+++/******************************************************************************+ * Protocol 1+ ******************************************************************************+ *+ * ccf+ * unilateral+ * one-pass+ */+protocol isoiec_9798_4_1_bdkey+{+ leak_A. A -> : TNA++ text_1. -> A: Text1, Text2+ 1. A -> B: A, B, TNA, Text2, Text1,+ h(('CCF', k[A,B]), ('isoiec_9798_4_1_ccf_1', TNA, B, Text1))+}++// Does not hold injectively.+properties (of isoiec_9798_4_1_bdkey)+ B_non_injective_agreement:+ niagree(B_1[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A, B})+++/******************************************************************************+ * Protocol 2+ ******************************************************************************+ *+ * ccf+ * unilateral+ * two-pass+ */+protocol isoiec_9798_4_2_bdkey+{+ text_1. -> B: Text1+ 1. B -> A: B, A, Rb, Text1++ text_2. -> A: Text2, Text3+ 2. A -> B: A, B, Text3, Rb, Text2,+ h(('CCF', k[A,B]), ('isoiec_9798_4_2_ccf_2', Rb, B, Text2))+}++properties (of isoiec_9798_4_2_bdkey)+ B_injective_agreement:+ iagree(B_2[A,B,Rb,Text2] -> A_2[A,B,Rb,Text2], {A, B})+++/******************************************************************************+ * Protocol 3+ ******************************************************************************+ *+ * ccf+ * mutual+ * two-pass+ */+protocol isoiec_9798_4_3_bdkey+{+ leak_A. A -> : TNa+ leak_B. B -> : TNb++ text_1. -> A: Text1, Text2+ 1. A -> B: A, B, TNa, Text2, Text1,+ h(('CCF', k[A,B]), ('isoiec_9798_4_3_ccf_1', TNa, B, Text1))++ text_2. -> B: Text3, Text4+ 2. B -> A: B, A, TNb, Text4, Text3,+ h(('CCF', k[A,B]), ('isoiec_9798_4_3_ccf_2', TNb, A, Text3))+}++// Does not hold injectively. Missing an opportunity to get injective+// agreement for role A by adding TNa in the second message.+properties (of isoiec_9798_4_3_bdkey)+ A_non_injective_agreement:+ niagree(A_2[A,B,TNb,Text3] -> B_2[A,B,TNb,Text3], {A, B})++ B_non_injective_agreement:+ niagree(B_1[A,B,TNa,Text1] -> A_1[A,B,TNa,Text1], {A, B})+++/******************************************************************************+ * Protocol 4+ ******************************************************************************+ *+ * ccf+ * mutual+ * three-pass+ */+protocol isoiec_9798_4_4_bdkey+{+ text_1. -> B: Text1+ 1. B -> A: B, A, Rb, Text1++ text_2. -> A: Text2, Text3+ 2. A -> B: A, B, Ra, Text3, Text2,+ h(('CCF', k[A,B]), ('isoiec_9798_4_4_ccf_2', Ra, Rb, B, Text2))++ text_3. -> B: Text4, Text5+ 3. B -> A: B, A, Text5, Text4,+ h(('CCF', k[A,B]), ('isoiec_9798_4_4_ccf_3', Rb, Ra, Text4))+}++properties (of isoiec_9798_4_4_bdkey)+ A_injective_agreement:+ iagree(A_3[A,B,Ra,Rb,Text2,Text4] -> B_3[A,B,Ra,Rb,Text2,Text4], {A, B})++ B_injective_agreement:+ iagree(B_2[A,B,Ra,Rb,Text2] -> A_2[A,B,Ra,Rb,Text2], {A, B})++++// %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+// 4 - udkey+// %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++/*+ * Modeled from ISO/IEC 9798-4+ * Modeler: Cas Cremers, Dec. 2010, Feb. 2011.+ * Ported to scyther-proof: Simon Meier, Feb. 2011.+ *+ * Modeling notes:+ * - Variant of ISO/IEC 9798-4 with unidirectional keys k(A,B) and+ * identities dropped if possible.+ * - time-variant-parameters, time-stamps, and sequence numbers are+ * modeled by nonces leaked to the adversary at the start of a role.+ * - The TextX fields are chosen by the adversary.+ * - The keyed CCF (f_kab(x)) is modeled as h(('CCF', k(a,b)), x)+ */+++/******************************************************************************+ * Protocol 1+ ******************************************************************************+ *+ * ccf+ * unilateral+ * one-pass+ */+protocol isoiec_9798_4_1_udkey+{+ leak_A. A -> : TNA++ text_1. -> A: Text1, Text2+ 1. A -> B: A, B, TNA, Text2, Text1,+ h(('CCF', k(A,B)), ('isoiec_9798_4_1_ccf_1', TNA, Text1))+}++// No injective agreement here, as the message from A can be received by+// multiple 'B's.+properties (of isoiec_9798_4_1_udkey)+ B_non_injective_agreement:+ niagree(B_1[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A, B})++++/******************************************************************************+ * Protocol 2+ ******************************************************************************+ *+ * ccf+ * unilateral+ * two-pass+ */+protocol isoiec_9798_4_2_udkey+{+ text_1. -> B: Text1+ 1. B -> A: B, A, Rb, Text1++ text_2. -> A: Text2, Text3+ 2. A -> B: A, B, Text3, Rb, Text2,+ h(('CCF', k(A,B)), ('isoiec_9798_4_2_ccf_2', Rb, Text2))+}++properties (of isoiec_9798_4_2_udkey)+ B_injective_agreement:+ iagree(B_2[A,B,Rb,Text2] -> A_2[A,B,Rb,Text2], {A, B})+++/******************************************************************************+ * Protocol 3+ ******************************************************************************+ *+ * ccf+ * mutual+ * two-pass+ */+protocol isoiec_9798_4_3_udkey+{+ leak_A. A -> : TNa+ leak_B. B -> : TNb++ text_1. -> A: Text1, Text2+ 1. A -> B: A, B, TNa, Text2, Text1,+ h(('CCF', k(A,B)), ('isoiec_9798_4_3_ccf_1', TNa, Text1))++ text_2. -> B: Text3, Text4+ 2. B -> A: B, A, TNb, Text4, Text3,+ h(('CCF', k(A,B)), ('isoiec_9798_4_3_ccf_2', TNb, Text3))+}++// The following properties do not hold injectively. This protocols misses a+// simple opportunity to get injective agreement for role A by adding TNa in+// the second message.+properties (of isoiec_9798_4_3_udkey)+ A_non_injective_agreement:+ niagree(A_2[A,B,TNb,Text3] -> B_2[A,B,TNb,Text3], {A, B})++ B_non_injective_agreement:+ niagree(B_1[A,B,TNa,Text1] -> A_1[A,B,TNa,Text1], {A, B})+++/******************************************************************************+ * Protocol 4+ ******************************************************************************+ *+ * ccf+ * mutual+ * three-pass+ */+protocol isoiec_9798_4_4_udkey+{+ text_1. -> B: Text1+ 1. B -> A: B, A, Rb, Text1++ text_2. -> A: Text2, Text3+ 2. A -> B: A, B, Ra, Text3, Text2,+ h(('CCF', k(A,B)), ('isoiec_9798_4_4_ccf_2', Ra, Rb, Text2))++ text_3. -> B: Text4, Text5+ 3. B -> A: B, A, Text5, Text4,+ h(('CCF', k(A,B)), ('isoiec_9798_4_4_ccf_3', Rb, Ra, Text4))+}++properties (of isoiec_9798_4_4_udkey)+ A_injective_agreement:+ iagree(A_3[A,B,Ra,Rb,Text2,Text4] -> B_3[A,B,Ra,Rb,Text2,Text4], {A, B})++ B_injective_agreement:+ iagree(B_2[A,B,Ra,Rb,Text2] -> A_2[A,B,Ra,Rb,Text2], {A, B})+++// %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+// The 2_5 and 2_6 protocols need manual type annotations to make the parallel+// composition proof go through. Therefore, we have to define+// %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+++/******************************************************************************+ * Protocol 5 (udkey and bdkey variants composed in parallel)+ ******************************************************************************+ *+ * symmetric+ * ttp+ * four-pass+ * mutual+ *+ * Modeling notes:+ * - The use of TNb in message 4, as specified by the ISO standard, is+ * different from other models, in which it was TNa.+ * - We send identity P in Step 3 in order for B to be able to lookup key k(B,P)+ */+protocol isoiec_9798_2_5+{++// original protocol: isoiec_9798_2_5_bdkey++ leakA. A -> : TVPa, TNa+ leakB. B -> : TNb+ leakP. P -> : TNp++ text1. -> A: Text1+ 1. A -> P: A, P, TVPa, B, Text1++ text2. -> P: Text2, Text3, Text4+ 2. P -> : P, A, Text4, { 'isoiec_9798_2_5_enc_2_1', TVPa, Kab, B, Text3 }k(A,P)+ , { 'isoiec_9798_2_5_enc_2_2', TNp , Kab, A, Text2 }k(B,P)+ -> A: P, A, Text4, { 'isoiec_9798_2_5_enc_2_1', TVPa, Kab, B, Text3 }k(A,P)+ , TokenPA_for_B++ text3. -> A: Text5, Text6+ 3. A -> : A, B, Text6, P, TokenPA_for_B+ , { 'isoiec_9798_2_5_enc_3', TNa, B, Text5 }Kab+ -> B: A, B, Text6, P, { 'isoiec_9798_2_5_enc_2_2', TNp, Kab, A, Text2 }k(B,P)+ , { 'isoiec_9798_2_5_enc_3', TNa, B, Text5 }Kab++ text4. -> B: Text7, Text8+ 4. B -> A: B, A, Text8, { 'isoiec_9798_2_5_enc_4', TNb, A, Text7 }Kab+++// original protocol: isoiec_9798_2_5_bdkey++ leakA. Abd -> : TVPa, TNa+ leakB. Bbd -> : TNb+ leakP. Pbd -> : TNp++ text1. -> Abd: Text1+ 1. Abd -> Pbd: Abd, Pbd, TVPa, Bbd, Text1++ text2. -> Pbd: Text2, Text3, Text4+ 2. Pbd -> : Pbd, Abd, Text4, { 'isoiec_9798_2_5_enc_2_1', TVPa, Kab, Abd, Bbd, Text3 }k[Abd,Pbd]+ , { 'isoiec_9798_2_5_enc_2_2', TNp , Kab, Abd, Bbd, Text2 }k[Bbd,Pbd]+ -> Abd: Pbd, Abd, Text4, { 'isoiec_9798_2_5_enc_2_1', TVPa, Kab, Abd, Bbd, Text3 }k[Abd,Pbd]+ , TokenPA_for_B++ text3. -> Abd: Text5, Text6+ 3. Abd -> : Abd, Bbd, Text6, Pbd, TokenPA_for_B+ , { 'isoiec_9798_2_5_enc_3', TNa, Bbd, Text5 }Kab+ -> Bbd: Abd, Bbd, Text6, Pbd, { 'isoiec_9798_2_5_enc_2_2', TNp, Kab, Abd, Bbd, Text2 }k[Bbd,Pbd]+ , { 'isoiec_9798_2_5_enc_3', TNa, Bbd, Text5 }Kab++ text4. -> Bbd: Text7, Text8+ 4. Bbd -> Abd: Bbd, Abd, Text8, { 'isoiec_9798_2_5_enc_4', TNb, Abd, Text7 }Kab++}++property (of isoiec_9798_2_5) typing_2_5:+ "Abd@Bbd :: Known(Bbd_3)+ Abd@Pbd :: Known(Pbd_1)+ A@B :: Known(B_3)+ A@P :: Known(P_1)+ Bbd@Pbd :: Known(Pbd_1)+ B@P :: Known(P_1)+ B@P :: Known(P_1)+ Kab@Abd :: (Known(Abd_2) | Kab@Pbd)+ Kab@Bbd :: (Known(Bbd_3) | Kab@Pbd)+ Kab@A :: (Known(A_2) | Kab@P)+ Kab@B :: (Known(B_3) | Kab@P)+ Pbd@Bbd :: Known(Bbd_3)+ P@B :: Known(B_3)++ // The following four lines are what is wrong in the automatically composed+ // type annotation.+ TNa@Bbd :: (Known(Bbd_3) | TNa@A | TNa@Abd)+ TNa@B :: (Known(B_3) | TNa@A | TNa@Abd)+ TNb@Abd :: (Known(Abd_4) | TNb@B | TNb@Bbd)+ TNb@A :: (Known(A_4) | TNb@B | TNb@Bbd)++ TNp@Bbd :: (Known(Bbd_3) | TNp@Pbd)+ TNp@B :: (Known(B_3) | TNp@P)+ TVPa@Pbd :: Known(Pbd_1)+ TVPa@P :: Known(P_1)+ Text1@Abd :: Known(Abd_text1)+ Text1@Pbd :: Known(Pbd_1)+ Text1@A :: Known(A_text1)+ Text1@P :: Known(P_1)+ Text2@Bbd :: Known(Bbd_3)+ Text2@Pbd :: Known(Pbd_text2)+ Text2@B :: Known(B_3)+ Text2@P :: Known(P_text2)+ Text3@Abd :: Known(Abd_2)+ Text3@Pbd :: Known(Pbd_text2)+ Text3@A :: Known(A_2)+ Text3@P :: Known(P_text2)+ Text4@Abd :: Known(Abd_2)+ Text4@Pbd :: Known(Pbd_text2)+ Text4@A :: Known(A_2)+ Text4@P :: Known(P_text2)+ Text5@Abd :: Known(Abd_text3)+ Text5@Bbd :: Known(Bbd_3)+ Text5@A :: Known(A_text3)+ Text5@B :: Known(B_3)+ Text6@Abd :: Known(Abd_text3)+ Text6@Bbd :: Known(Bbd_3)+ Text6@A :: Known(A_text3)+ Text6@B :: Known(B_3)+ Text7@Abd :: Known(Abd_4)+ Text7@Bbd :: Known(Bbd_text4)+ Text7@A :: Known(A_4)+ Text7@B :: Known(B_text4)+ Text8@Abd :: Known(Abd_4)+ Text8@Bbd :: Known(Bbd_text4)+ Text8@A :: Known(A_4)+ Text8@B :: Known(B_text4)+ TokenPA_for_B@Abd :: Known(Abd_2)+ TokenPA_for_B@A :: Known(A_2)"+++properties (of isoiec_9798_2_5) // udkey variant++ P_secret_Kab: secret(P, -, Kab, {A, B, P})+ A_secret_Kab: secret(A, 2, Kab, {A, B, P})+ B_secret_Kab: secret(B, 3, Kab, {A, B, P})++ // Agreement properties strengthened with respect to Cas Cremers' models:+ // (a) we also verify agreement on the freshness data TNa, TNb+ // (b) we also verify agreement with the trusted third party+ //+ A_injective_agreement_B:+ iagree(A_4[A,B,P,Kab,TNa,Text5,TNb,Text7] -> B_4[A,B,P,Kab,TNa,Text5,TNb,Text7], {A, B, P})++ // Injectivity agreement does not hold. See+ //+ // NO injective agreement can be proven. There may be several B-threads+ // communicating with the same A-thread! Checking the 'TNb' timestamp in+ // later steps could be used to remove this problem, up to the clock+ // resolution.+ B_non_injective_agreement_A:+ niagree(B_3[A,B,P,Kab,TNa,Text5] -> A_3[A,B,P,Kab,TNa,Text5], {A, B, P})++ A_injective_agreement_P:+ iagree(A_2[A,B,P,Kab,TVPa,Text3] -> P_2[A,B,P,Kab,TVPa,Text3], {A, B, P})++ // No injective agreement, as the TTP does not receive any message from 'B'.+ B_non_injective_agreement_P:+ niagree(B_3[A,B,P,Kab,TNp,Text2] -> P_2[A,B,P,Kab,TNp,Text2], {A, B, P})+++properties (of isoiec_9798_2_5) // bdkey variant++ Pbd_secret_Kab: secret(Pbd, -, Kab, {Abd, Bbd, Pbd})+ Abd_secret_Kab: secret(Abd, 2, Kab, {Abd, Bbd, Pbd})+ Bbd_secret_Kab: secret(Bbd, 3, Kab, {Abd, Bbd, Pbd})++ // Agreement properties strengthened with respect to Cas Cremers' models:+ // (a) we also verify agreement on the freshness data TNa, TNb+ // (b) we also verify agreement with the trusted third party+ //+ Abd_injective_agreement_Bbd:+ iagree(Abd_4[Abd,Bbd,Pbd,Kab,TNa,Text5,TNb,Text7]+ -> Bbd_4[Abd,Bbd,Pbd,Kab,TNa,Text5,TNb,Text7], {Abd, Bbd, Pbd})++ // Injective agreement does not hold. See+ // isoiec_9798_2_5_special_TTP_bdkey for more information.+ Bbd_non_injective_agreement_Abd:+ niagree(Bbd_3[Abd,Bbd,Pbd,Kab,TNa,Text5]+ -> Abd_3[Abd,Bbd,Pbd,Kab,TNa,Text5], {Abd, Bbd, Pbd})++ Abd_injective_agreement_Pbd:+ iagree(Abd_2[Abd,Bbd,Pbd,Kab,TVPa,Text3]+ -> Pbd_2[Abd,Bbd,Pbd,Kab,TVPa,Text3], {Abd, Bbd, Pbd})++ // Injective agreement does not hold. See+ // isoiec_9798_2_5_special_TTP_bdkey for more information.+ Bbd_non_injective_agreement_Pbd:+ niagree(Bbd_3[Abd,Bbd,Pbd,Kab,TNp,Text2]+ -> Pbd_2[Abd,Bbd,Pbd,Kab,TNp,Text2], {Abd, Bbd, Pbd})++*/++/******************************************************************************+ * Protocol 6+ ******************************************************************************+ *+ * symmetric+ * ttp+ * five-pass+ * mutual+ *+ * Modeling notes:+ * - We send identity P in Step 4 in order for B to be able to lookup key k(B,P)+ *+ * MPA Attack reported by Mathuria:+ * - Type flaw MPA when in parallel with Abadi-Needham protocol.+ */+protocol isoiec_9798_2_6+{++// original protocol: isoiec_9798_2_6_udkey++ text1. -> B: Text1+ 1. B -> A: B, A, Rb, Text1++ text2. -> A: Text2+ 2. A -> P: A, P, Ra, Rb, B, Text2++ text3. -> P: Text3, Text4, Text5+ 3. P -> : P, A, Text5, {'isoiec_9798_2_6_enc_3_1', Ra, Kab, B, Text4}k(A,P)+ , {'isoiec_9798_2_6_enc_3_2', Rb, Kab, A, Text3}k(B,P)+ -> A: P, A, Text5, {'isoiec_9798_2_6_enc_3_1', Ra, Kab, B, Text4}k(A,P)+ , TokenPA_for_B++ text4. -> A: Text6, Text7+ 4. A -> : A, B, Text7, P, TokenPA_for_B+ , {'isoiec_9798_2_6_enc_4', Rpa, Rb, Text6}Kab+ -> B: A, B, Text7, P, {'isoiec_9798_2_6_enc_3_2', Rb, Kab, A, Text3}k(B,P)+ , {'isoiec_9798_2_6_enc_4', Rpa, Rb, Text6}Kab++ text5. -> B: Text8, Text9+ 5. B -> A: B, A, Text9, {'isoiec_9798_2_6_enc_5', Rb, Rpa, Text8}Kab+++//original protocol isoiec_9798_2_6_bdkey++ text1. -> Bbd: Text1+ 1. Bbd -> Abd: Bbd, Abd, Rb, Text1++ text2. -> Abd: Text2+ 2. Abd -> Pbd: Abd, Pbd, Ra, Rb, Bbd, Text2++ text3. -> Pbd: Text3, Text4, Text5+ 3. Pbd -> : Pbd, Abd, Text5, {'isoiec_9798_2_6_enc_3_1', Ra, Kab, Abd, Bbd, Text4}k[Abd,Pbd]+ , {'isoiec_9798_2_6_enc_3_2', Rb, Kab, Abd, Bbd, Text3}k[Bbd,Pbd]+ -> Abd: Pbd, Abd, Text5, {'isoiec_9798_2_6_enc_3_1', Ra, Kab, Abd, Bbd, Text4}k[Abd,Pbd]+ , TokenPA_for_B++ text4. -> Abd: Text6, Text7+ 4. Abd -> : Abd, Bbd, Text7, Pbd, TokenPA_for_B+ , {'isoiec_9798_2_6_enc_4', Rpa, Rb, Text6}Kab+ -> Bbd: Abd, Bbd, Text7, Pbd, {'isoiec_9798_2_6_enc_3_2', Rb, Kab, Abd, Bbd, Text3}k[Bbd,Pbd]+ , {'isoiec_9798_2_6_enc_4', Rpa, Rb, Text6}Kab++ text5. -> Bbd: Text8, Text9+ 5. Bbd -> Abd: Bbd, Abd, Text9, {'isoiec_9798_2_6_enc_5', Rb, Rpa, Text8}Kab+}+++property (of isoiec_9798_2_6) typing_2_6:+ "Abd@Pbd :: Known(Pbd_2)+ A@P :: Known(P_2)+ Bbd@Abd :: Known(Abd_1)+ Bbd@Pbd :: Known(Pbd_2)+ B@A :: Known(A_1)+ B@P :: Known(P_2)+ Kab@Abd :: (Known(Abd_3) | Kab@Pbd)+ Kab@Bbd :: (Known(Bbd_4) | Kab@Pbd)+ Kab@A :: (Known(A_3) | Kab@P)+ Kab@B :: (Known(B_4) | Kab@P)+ Pbd@Bbd :: Known(Bbd_4)+ P@B :: Known(B_4)+ Ra@Pbd :: Known(Pbd_2)+ Ra@P :: Known(P_2)+ Rb@Abd :: Known(Abd_1)+ Rb@Pbd :: Known(Pbd_2)+ Rb@A :: Known(A_1)+ Rb@P :: Known(P_2)++ // The following two lines are different from the automatically computed+ // type invariant for the composed protocols.+ Rpa@Bbd :: (Known(Bbd_4) | Rpa@A | Rpa@Abd)+ Rpa@B :: (Known(B_4) | Rpa@A | Rpa@Abd)++ Text1@Abd :: Known(Abd_1)+ Text1@Bbd :: Known(Bbd_text1)+ Text1@A :: Known(A_1)+ Text1@B :: Known(B_text1)+ Text2@Abd :: Known(Abd_text2)+ Text2@Pbd :: Known(Pbd_2)+ Text2@A :: Known(A_text2)+ Text2@P :: Known(P_2)+ Text3@Bbd :: Known(Bbd_4)+ Text3@Pbd :: Known(Pbd_text3)+ Text3@B :: Known(B_4)+ Text3@P :: Known(P_text3)+ Text4@Abd :: Known(Abd_3)+ Text4@Pbd :: Known(Pbd_text3)+ Text4@A :: Known(A_3)+ Text4@P :: Known(P_text3)+ Text5@Abd :: Known(Abd_3)+ Text5@Pbd :: Known(Pbd_text3)+ Text5@A :: Known(A_3)+ Text5@P :: Known(P_text3)+ Text6@Abd :: Known(Abd_text4)+ Text6@Bbd :: Known(Bbd_4)+ Text6@A :: Known(A_text4)+ Text6@B :: Known(B_4)+ Text7@Abd :: Known(Abd_text4)+ Text7@Bbd :: Known(Bbd_4)+ Text7@A :: Known(A_text4)+ Text7@B :: Known(B_4)+ Text8@Abd :: Known(Abd_5)+ Text8@Bbd :: Known(Bbd_text5)+ Text8@A :: Known(A_5)+ Text8@B :: Known(B_text5)+ Text9@Abd :: Known(Abd_5)+ Text9@Bbd :: Known(Bbd_text5)+ Text9@A :: Known(A_5)+ Text9@B :: Known(B_text5)+ TokenPA_for_B@Abd :: Known(Abd_3)+ TokenPA_for_B@A :: Known(A_3)"+++/*+properties (of isoiec_9798_2_6) //udkey variant++ P_secret_Kab: secret(P, -, Kab, {A, B, P})+ A_secret_Kab: secret(A, 3, Kab, {A, B, P})+ B_secret_Kab: secret(B, 4, Kab, {A, B, P})++ // Agreement properties strengthened with respect to Cas Cremers' models:+ // (a) we also verify agreement on the freshness data+ // (b) we also verify agreement with the trusted third party+ //+ A_injective_agreement_B:+ iagree(A_5[A,B,P,Kab,Rpa,Rb,Text6,Text8] -> B_5[A,B,P,Kab,Rpa,Rb,Text6,Text8], {A, B, P})++ B_injective_agreement_A:+ iagree(B_4[A,B,P,Kab,Rpa,Rb,Text6] -> A_4[A,B,P,Kab,Rpa,Rb,Text6], {A, B, P})++ A_injective_agreement_P:+ iagree(A_3[A,B,P,Ra,Kab,Text4] -> P_3[A,B,P,Ra,Kab,Text4], {A, B, P})++ B_injective_agreement_P:+ iagree(B_4[A,B,P,Rb,Kab,Text3] -> P_3[A,B,P,Rb,Kab,Text3], {A, B, P})+++properties (of isoiec_9798_2_6) //bdkey variant++ Pbd_secret_Kab: secret(Pbd, -, Kab, {Abd, Bbd, Pbd})+ Abd_secret_Kab: secret(Abd, 3, Kab, {Abd, Bbd, Pbd})+ Bbd_secret_Kab: secret(Bbd, 4, Kab, {Abd, Bbd, Pbd})++ // Agreement properties strengthened with respect to Cas Cremers' models:+ // (a) we also verify agreement on the freshness data+ // (b) we also verify agreement with the trusted third party+ //+ Abd_injective_agreement_Bbd:+ iagree(Abd_5[Abd,Bbd,Pbd,Kab,Rpa,Rb,Text6,Text8]+ -> Bbd_5[Abd,Bbd,Pbd,Kab,Rpa,Rb,Text6,Text8], {Abd, Bbd, Pbd})++ Bbd_injective_agreement_Abd:+ iagree(Bbd_4[Abd,Bbd,Pbd,Kab,Rpa,Rb,Text6]+ -> Abd_4[Abd,Bbd,Pbd,Kab,Rpa,Rb,Text6], {Abd, Bbd, Pbd})++ Abd_injective_agreement_Pbd:+ iagree(Abd_3[Abd,Bbd,Pbd,Ra,Kab,Text4]+ -> Pbd_3[Abd,Bbd,Pbd,Ra,Kab,Text4], {Abd, Bbd, Pbd})++ Bbd_injective_agreement_Pbd:+ iagree(Bbd_4[Abd,Bbd,Pbd,Rb,Kab,Text3]+ -> Pbd_3[Abd,Bbd,Pbd,Rb,Kab,Text3], {Abd, Bbd, Pbd})+*/++end
data/isabelle/README view
@@ -3,7 +3,7 @@ Authors: Simon Meier <iridcode@gmail.com> Creation Date: 2011-05-13-Last Updated: 2013-02-27 by Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>+Last Updated: 2014-01-31 by Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch> 1. Introduction ===============@@ -55,10 +55,10 @@ 2.2 Installing the Isabelle/HOL theories ---------------------------------------- -Download and install full Isabelle2013 according to the installation+Download and install full Isabelle2013-2 according to the installation instructions at - http://isabelle.in.tum.de/website-Isabelle2013/download_x86-linux.html+ http://isabelle.in.tum.de/website-Isabelle2013-2/ The first time you call `scyther-proof` with the `--isabelle` flag it will build the logic image of the Isabelle/HOL theories formalizing the security@@ -178,6 +178,6 @@ `Happy Proving :)` -In case of questions do not hesistate to contact Simon Meier at-iridcode@gmail.com.+In case of questions do not hesistate to contact Andreas Lochbihler+(andreas.lochbihler@inf.ethz.ch) or Simon Meier (iridcode@gmail.com).
data/isabelle/src/ESPLogic/Hints.thy view
@@ -40,15 +40,12 @@ sig val dest_hint: term -> string * term val mk_hint: string -> term -> term- val mk_hint_thm: theory -> string -> term -> thm+ val mk_hint_thm: Proof.context -> string -> term -> thm val gather: (string * term -> bool) -> term list -> (string * term) list val gather_by_name: string -> term list -> term list- val remove_all_hints_tac: int -> tactic+ val remove_all_hints_tac: Proof.context -> int -> tactic end;-*} -ML{*- structure Hints: HINTS = struct @@ -65,7 +62,7 @@ fun gather_by_name name = map snd o gather (equal name o fst) (* A tactic removing all hints in the given subgoal *)-val remove_all_hints_tac = full_simp_tac (HOL_ss addsimps @{thms remove_hints})+fun remove_all_hints_tac ctxt = full_simp_tac (put_simpset HOL_ss ctxt addsimps @{thms remove_hints}) (* create a hint term *) fun mk_hint name t =@@ -77,12 +74,12 @@ end; (* create a hint theorem *)-fun mk_hint_thm thy name t =+fun mk_hint_thm ctxt name t = let val hint_ct = mk_hint name t |> HOLogic.mk_Trueprop- |> Thm.cterm_of thy;+ |> Thm.cterm_of (Proof_Context.theory_of ctxt); in- Goal.prove_internal [] hint_ct (K (ALLGOALS remove_all_hints_tac))+ Goal.prove_internal [] hint_ct (K (ALLGOALS (remove_all_hints_tac ctxt))) end; end;
data/isabelle/src/ESPLogic/Unify.thy view
@@ -183,10 +183,10 @@ (* Tries to derive 'False' from equality of sizes of equated terms. *)-fun inequal_sizes ss eq_th =+fun inequal_sizes ctxt eq_th = let val opt_size_eq = - SOME (simplify ss (eq_th RS @{thm eq_imp_size_eq}))+ SOME (simplify ctxt (eq_th RS @{thm eq_imp_size_eq})) handle THM _ => NONE in case opt_size_eq of@@ -204,7 +204,7 @@ let (* TODO: Remove hack by using Named_Thms data functor. *) val thm_by_name = Proof_Context.get_thm ctxt;- val ss = simpset_of ctxt + val ss = ctxt delsimps map thm_by_name ["tid_eq_commute", "reorient_store_eq_store"]; (* substitute an equality theorem in the given list of 'done' and
data/isabelle/src/ESPLogic/WeakTyping.thy view
@@ -713,7 +713,19 @@ m \<notin> knows t" by(auto simp: KnownT_def) +lemma in_SumT_NonceT_NonceTE [elim!]:+ "\<lbrakk> m \<in> SumT (NonceT Ro n) (NonceT Ro' n') i q; + m \<in> NonceT Ro n i q \<Longrightarrow> R; + m \<in> NonceT Ro' n' i q \<Longrightarrow> R + \<rbrakk> \<Longrightarrow> R"+ by(auto simp: SumT_def) +(* TODO: Add more of the restricted SumT unfoldings analogous to the ones above.+ We don't unfold SumT eagerly, as this would result in too many branches being created.+ The above lemma is a hack to get triple types of the form SumT KnownT (SumT NonceT NonceT)+ to work. The proper way would be to only expand types of variables that are being analyzed+ by the decrChain function.+*) text{* Direct unfoldings *}
data/isabelle/src/ESPLogic/espl_definitions.ML view
@@ -174,8 +174,8 @@ let val ((msg_const,msg_def),(step_const,step_def)) = ann_defs; - val ss_step = Simplifier.simpset_of lthy addsimps [step_def];- val ss_full = ss_step addsimps [msg_def];+ val ss_step = lthy addsimps [step_def] |> simpset_of;+ val ss_full = lthy addsimps [step_def, msg_def] |> simpset_of; val sendStep_t = @{const sendStep} $ step_const; val noteStep_t = @{const noteStep} $ step_const;@@ -258,15 +258,16 @@ val step_defs = map (snd o snd) steps; val step_consts = map (fst o snd) steps; - val ss_role = Simplifier.simpset_of ctxt addsimps - [role_def, @{thm prefixClose_def}];- val ss_full = ss_role addsimps (pat_defs @ step_defs @- @{thms wf_role_def distinct_list_def wf_role_axioms_def});+ val ss_role = ctxt addsimps [role_def, @{thm prefixClose_def}] |> simpset_of;+ val ss_full = ctxt addsimps ([role_def, @{thm prefixClose_def}] @ pat_defs @ step_defs @+ @{thms wf_role_def distinct_list_def wf_role_axioms_def}) |> simpset_of - val simp_tactic = K (FIRSTGOAL (Simplifier.full_simp_tac ss_full));+ fun simp_tactic {prems, context} = FIRSTGOAL (Simplifier.full_simp_tac (put_simpset ss_full context)); val distinct_steps_thms = prove_distinctness ctxt simp_tactic step_consts; + val ss_prefixClose = ctxt addsimps ([role_def, @{thm prefixClose_def}] @ distinct_steps_thms) |> simpset_of;+ val wf_goal = HOLogic.mk_Trueprop (@{const wf_role} $ role_const); val avars_t = @{const aVars}$ role_const;@@ -274,15 +275,13 @@ val lastComStep_t = @{const lastComStep} $ role_const; val firstComStep_t = @{const firstComStep} $ role_const; - val ss_prefixClose = ss_role addsimps distinct_steps_thms;-- fun mk_prefixClose_thm step_def =+ fun mk_prefixClose_thm ctxt step_def = let val step = step_def |> Thm.prop_of |> dest_HOL_def |> #1; val t = @{const prefixClose} $ (Free ("s", @{typ store})) $ (Free ("t", @{typ explicit_trace})) $ role_const $ step $ (Free ("i", @{typ tid}));- in expand_term ss_prefixClose t end+ in expand_term ss_prefixClose ctxt t end fun pat_def_msgvars pat_def = pat_def |> Thm.prop_of |> dest_HOL_def |> #2 |> pat_msgvars;@@ -299,11 +298,11 @@ |> #2 o notes_proven simp_tactic [ (mk_binding "wf_role", [([wf_goal],[att_iff_add])]) ] (* distinct steps and prefixClose expansions *)- |> #2 o Local_Theory.notes+ |> #2 o (fn ctxt => Local_Theory.notes [ (mk_binding "distinct_steps", [(distinct_steps_thms,[att_iff_add])]) , (mk_binding "prefixClose_convs", - [(map mk_prefixClose_thm step_defs, [att_iff_add])])- ]+ [(map (mk_prefixClose_thm ctxt) step_defs, [att_iff_add])])+ ] ctxt) (* expansions *) |> notes_expansion ss_role [ (mk_binding "in_set_conv", [([in_set_t],[att_iff_add])])@@ -364,8 +363,7 @@ |> dest_HOL_def |> #2 |> HOLogic.dest_set; val role_unfolds = flat (map (get_unfold_thms ctxt) role_consts); - val proto_ss = Simplifier.simpset_of ctxt addsimps - (proto_def :: @{thms wf_proto_def});+ val proto_ss = ctxt addsimps (proto_def :: @{thms wf_proto_def}); val full_ss = proto_ss addsimps role_unfolds; fun simp_tactic ss = K (FIRSTGOAL (Simplifier.full_simp_tac ss));@@ -387,7 +385,7 @@ , (mk_binding "wf_proto", [([wf_proto_thm], [att_iff_add])]) ] (* expansions *) - |> #2 o notes_expansion proto_ss+ |> #2 o notes_expansion (proto_ss |> simpset_of) [ (mk_binding "in_set_conv", [([in_set_t],[att_iff_add])]) ] (* restore annotated definition *)@@ -545,13 +543,12 @@ (* Insert the case names into a theorem *) fun insert_case_names ctxt th = let- val thy = Proof_Context.theory_of ctxt; val cases = source_case_names th;- val case_hint = Hints.mk_hint_thm thy "case_name" o HOLogic.mk_string o nth cases;+ val case_hint = Hints.mk_hint_thm ctxt "case_name" o HOLogic.mk_string o nth cases; fun ins_tac (_,i) = Method.insert_tac [case_hint (i-1)] i; in HOL_Ext.refine_rule ctxt - (K (ALLGOALS (Hints.remove_all_hints_tac THEN' SUBGOAL ins_tac))) th+ (K (ALLGOALS (Hints.remove_all_hints_tac ctxt THEN' SUBGOAL ins_tac))) th end @@ -627,7 +624,7 @@ EVERY' [ etac ty_elim_th , assume_tac- , TRY o full_simp_tac (simpset_of ctxt)+ , TRY o full_simp_tac ctxt , TRY o (REPEAT o etac @{thm conjE}) , TRY o Orders.order_tac ctxt [] ]@@ -640,7 +637,7 @@ fun expand_knows_cases_tac ctxt ty_elim_ths = REPEAT_DETERM1 ( FIRST [ safe_tac ctxt- , CHANGED_PROP (TRYALL (full_simp_tac (simpset_of ctxt)))+ , CHANGED_PROP (TRYALL (full_simp_tac ctxt)) , CHANGED_PROP (TRYALL (type_elim_tac ctxt ty_elim_ths)) ] );@@ -753,9 +750,8 @@ let val (typ_const,typ_def) = ann_def; - val autom_tac = auto_tac (map_simpset (fn ss => ss addsimps [typ_def]) ctxt)- val ss_full = Simplifier.simpset_of ctxt - addsimps [typ_def] addsimps @{thms mk_typing_def};+ val autom_tac = auto_tac (ctxt addsimps [typ_def])+ val ss_full = ctxt addsimps [typ_def] addsimps @{thms mk_typing_def} |> simpset_of; val vars = typ_def |> Thm.prop_of |> ESPL_Utils.dest_HOL_def |> snd |> dest_mk_typing |> map fst;
data/isabelle/src/ESPLogic/espl_methods.ML view
@@ -47,7 +47,7 @@ fun err_no_matching_rule ctxt raw_rules knows_thm = error (Pretty.string_of (Pretty.block (Pretty.fbreaks [ Pretty.str "none of the rules:"- , Pretty.indent 2 (Display.pretty_thms ctxt raw_rules)+ , Pretty.indent 2 (Proof_Context.pretty_fact ctxt ("", raw_rules)) , Pretty.str "resolved against:" , Pretty.indent 2 (Display.pretty_thm ctxt knows_thm) ])))@@ -65,7 +65,7 @@ val facts' = filter (not o is_hint_thm) facts; val final_tac = ALLGOALS ( (if minimal then - TRY o Simplifier.full_simp_tac (simpset_of ctxt)+ TRY o Simplifier.full_simp_tac ctxt else TRY o Method.insert_tac facts' THEN' TRY o (@@ -88,7 +88,6 @@ let val thy = Proof_Context.theory_of ctxt; val cert = Thm.cterm_of thy;- val ss = simpset_of ctxt; val raw_rules = case opt_raw_rule of SOME th => [th]@@ -115,7 +114,7 @@ (ALLGOALS (assume_tac ORELSE' eresolve_tac predOrd_elim_ths) ORELSE auto_tac (ctxt addIs predOrd_elim_ths)) )- |> simplify ss+ |> simplify ctxt val (cases, rule) = case get_first (try (curry (op RS) knows_thm)) raw_rules of@@ -183,7 +182,7 @@ let val prefixClose_th = Proof_Context.get_thm ctxt "ext_prefixClose"; fun close step roleMap = [step, roleMap] MRS prefixClose_th;- val expand = Simplifier.simplify (Simplifier.simpset_of ctxt);+ val expand = Simplifier.simplify ctxt; val distinct_prop = distinct (Thm.eq_thm); (* fun new_fact th = forall (not_equal (Thm.prop_of th) o Thm.prop_of) facts; *)@@ -266,9 +265,7 @@ *) fun completeness_cases_attrib ctxt th = let- val cs = Classical.get_cs ctxt;- val ss = (Context.cases Simplifier.global_simpset_of Simplifier.simpset_of ctxt)- addsimps @{thms finite_setdiff_compute};+ val ss = Context.proof_of ctxt addsimps @{thms finite_setdiff_compute}; fun add_case_info th = th |> Rule_Cases.add_consumes 0 |> Rule_Cases.name (completeness_case_names th)
data/isabelle/src/ESPLogic/espl_utils.ML view
@@ -19,15 +19,15 @@ (* Pure specific functions *) val local_standard': thm -> thm- val expand_term: simpset -> term -> thm- val thms_to_simpset: Proof.context -> thm list -> simpset+ val expand_term: simpset -> Proof.context -> term -> thm+ val thms_to_simpset: Proof.context -> thm list -> Proof.context val prove_prop : Proof.context -> ({prems: thm list, context: Proof.context} -> tactic) -> term -> thm val notes_expansion : simpset -> (Attrib.binding * (term list * Args.src list) list) list -> local_theory -> (string * thm list) list * local_theory val note_expansion- : simpset -> Attrib.binding * term list -> + : simpset -> Attrib.binding * term list -> local_theory -> (string * thm list) * local_theory val notes_proven : ({prems: thm list, context: Proof.context} -> tactic) ->@@ -114,9 +114,9 @@ (* Generate the theorem proving the expansion of a term wrto to the given simpset and convert it into a rule. *)-fun expand_term ss t = t- |> Thm.cterm_of (Proof_Context.theory_of (Raw_Simplifier.the_context ss))- |> Simplifier.rewrite ss+fun expand_term ss ctxt t = t+ |> Thm.cterm_of (Proof_Context.theory_of ctxt)+ |> Simplifier.rewrite (put_simpset ss ctxt) |> (fn conv => conv RS @{thm meta_eq_to_obj_eq}) |> local_standard' @@ -124,15 +124,14 @@ fun prove_prop ctxt mk_tactic goal = Goal.prove ctxt [] [] goal mk_tactic; (* create a simpset consisting only of the given theorems in the given context *)-fun thms_to_simpset ctxt ths = - Simplifier.context ctxt (Raw_Simplifier.empty_ss addsimps ths);+fun thms_to_simpset ctxt ths = empty_simpset ctxt addsimps ths; (* Expand a list of terms and note the resulting theorems. *)-fun notes_expansion ss to_expand = - Local_Theory.notes (map (apsnd (map (apfst (map (expand_term ss))))) to_expand);+fun notes_expansion ss to_expand lthy =+ Local_Theory.notes (map (apsnd (map (apfst (map (expand_term ss lthy))))) to_expand) lthy; (* Expand a term and note the resulting theorem. *)-fun note_expansion ss (a, ts) = +fun note_expansion ss (a, ts) = notes_expansion ss [(a, [(ts, [])])] #>> the_single; (* Prove a list of propositions and note the resulting theorems *)
− data/isabelle/src/Tutorial.thy
@@ -1,295 +0,0 @@-theory Tutorial-imports- ESPLogic-begin--chapter{* A Short Tutorial on the Theories *}--text{*- Here, we explain the differences to the presentation given in- the submitted paper. Furthermore, we illustrate the usage of- the Isabelle theories on the running example of the paper.-- There are two syntaxes for specifying patterns and - messages. For one there is the syntax given by their construction- as algebraic datatypes. This syntax is used for specifying and- proving inference rules and all the other infrastructure. Then,- in the theory Syntax, we define an alternative syntax which- is used for the definition of actual protocols and their proofs.- We introduce this additional syntax because otherwise to shorten- the representation of patterns and messages.- - The following example pattern represents the first- message of the client role of the CR protocol in the paper.-*}--definition somePt :: pattern-where "somePt = PEnc (PFresh ''n'') (PAsymPK (PVar (AVar ''s'')))"--text{*- The atomic sets $\textit{Const}$, $\textit{Fresh}$, and $\textit{Var}$ - from the paper, are represented explicitely using the constructors- @{const PConst}, @{const PFresh}, @{const PVar}. The injection of -*}---lemma inst_example: - "inst \<sigma> i somePt = Some (Enc (LN ''n'' i) (PK (\<sigma>(AV ''s'' i))))"- unfolding somePt_def by simp--text{*- Roles and protocols are modeled according to the types- given in the paper. However, the assumptions about- duplicate-freeness and no sending of message variables- before receiving them is handled using the following- two locales.-*}--print_locale wf_role-print_locale wf_proto--text{*- Roles are defined using the custom ``role'' command.-- \begin{quote}\bf- If this command doesn't work for you (outer syntax error),- then you forgot to replace the ``isar-keywords.el'' file.- Check the README file for instructions.- \end{quote}-- The benefit of these commands is that they prove a number- of simple theorems which are later used for automation. Typical- things include distinctness of role steps in a role and no- sending of non-received message variables. -- Here, the running example from the paper. (Due to a name-clash- with existing constants, we call the $C$ role client and - the $S$ role server.-*}--role client-where "client =- [ Send ''1'' (PEnc (sLN ''k'') (sPK ''s''))- , Recv ''2'' (PHash (sLN ''k''))- ]"--thm client.unfold-thm client_1.sendStep_conv--role server-where "server =- [ Recv ''1'' (PEnc (sLMV ''v'') (sPK ''s''))- , Send ''2'' (PHash (sLMV ''v''))- ]"--protocol CR-where "CR = {client,server}"--text{* - The role command also defines constants representing- the individual role steps and their patterns. - They are labelled according- to the label. Hence, labels must be distinct for these- constants to be definable. For example @{const client_1} is- the first role step of the @{const client} role. @{const client_1_pt} - is the pattern of this role step.-- The protocol definition command also introduces a locale CR\_state- that provides a convenient way for proving theorems under- the assumption that @{term "(t,r,s)"} is a reachable state.- The construction is based on the- function @{const reachable} (cf. ExecutionModel.thy).- Most theorems are derived under the assumption that- we are reasoning about a reachable state of some - protocol $P$. In Isabelle, we model this using the- following locale.-*}--print_locale reachable_state--text{* We adapt notation a bit more to the paper.*}--abbreviation (in reachable_state) "th \<equiv> r"-abbreviation (in reachable_state) "tr \<equiv> t"-abbreviation (in reachable_state) "\<sigma> \<equiv> s"-abbreviation (in reachable_state) "role \<equiv> roleMap"--text{*- Note that the naming convention is a bit different from- the paper. The default reachable state is $(t,r,s)$ which- corresponds to the reachable state $(tr,th,\<sigma>)$ in the- paper.-- The functions @{const knows} and @{const steps} are defined- as in the paper. The event order relation is modelled by- the function @{const predOrd}. In the locale - reachable\_state it is abbreviated as $\prec$. The- inference rules are derived in the theory InferenceRules.- As an example, we show the chain rule.-*}--lemma (in reachable_state) chain_rule:- assumes known: "m' \<in> knows t"- shows- "(m' \<in> IK0) \<or>- (\<exists> m. m' = Hash m \<and> Ln m \<prec> Ln (Hash m)) \<or>- (\<exists> m k. m' = Enc m k \<and> Ln m \<prec> Ln (Enc m k) \<and> Ln k \<prec> Ln (Enc m k)) \<or>- (\<exists> x y. m' = Tup x y \<and> Ln x \<prec> Ln (Tup x y) \<and> Ln y \<prec> Ln (Tup x y)) \<or>- (\<exists> i done todo skipped. r i = Some (done, todo, skipped) \<and> - (\<exists> l pt m. - Send l pt \<in> set done \<and> Some m = inst s i pt \<and> - decrChain [] t {St (i, Send l pt)} m m'- )- ) \<or>- (\<exists> i done todo skipped. r i = Some (done, todo, skipped) \<and> - (\<exists> l ty pt m. - Note l ty pt \<in> set done \<and> Note l ty pt \<notin> skipped \<and> - Some m = inst s i pt \<and> - decrChain [] t {St (i, Note l ty pt)} m m'- )- ) \<or>- (\<exists> a. m' = SK a \<and> LKR a \<prec> Ln m') \<or>- (\<exists> a b. m' = K a b \<and> LKR a \<prec> Ln m') \<or>- (\<exists> a b. m' = K a b \<and> LKR b \<prec> Ln m') \<or> - (\<exists> A. \<exists> a \<in> A. m' = KShr A \<and> LKR (Lit (EAgent a)) \<prec> Ln m')- "- using known by (rule knows_cases_raw)--text{*- Note that learn events have to be represented explicitely.- We are using the constructors @{const St} for step events- and @{const Ln} for learn events. Basic learn events are- marked with @{const Step} and @{const Learns}. The confusion- with respect to the paper version comes from the desire- to have short names.-*}--text{* - Weak atomicity is a special type invariant defined- in the WeakTyping theory. We prove that every reachable state- of the @{const CR} is also weakly atomic by specifying - the following type invariant.-*}---type_invariant atomic_CR for CR-where "atomic_CR = weakly_atomic"--(* declare (in CR_state) event_predOrdI[intro] *)--sublocale CR_state \<subseteq> atomic_CR_state-proof -- have "(tr, th, \<sigma>) \<in> approx weakly_atomic"- proof(cases rule: reachable_in_approxI_ext- [OF monoTyp_weakly_atomic, completeness_cases_rule])- case (server_1_v tr th \<sigma> tid)- then interpret state: atomic_CR_state tr th \<sigma>- by unfold_locales auto- show ?case using server_1_v- by (sources "Enc (\<sigma> (MV ''v'' tid)) (PK (\<sigma> (AV ''s'' tid)))") - (auto intro: event_predOrdI)- qed- thus "atomic_CR_state tr th \<sigma>" by unfold_locales simp-qed--text{*- We can now use the "sources" method to prove security- properties for reachable states of the @{const CR} protocol.-*}--lemma (in CR_state) nonce_after_lkr:- assumes asms: - "role th i = Some client"- "LN ''k'' i \<in> knows tr"- shows "LKR (\<sigma>(AV ''s'' i)) \<prec> Ln (LN ''k'' i)" (is "?lkrbef")-using asms-proof(sources "LN ''k'' i")- case client_1_k- thus "?thesis" by(sources "SK (\<sigma> (AV ''s'' i))") auto-thm noteStep_def-qed--lemma (in CR_state) client_k_secrecy:- assumes asms:- "role th i = Some client"- "RLKR (\<sigma>(AV ''s'' i)) \<notin> reveals tr"- shows "LN ''k'' i \<notin> knows tr"-using asms-by(auto dest!: nonce_after_lkr intro: compr_predOrdI)--lemma (in CR_state) client_k_secrecy_old:- assumes asms:- "role th i = Some client"- "LN ''k'' i \<in> knows tr"- "RLKR (\<sigma>(AV ''s'' i)) \<notin> reveals tr"- shows "False"-using asms-proof(sources "LN ''k'' i")- case client_1_k thus False by (sources "SK (\<sigma> (AV ''s'' i))") (auto intro: compr_predOrdI)-qed--lemma (in CR_state) client_nisynch:- assumes asms: "(i, client_2) \<in> steps tr"- "roleMap th i = Some client"- and reveal_after: "\<sigma>(AV ''s'' i) \<in> lkreveals tr \<Longrightarrow> St (i, client_2) \<prec> LKR (\<sigma>(AV ''s'' i))"- shows- "\<exists> j. role th j = Some server \<and>- \<sigma>(AV ''s'' i) = \<sigma>(AV ''s'' j) \<and>- LN ''k'' i = s(MV ''v'' j) \<and>- St(i, client_1) \<prec> St (j, server_1) \<and>- St(j, server_2) \<prec> St (i, client_2)" (is "?syncWith")-proof -- note_prefix_closed facts = asms- thus ?thesis- proof(sources! "Hash (LN ''k'' i)")- case fake- thus "?thesis" using facts and reveal_after - apply -- apply(frule_tac x = "LN ''k'' i" in in_knows_predOrd1)-- apply(frule nonce_after_lkr)- apply(assumption)- apply(frule_tac x = "\<sigma> (AV ''s'' i)" in in_lkreveals_predOrd1)- apply(simp)- done- next- case (server_2_hash j)- note facts_s2h = this - thus "?thesis" using facts and reveal_after - proof (sources! "Enc (\<sigma> (MV ''v'' j)) (PK (\<sigma> (AV ''s'' j)))")- case fake - thus "?thesis" using facts and facts_s2h and reveal_after- apply -- apply(frule_tac x = "\<sigma> (MV ''v'' j)" in in_knows_predOrd1)- apply(frule nonce_after_lkr)- apply(simp)- apply(frule in_lkreveals_predOrd1)- apply(simp)- done- next - case client_1_enc thus "?thesis" using facts_s2h and facts and reveal_after by auto- qed- qed-qed - --text{*- Please note that the easiest way to construct machine-checked- security proofs is to use the 'scyther-proof' tool, as described- in the accompanying README file.-- The only exception are security proofs with respect to compromising- adversaries, as described in Martin Schaub, ``Efficient Interactive- Construction of Machine-Checked Protocol Security Proofs in the Context of- Dynamically Compromising Adversaries''. Master Thesis. ETH Zurich, 2011.- See the corresponding publication in the 'publications' directory and- the corresponding examples in 'compromising_adversaries'.-*}---end---- -
scyther-proof.cabal view
@@ -1,6 +1,6 @@ build-type: Simple name: scyther-proof-version: 0.6.0.0+version: 0.8.0.0 license: GPL license-file: LICENSE category: Security, Theorem Provers@@ -112,9 +112,9 @@ containers >= 0.4.2 && < 0.5 , safe >= 0.2 && < 0.4 , - mtl == 2.0.* ,+ mtl >= 2.1 && < 3.0, - cmdargs >= 0.6.8 && < 0.7 ,+ cmdargs >= 0.10.7 , filepath >= 1.2 && < 1.4 , directory >= 1.0 && < 1.3 , process == 1.1.* ,
src/Main.hs view
@@ -29,7 +29,7 @@ import System.Process import System.Console.CmdArgs.Text-import System.Console.CmdArgs.Explicit+import System.Console.CmdArgs.Explicit hiding (complete) import Extension.Prelude @@ -62,7 +62,7 @@ [ programName , " " , showVersion version- , ", (C) Simon Meier, Andreas Lochbihler, ETH Zurich, 2009-2013"+ , ", (C) Simon Meier, Andreas Lochbihler, ETH Zurich, 2009-2014" ] -- | Version string with HTML markup.@@ -74,7 +74,7 @@ , ", © " , link "https://github.com/meiersi/scyther-proof" "Simon Meier" , link "http://github.com/meiersi" "Andreas Lochbihler"- , ", ETH Zurich, 2009-2013"+ , ", ETH Zurich, 2009-2014" ] where link href name =@@ -120,7 +120,7 @@ processArgs argMode >>= run where run as- | argExists "help" as = print $ helpText HelpFormatAll argMode+ | argExists "help" as = print $ helpText [] HelpFormatAll argMode | argExists "version" as = putStrLn versionStr | otherwise = io as @@ -151,14 +151,14 @@ , " The '--html' flag requires the 'dot' tool from GraphViz available at:" , " " ++ "http://www.graphviz.org/" , " "- , " The '--isabelle' flag requires the 'Isabelle-2013' release of Isabelle/HOL:"- , " " ++ "http://isabelle.in.tum.de/website-Isabelle2013/index.html"+ , " The '--isabelle' flag requires the 'Isabelle2013-2' release of Isabelle/HOL:"+ , " " ++ "http://isabelle.in.tum.de/website-Isabelle2013-2/" , "" , " Check the '" ++ readmePath ++ "' file for instructions on how to load the generated theory files in Isabelle's interactive mode." ] ) { modeCheck = upd "mode" "translate"- , modeArgs = Just $ flagArg (upd "inFile") "FILES"+ , modeArgs = ([], Just $ flagArg (upd "inFile") "FILES") , modeGroupFlags = Group { groupUnnamed = [ flagNone ["first", "f"] (addArg "strategy" "first")@@ -239,11 +239,12 @@ , modeNames = [name] , modeValue = [] , modeCheck = upd "mode" name+ , modeExpandAt = True , modeReform = const Nothing-- no reform possibility , modeHelp = help , modeHelpSuffix = helpSuffix- , modeArgs = Nothing -- no positional arguments- , modeGroupFlags = toGroup [] -- no flags+ , modeArgs = ([], Nothing) -- no positional arguments+ , modeGroupFlags = toGroup [] -- no flags } outputFlags =@@ -259,7 +260,7 @@ putStrLn $ "error: " ++ msg putStrLn $ "" putStrLn $ showText (Wrap 100)- $ helpText HelpFormatDefault mainMode+ $ helpText [] HelpFormatDefault mainMode exitFailure @@ -756,14 +757,14 @@ putStrLn "" where checkVersion out _- | "Isabelle2013" `isInfixOf` out = Right $ init out ++ ". OK."+ | "Isabelle2013-2" `isInfixOf` out = Right $ init out ++ ". OK." | otherwise = Left $ unlines $ [ "WARNING:" , ""- , " " ++ programName ++ " requires Isabelle2013."+ , " " ++ programName ++ " requires Isabelle2013-2." , " Proof checking is likely not to work."- , " Please download Isabelle2013 from:"- , " http://isabelle.in.tum.de/website-Isabelle2013/index.html"+ , " Please download Isabelle2013-2 from:"+ , " http://isabelle.in.tum.de/website-Isabelle2013-2/" ] checkLogics out _
src/System/Isabelle.hs view
@@ -2,7 +2,7 @@ -- -- Requirements: ----- 1. A working installation of Isabelle2013 (http://isabelle.in.tum.de/)+-- 1. A working installation of Isabelle2013-2 (http://isabelle.in.tum.de/) -- 2. The \'isabelle\' command must be on the PATH. -- module System.Isabelle (