1.1 --- a/src/HOL/Auth/CertifiedEmail.thy Tue Jul 20 14:23:09 2004 +0200
1.2 +++ b/src/HOL/Auth/CertifiedEmail.thy Tue Jul 20 14:24:23 2004 +0200
1.3 @@ -48,26 +48,26 @@
1.4 ==> Notes TTP {|Agent Spy, Agent TTP, X|} # evsfssl \<in> certified_mail"
1.5
1.6 CM1: --{*The sender approaches the recipient. The message is a number.*}
1.7 -"[|evs1 \<in> certified_mail;
1.8 - Key K \<notin> used evs1;
1.9 - K \<in> symKeys;
1.10 - Nonce q \<notin> used evs1;
1.11 - hs = Hash {|Number cleartext, Nonce q, response S R q, Crypt K (Number m)|};
1.12 - S2TTP = Crypt (pubEK TTP) {|Agent S, Number BothAuth, Key K, Agent R, hs|}|]
1.13 - ==> Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number BothAuth,
1.14 - Number cleartext, Nonce q, S2TTP|} # evs1
1.15 - \<in> certified_mail"
1.16 + "[|evs1 \<in> certified_mail;
1.17 + Key K \<notin> used evs1;
1.18 + K \<in> symKeys;
1.19 + Nonce q \<notin> used evs1;
1.20 + hs = Hash{|Number cleartext, Nonce q, response S R q, Crypt K (Number m)|};
1.21 + S2TTP = Crypt(pubEK TTP) {|Agent S, Number BothAuth, Key K, Agent R, hs|}|]
1.22 + ==> Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number BothAuth,
1.23 + Number cleartext, Nonce q, S2TTP|} # evs1
1.24 + \<in> certified_mail"
1.25
1.26 CM2: --{*The recipient records @{term S2TTP} while transmitting it and her
1.27 password to @{term TTP} over an SSL channel.*}
1.28 -"[|evs2 \<in> certified_mail;
1.29 - Gets R {|Agent S, Agent TTP, em, Number BothAuth, Number cleartext,
1.30 - Nonce q, S2TTP|} \<in> set evs2;
1.31 - TTP \<noteq> R;
1.32 - hr = Hash {|Number cleartext, Nonce q, response S R q, em|} |]
1.33 - ==>
1.34 - Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} # evs2
1.35 - \<in> certified_mail"
1.36 + "[|evs2 \<in> certified_mail;
1.37 + Gets R {|Agent S, Agent TTP, em, Number BothAuth, Number cleartext,
1.38 + Nonce q, S2TTP|} \<in> set evs2;
1.39 + TTP \<noteq> R;
1.40 + hr = Hash {|Number cleartext, Nonce q, response S R q, em|} |]
1.41 + ==>
1.42 + Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} # evs2
1.43 + \<in> certified_mail"
1.44
1.45 CM3: --{*@{term TTP} simultaneously reveals the key to the recipient and gives
1.46 a receipt to the sender. The SSL channel does not authenticate
1.47 @@ -79,10 +79,10 @@
1.48 S2TTP = Crypt (pubEK TTP)
1.49 {|Agent S, Number BothAuth, Key k, Agent R, hs|};
1.50 TTP \<noteq> R; hs = hr; k \<in> symKeys|]
1.51 - ==>
1.52 - Notes R {|Agent TTP, Agent R, Key k, hr|} #
1.53 - Gets S (Crypt (priSK TTP) S2TTP) #
1.54 - Says TTP S (Crypt (priSK TTP) S2TTP) # evs3 \<in> certified_mail"
1.55 + ==>
1.56 + Notes R {|Agent TTP, Agent R, Key k, hr|} #
1.57 + Gets S (Crypt (priSK TTP) S2TTP) #
1.58 + Says TTP S (Crypt (priSK TTP) S2TTP) # evs3 \<in> certified_mail"
1.59
1.60 Reception:
1.61 "[|evsr \<in> certified_mail; Says A B X \<in> set evsr|]
2.1 --- a/src/HOL/Auth/ZhouGollmann.thy Tue Jul 20 14:23:09 2004 +0200
2.2 +++ b/src/HOL/Auth/ZhouGollmann.thy Tue Jul 20 14:24:23 2004 +0200
2.3 @@ -178,7 +178,7 @@
2.4 sent it, provided @{term A} is not broken.*}
2.5
2.6 text{*Strong conclusion for a good agent*}
2.7 -lemma NRO_authenticity_good:
2.8 +lemma NRO_validity_good:
2.9 "[|NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
2.10 NRO \<in> parts (spies evs);
2.11 A \<notin> bad; evs \<in> zg |]
2.12 @@ -197,7 +197,7 @@
2.13 done
2.14
2.15 text{*Holds also for @{term "A = Spy"}!*}
2.16 -theorem NRO_authenticity:
2.17 +theorem NRO_validity:
2.18 "[|Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs;
2.19 NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
2.20 A \<notin> broken; evs \<in> zg |]
2.21 @@ -207,8 +207,8 @@
2.22 apply (frule NRO_sender, auto)
2.23 txt{*We are left with the case where the sender is @{term Spy} and not
2.24 equal to @{term A}, because @{term "A \<notin> bad"}.
2.25 - Thus theorem @{text NRO_authenticity_good} applies.*}
2.26 -apply (blast dest: NRO_authenticity_good [OF refl])
2.27 + Thus theorem @{text NRO_validity_good} applies.*}
2.28 +apply (blast dest: NRO_validity_good [OF refl])
2.29 done
2.30
2.31
2.32 @@ -218,7 +218,7 @@
2.33 sent it, provided @{term B} is not broken.*}
2.34
2.35 text{*Strong conclusion for a good agent*}
2.36 -lemma NRR_authenticity_good:
2.37 +lemma NRR_validity_good:
2.38 "[|NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
2.39 NRR \<in> parts (spies evs);
2.40 B \<notin> bad; evs \<in> zg |]
2.41 @@ -237,7 +237,7 @@
2.42 done
2.43
2.44 text{*Holds also for @{term "B = Spy"}!*}
2.45 -theorem NRR_authenticity:
2.46 +theorem NRR_validity:
2.47 "[|Says B' A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs;
2.48 NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
2.49 B \<notin> broken; evs \<in> zg|]
2.50 @@ -245,8 +245,8 @@
2.51 apply clarify
2.52 apply (frule NRR_sender, auto)
2.53 txt{*We are left with the case where @{term "B' = Spy"} and @{term "B' \<noteq> B"},
2.54 - i.e. @{term "B \<notin> bad"}, when we can apply @{text NRR_authenticity_good}.*}
2.55 - apply (blast dest: NRR_authenticity_good [OF refl])
2.56 + i.e. @{term "B \<notin> bad"}, when we can apply @{text NRR_validity_good}.*}
2.57 + apply (blast dest: NRR_validity_good [OF refl])
2.58 done
2.59
2.60
2.61 @@ -256,7 +256,7 @@
2.62 sent it, provided @{term A} is not broken. *}
2.63
2.64 text{*Strong conclusion for a good agent*}
2.65 -lemma sub_K_authenticity_good:
2.66 +lemma sub_K_validity_good:
2.67 "[|sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
2.68 sub_K \<in> parts (spies evs);
2.69 A \<notin> bad; evs \<in> zg |]
2.70 @@ -277,7 +277,7 @@
2.71 done
2.72
2.73 text{*Holds also for @{term "A = Spy"}!*}
2.74 -theorem sub_K_authenticity:
2.75 +theorem sub_K_validity:
2.76 "[|Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs;
2.77 sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
2.78 A \<notin> broken; evs \<in> zg |]
2.79 @@ -287,8 +287,8 @@
2.80 apply (frule sub_K_sender, auto)
2.81 txt{*We are left with the case where the sender is @{term Spy} and not
2.82 equal to @{term A}, because @{term "A \<notin> bad"}.
2.83 - Thus theorem @{text sub_K_authenticity_good} applies.*}
2.84 -apply (blast dest: sub_K_authenticity_good [OF refl])
2.85 + Thus theorem @{text sub_K_validity_good} applies.*}
2.86 +apply (blast dest: sub_K_validity_good [OF refl])
2.87 done
2.88
2.89
2.90 @@ -299,7 +299,7 @@
2.91 and therefore @{term A} and @{term B}) can get it too. Moreover, we know
2.92 that @{term A} sent @{term sub_K}*}
2.93
2.94 -lemma con_K_authenticity:
2.95 +lemma con_K_validity:
2.96 "[|con_K \<in> used evs;
2.97 con_K = Crypt (priK TTP)
2.98 {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
2.99 @@ -331,19 +331,19 @@
2.100 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
2.101 txt{*ZG4*}
2.102 apply clarify
2.103 -apply (rule sub_K_authenticity, auto)
2.104 +apply (rule sub_K_validity, auto)
2.105 done
2.106
2.107 text{*If @{term con_K} exists, then @{term A} sent @{term sub_K}. We again
2.108 assume that @{term A} is not broken. *}
2.109 -theorem B_sub_K_authenticity:
2.110 +theorem B_sub_K_validity:
2.111 "[|con_K \<in> used evs;
2.112 con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
2.113 Nonce L, Key K|};
2.114 sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
2.115 A \<notin> broken; evs \<in> zg|]
2.116 ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
2.117 -by (blast dest: con_K_authenticity Notes_TTP_imp_Says_A)
2.118 +by (blast dest: con_K_validity Notes_TTP_imp_Says_A)
2.119
2.120
2.121 subsection{*Proving fairness*}
2.122 @@ -456,7 +456,7 @@
2.123
2.124
2.125 text{*If @{term con_K} exists at all, then @{term B} can get it, by @{text
2.126 -con_K_authenticity}. Cannot conclude that also NRO is available to @{term B},
2.127 +con_K_validity}. Cannot conclude that also NRO is available to @{term B},
2.128 because if @{term A} were unfair, @{term A} could build message 3 without
2.129 building message 1, which contains NRO. *}
2.130