diff --git a/CHANGES b/CHANGES --- a/CHANGES +++ b/CHANGES @@ -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 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -3,7 +3,7 @@ Authors: Simon Meier Creation Date: 2011-05-13 -Last Updated: 2013-02-27 by Andreas Lochbihler +Last Updated: 2014-01-31 by Andreas Lochbihler 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). diff --git a/data/examples/Makefile b/data/examples/Makefile --- a/data/examples/Makefile +++ b/data/examples/Makefile @@ -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 diff --git a/data/examples/iso9798/isabelle-proofs/isoiec-9798_cert_auto.thy b/data/examples/iso9798/isabelle-proofs/isoiec-9798_cert_auto.thy new file mode 100644 --- /dev/null +++ b/data/examples/iso9798/isabelle-proofs/isoiec-9798_cert_auto.thy @@ -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 diff --git a/data/examples/iso9798/isoiec-9798.spthy b/data/examples/iso9798/isoiec-9798.spthy new file mode 100644 --- /dev/null +++ b/data/examples/iso9798/isoiec-9798.spthy @@ -0,0 +1,1619 @@ +// All protocols in a single file to test their parallel composition. +// Author: Simon Meier +// 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 diff --git a/data/isabelle/README b/data/isabelle/README --- a/data/isabelle/README +++ b/data/isabelle/README @@ -3,7 +3,7 @@ Authors: Simon Meier Creation Date: 2011-05-13 -Last Updated: 2013-02-27 by Andreas Lochbihler +Last Updated: 2014-01-31 by Andreas Lochbihler 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). diff --git a/data/isabelle/src/ESPLogic/Hints.thy b/data/isabelle/src/ESPLogic/Hints.thy --- a/data/isabelle/src/ESPLogic/Hints.thy +++ b/data/isabelle/src/ESPLogic/Hints.thy @@ -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; diff --git a/data/isabelle/src/ESPLogic/Unify.thy b/data/isabelle/src/ESPLogic/Unify.thy --- a/data/isabelle/src/ESPLogic/Unify.thy +++ b/data/isabelle/src/ESPLogic/Unify.thy @@ -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 diff --git a/data/isabelle/src/ESPLogic/WeakTyping.thy b/data/isabelle/src/ESPLogic/WeakTyping.thy --- a/data/isabelle/src/ESPLogic/WeakTyping.thy +++ b/data/isabelle/src/ESPLogic/WeakTyping.thy @@ -713,7 +713,19 @@ m \ knows t" by(auto simp: KnownT_def) +lemma in_SumT_NonceT_NonceTE [elim!]: + "\ m \ SumT (NonceT Ro n) (NonceT Ro' n') i q; + m \ NonceT Ro n i q \ R; + m \ NonceT Ro' n' i q \ R + \ \ 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 *} diff --git a/data/isabelle/src/ESPLogic/espl_definitions.ML b/data/isabelle/src/ESPLogic/espl_definitions.ML --- a/data/isabelle/src/ESPLogic/espl_definitions.ML +++ b/data/isabelle/src/ESPLogic/espl_definitions.ML @@ -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; diff --git a/data/isabelle/src/ESPLogic/espl_methods.ML b/data/isabelle/src/ESPLogic/espl_methods.ML --- a/data/isabelle/src/ESPLogic/espl_methods.ML +++ b/data/isabelle/src/ESPLogic/espl_methods.ML @@ -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) diff --git a/data/isabelle/src/ESPLogic/espl_utils.ML b/data/isabelle/src/ESPLogic/espl_utils.ML --- a/data/isabelle/src/ESPLogic/espl_utils.ML +++ b/data/isabelle/src/ESPLogic/espl_utils.ML @@ -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 *) diff --git a/data/isabelle/src/Tutorial.thy b/data/isabelle/src/Tutorial.thy deleted file mode 100644 --- a/data/isabelle/src/Tutorial.thy +++ /dev/null @@ -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 \ i somePt = Some (Enc (LN ''n'' i) (PK (\(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 \ r" -abbreviation (in reachable_state) "tr \ t" -abbreviation (in reachable_state) "\ \ s" -abbreviation (in reachable_state) "role \ 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,\)$ 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' \ knows t" - shows - "(m' \ IK0) \ - (\ m. m' = Hash m \ Ln m \ Ln (Hash m)) \ - (\ m k. m' = Enc m k \ Ln m \ Ln (Enc m k) \ Ln k \ Ln (Enc m k)) \ - (\ x y. m' = Tup x y \ Ln x \ Ln (Tup x y) \ Ln y \ Ln (Tup x y)) \ - (\ i done todo skipped. r i = Some (done, todo, skipped) \ - (\ l pt m. - Send l pt \ set done \ Some m = inst s i pt \ - decrChain [] t {St (i, Send l pt)} m m' - ) - ) \ - (\ i done todo skipped. r i = Some (done, todo, skipped) \ - (\ l ty pt m. - Note l ty pt \ set done \ Note l ty pt \ skipped \ - Some m = inst s i pt \ - decrChain [] t {St (i, Note l ty pt)} m m' - ) - ) \ - (\ a. m' = SK a \ LKR a \ Ln m') \ - (\ a b. m' = K a b \ LKR a \ Ln m') \ - (\ a b. m' = K a b \ LKR b \ Ln m') \ - (\ A. \ a \ A. m' = KShr A \ LKR (Lit (EAgent a)) \ 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 \ atomic_CR_state -proof - - have "(tr, th, \) \ approx weakly_atomic" - proof(cases rule: reachable_in_approxI_ext - [OF monoTyp_weakly_atomic, completeness_cases_rule]) - case (server_1_v tr th \ tid) - then interpret state: atomic_CR_state tr th \ - by unfold_locales auto - show ?case using server_1_v - by (sources "Enc (\ (MV ''v'' tid)) (PK (\ (AV ''s'' tid)))") - (auto intro: event_predOrdI) - qed - thus "atomic_CR_state tr th \" 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 \ knows tr" - shows "LKR (\(AV ''s'' i)) \ Ln (LN ''k'' i)" (is "?lkrbef") -using asms -proof(sources "LN ''k'' i") - case client_1_k - thus "?thesis" by(sources "SK (\ (AV ''s'' i))") auto -thm noteStep_def -qed - -lemma (in CR_state) client_k_secrecy: - assumes asms: - "role th i = Some client" - "RLKR (\(AV ''s'' i)) \ reveals tr" - shows "LN ''k'' i \ 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 \ knows tr" - "RLKR (\(AV ''s'' i)) \ reveals tr" - shows "False" -using asms -proof(sources "LN ''k'' i") - case client_1_k thus False by (sources "SK (\ (AV ''s'' i))") (auto intro: compr_predOrdI) -qed - -lemma (in CR_state) client_nisynch: - assumes asms: "(i, client_2) \ steps tr" - "roleMap th i = Some client" - and reveal_after: "\(AV ''s'' i) \ lkreveals tr \ St (i, client_2) \ LKR (\(AV ''s'' i))" - shows - "\ j. role th j = Some server \ - \(AV ''s'' i) = \(AV ''s'' j) \ - LN ''k'' i = s(MV ''v'' j) \ - St(i, client_1) \ St (j, server_1) \ - St(j, server_2) \ 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 = "\ (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 (\ (MV ''v'' j)) (PK (\ (AV ''s'' j)))") - case fake - thus "?thesis" using facts and facts_s2h and reveal_after - apply - - apply(frule_tac x = "\ (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 - - - - - diff --git a/scyther-proof.cabal b/scyther-proof.cabal --- a/scyther-proof.cabal +++ b/scyther-proof.cabal @@ -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.* , diff --git a/src/Main.hs b/src/Main.hs --- a/src/Main.hs +++ b/src/Main.hs @@ -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 _ diff --git a/src/System/Isabelle.hs b/src/System/Isabelle.hs --- a/src/System/Isabelle.hs +++ b/src/System/Isabelle.hs @@ -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 (