src/HOL/SET_Protocol/Merchant_Registration.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 33028 9aa8bfb1649d
child 58889 5b7a9633cfa8
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33028
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 32960
diff changeset
     1
(*  Title:      HOL/SET_Protocol/Merchant_Registration.thy
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
     2
    Author:     Giampaolo Bella
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
     3
    Author:     Fabio Massacci
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
     4
    Author:     Lawrence C Paulson
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     5
*)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     6
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     7
header{*The SET Merchant Registration Protocol*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     8
33028
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 32960
diff changeset
     9
theory Merchant_Registration
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 32960
diff changeset
    10
imports Public_SET
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 32960
diff changeset
    11
begin
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    12
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    13
text{*Copmpared with Cardholder Reigstration, @{text KeyCryptKey} is not
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    14
  needed: no session key encrypts another.  Instead we
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    15
  prove the "key compromise" theorems for sets KK that contain no private
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    16
  encryption keys (@{term "priEK C"}). *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    17
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    18
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    19
inductive_set
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    20
  set_mr :: "event list set"
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    21
where
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    22
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    23
  Nil:    --{*Initial trace is empty*}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    24
           "[] \<in> set_mr"
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    25
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    26
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    27
| Fake:    --{*The spy MAY say anything he CAN say.*}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    28
           "[| evsf \<in> set_mr; X \<in> synth (analz (knows Spy evsf)) |]
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    29
            ==> Says Spy B X  # evsf \<in> set_mr"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    30
        
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    31
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    32
| Reception: --{*If A sends a message X to B, then B might receive it*}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    33
             "[| evsr \<in> set_mr; Says A B X \<in> set evsr |]
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    34
              ==> Gets B X  # evsr \<in> set_mr"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    35
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    36
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    37
| SET_MR1: --{*RegFormReq: M requires a registration form to a CA*}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    38
           "[| evs1 \<in> set_mr; M = Merchant k; Nonce NM1 \<notin> used evs1 |]
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    39
            ==> Says M (CA i) {|Agent M, Nonce NM1|} # evs1 \<in> set_mr"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    40
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    41
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    42
| SET_MR2: --{*RegFormRes: CA replies with the registration form and the 
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    43
               certificates for her keys*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    44
  "[| evs2 \<in> set_mr; Nonce NCA \<notin> used evs2;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    45
      Gets (CA i) {|Agent M, Nonce NM1|} \<in> set evs2 |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    46
   ==> Says (CA i) M {|sign (priSK (CA i)) {|Agent M, Nonce NM1, Nonce NCA|},
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    47
                       cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    48
                       cert (CA i) (pubSK (CA i)) onlySig (priSK RCA) |}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    49
         # evs2 \<in> set_mr"
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    50
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    51
| SET_MR3:
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    52
         --{*CertReq: M submits the key pair to be certified.  The Notes
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    53
             event allows KM1 to be lost if M is compromised. Piero remarks
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    54
             that the agent mentioned inside the signature is not verified to
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    55
             correspond to M.  As in CR, each Merchant has fixed key pairs.  M
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    56
             is only optionally required to send NCA back, so M doesn't do so
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    57
             in the model*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    58
  "[| evs3 \<in> set_mr; M = Merchant k; Nonce NM2 \<notin> used evs3;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    59
      Key KM1 \<notin> used evs3;  KM1 \<in> symKeys;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    60
      Gets M {|sign (invKey SKi) {|Agent X, Nonce NM1, Nonce NCA|},
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    61
               cert (CA i) EKi onlyEnc (priSK RCA),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    62
               cert (CA i) SKi onlySig (priSK RCA) |}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    63
        \<in> set evs3;
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    64
      Says M (CA i) {|Agent M, Nonce NM1|} \<in> set evs3 |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    65
   ==> Says M (CA i)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    66
            {|Crypt KM1 (sign (priSK M) {|Agent M, Nonce NM2,
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    67
                                          Key (pubSK M), Key (pubEK M)|}),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    68
              Crypt EKi (Key KM1)|}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    69
         # Notes M {|Key KM1, Agent (CA i)|}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    70
         # evs3 \<in> set_mr"
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    71
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    72
| SET_MR4:
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    73
         --{*CertRes: CA issues the certificates for merSK and merEK,
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    74
             while checking never to have certified the m even
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    75
             separately. NOTE: In Cardholder Registration the
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    76
             corresponding rule (6) doesn't use the "sign" primitive. "The
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    77
             CertRes shall be signed but not encrypted if the EE is a Merchant
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    78
             or Payment Gateway."-- Programmer's Guide, page 191.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    79
    "[| evs4 \<in> set_mr; M = Merchant k;
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    80
        merSK \<notin> symKeys;  merEK \<notin> symKeys;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    81
        Notes (CA i) (Key merSK) \<notin> set evs4;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    82
        Notes (CA i) (Key merEK) \<notin> set evs4;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    83
        Gets (CA i) {|Crypt KM1 (sign (invKey merSK)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    84
                                 {|Agent M, Nonce NM2, Key merSK, Key merEK|}),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    85
                      Crypt (pubEK (CA i)) (Key KM1) |}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    86
          \<in> set evs4 |]
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    87
    ==> Says (CA i) M {|sign (priSK(CA i)) {|Agent M, Nonce NM2, Agent(CA i)|},
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    88
                        cert  M      merSK    onlySig (priSK (CA i)),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    89
                        cert  M      merEK    onlyEnc (priSK (CA i)),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    90
                        cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    91
          # Notes (CA i) (Key merSK)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    92
          # Notes (CA i) (Key merEK)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
    93
          # evs4 \<in> set_mr"
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    94
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    95
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    96
text{*Note possibility proofs are missing.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    97
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    98
declare Says_imp_knows_Spy [THEN parts.Inj, dest]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    99
declare parts.Body [dest]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   100
declare analz_into_parts [dest]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   101
declare Fake_parts_insert_in_Un [dest]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   102
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   103
text{*General facts about message reception*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   104
lemma Gets_imp_Says:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   105
     "[| Gets B X \<in> set evs; evs \<in> set_mr |] ==> \<exists>A. Says A B X \<in> set evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   106
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   107
apply (erule set_mr.induct, auto)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   108
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   109
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   110
lemma Gets_imp_knows_Spy:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   111
     "[| Gets B X \<in> set evs; evs \<in> set_mr |]  ==> X \<in> knows Spy evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   112
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   113
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   114
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   115
declare Gets_imp_knows_Spy [THEN parts.Inj, dest]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   116
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   117
subsubsection{*Proofs on keys *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   118
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   119
text{*Spy never sees an agent's private keys! (unless it's bad at start)*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   120
lemma Spy_see_private_Key [simp]:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   121
     "evs \<in> set_mr
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   122
      ==> (Key(invKey (publicKey b A)) \<in> parts(knows Spy evs)) = (A \<in> bad)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   123
apply (erule set_mr.induct)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   124
apply (auto dest!: Gets_imp_knows_Spy [THEN parts.Inj])
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   125
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   126
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   127
lemma Spy_analz_private_Key [simp]:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   128
     "evs \<in> set_mr ==>
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   129
     (Key(invKey (publicKey b A)) \<in> analz(knows Spy evs)) = (A \<in> bad)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   130
by auto
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   131
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   132
declare Spy_see_private_Key [THEN [2] rev_iffD1, dest!]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   133
declare Spy_analz_private_Key [THEN [2] rev_iffD1, dest!]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   134
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   135
(*This is to state that the signed keys received in step 4
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   136
  are into parts - rather than installing sign_def each time.
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   137
  Needed in Spy_see_priSK_RCA, Spy_see_priEK and in Spy_see_priSK
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   138
Goal "[|Gets C \<lbrace>Crypt KM1
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   139
                (sign K \<lbrace>Agent M, Nonce NM2, Key merSK, Key merEK\<rbrace>), X\<rbrace>
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   140
          \<in> set evs;  evs \<in> set_mr |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   141
    ==> Key merSK \<in> parts (knows Spy evs) \<and>
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   142
        Key merEK \<in> parts (knows Spy evs)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   143
by (fast_tac (claset() addss (simpset())) 1);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   144
qed "signed_keys_in_parts";
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   145
???*)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   146
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   147
text{*Proofs on certificates -
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   148
  they hold, as in CR, because RCA's keys are secure*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   149
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   150
lemma Crypt_valid_pubEK:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   151
     "[| Crypt (priSK RCA) {|Agent (CA i), Key EKi, onlyEnc|}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   152
           \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   153
         evs \<in> set_mr |] ==> EKi = pubEK (CA i)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   154
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   155
apply (erule set_mr.induct, auto)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   156
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   157
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   158
lemma certificate_valid_pubEK:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   159
    "[| cert (CA i) EKi onlyEnc (priSK RCA) \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   160
        evs \<in> set_mr |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   161
     ==> EKi = pubEK (CA i)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   162
apply (unfold cert_def signCert_def)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   163
apply (blast dest!: Crypt_valid_pubEK)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   164
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   165
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   166
lemma Crypt_valid_pubSK:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   167
     "[| Crypt (priSK RCA) {|Agent (CA i), Key SKi, onlySig|}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   168
           \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   169
         evs \<in> set_mr |] ==> SKi = pubSK (CA i)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   170
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   171
apply (erule set_mr.induct, auto)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   172
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   173
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   174
lemma certificate_valid_pubSK:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   175
    "[| cert (CA i) SKi onlySig (priSK RCA) \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   176
        evs \<in> set_mr |] ==> SKi = pubSK (CA i)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   177
apply (unfold cert_def signCert_def)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   178
apply (blast dest!: Crypt_valid_pubSK)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   179
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   180
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   181
lemma Gets_certificate_valid:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   182
     "[| Gets A {| X, cert (CA i) EKi onlyEnc (priSK RCA),
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   183
                      cert (CA i) SKi onlySig (priSK RCA)|} \<in> set evs;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   184
         evs \<in> set_mr |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   185
      ==> EKi = pubEK (CA i) & SKi = pubSK (CA i)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   186
by (blast dest: certificate_valid_pubEK certificate_valid_pubSK)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   187
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   188
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   189
text{*Nobody can have used non-existent keys!*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   190
lemma new_keys_not_used [rule_format,simp]:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   191
     "evs \<in> set_mr
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   192
      ==> Key K \<notin> used evs --> K \<in> symKeys -->
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   193
          K \<notin> keysFor (parts (knows Spy evs))"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   194
apply (erule set_mr.induct, simp_all)
14218
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14199
diff changeset
   195
apply (force dest!: usedI keysFor_parts_insert)  --{*Fake*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14199
diff changeset
   196
apply force  --{*Message 2*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14199
diff changeset
   197
apply (blast dest: Gets_certificate_valid)  --{*Message 3*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14199
diff changeset
   198
apply force  --{*Message 4*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   199
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   200
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   201
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   202
subsubsection{*New Versions: As Above, but Generalized with the Kk Argument*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   203
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   204
lemma gen_new_keys_not_used [rule_format]:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   205
     "evs \<in> set_mr
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   206
      ==> Key K \<notin> used evs --> K \<in> symKeys -->
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   207
          K \<notin> keysFor (parts (Key`KK Un knows Spy evs))"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   208
by auto
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   209
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   210
lemma gen_new_keys_not_analzd:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   211
     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_mr |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   212
      ==> K \<notin> keysFor (analz (Key`KK Un knows Spy evs))"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   213
by (blast intro: keysFor_mono [THEN [2] rev_subsetD]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   214
          dest: gen_new_keys_not_used)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   215
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   216
lemma analz_Key_image_insert_eq:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   217
     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_mr |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   218
      ==> analz (Key ` (insert K KK) \<union> knows Spy evs) =
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   219
          insert (Key K) (analz (Key ` KK \<union> knows Spy evs))"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   220
by (simp add: gen_new_keys_not_analzd)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   221
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   222
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   223
lemma Crypt_parts_imp_used:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   224
     "[|Crypt K X \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   225
        K \<in> symKeys; evs \<in> set_mr |] ==> Key K \<in> used evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   226
apply (rule ccontr)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   227
apply (force dest: new_keys_not_used Crypt_imp_invKey_keysFor)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   228
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   229
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   230
lemma Crypt_analz_imp_used:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   231
     "[|Crypt K X \<in> analz (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   232
        K \<in> symKeys; evs \<in> set_mr |] ==> Key K \<in> used evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   233
by (blast intro: Crypt_parts_imp_used)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   234
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   235
text{*Rewriting rule for private encryption keys.  Analogous rewriting rules
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   236
for other keys aren't needed.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   237
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   238
lemma parts_image_priEK:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   239
     "[|Key (priEK (CA i)) \<in> parts (Key`KK Un (knows Spy evs));
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   240
        evs \<in> set_mr|] ==> priEK (CA i) \<in> KK | CA i \<in> bad"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   241
by auto
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   242
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   243
text{*trivial proof because (priEK (CA i)) never appears even in (parts evs)*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   244
lemma analz_image_priEK:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   245
     "evs \<in> set_mr ==>
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   246
          (Key (priEK (CA i)) \<in> analz (Key`KK Un (knows Spy evs))) =
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   247
          (priEK (CA i) \<in> KK | CA i \<in> bad)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   248
by (blast dest!: parts_image_priEK intro: analz_mono [THEN [2] rev_subsetD])
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   249
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   250
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   251
subsection{*Secrecy of Session Keys*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   252
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   253
text{*This holds because if (priEK (CA i)) appears in any traffic then it must
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   254
  be known to the Spy, by @{text Spy_see_private_Key}*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   255
lemma merK_neq_priEK:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   256
     "[|Key merK \<notin> analz (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   257
        Key merK \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   258
        evs \<in> set_mr|] ==> merK \<noteq> priEK C"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   259
by blast
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   260
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   261
text{*Lemma for message 4: either merK is compromised (when we don't care)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   262
  or else merK hasn't been used to encrypt K.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   263
lemma msg4_priEK_disj:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   264
     "[|Gets B {|Crypt KM1
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   265
                       (sign K {|Agent M, Nonce NM2, Key merSK, Key merEK|}),
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   266
                 Y|} \<in> set evs;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   267
        evs \<in> set_mr|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   268
  ==> (Key merSK \<in> analz (knows Spy evs) | merSK \<notin> range(\<lambda>C. priEK C))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   269
   &  (Key merEK \<in> analz (knows Spy evs) | merEK \<notin> range(\<lambda>C. priEK C))"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   270
apply (unfold sign_def)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   271
apply (blast dest: merK_neq_priEK)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   272
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   273
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   274
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   275
lemma Key_analz_image_Key_lemma:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   276
     "P --> (Key K \<in> analz (Key`KK Un H)) --> (K\<in>KK | Key K \<in> analz H)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   277
      ==>
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   278
      P --> (Key K \<in> analz (Key`KK Un H)) = (K\<in>KK | Key K \<in> analz H)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   279
by (blast intro: analz_mono [THEN [2] rev_subsetD])
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   280
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   281
lemma symKey_compromise:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   282
     "evs \<in> set_mr ==>
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   283
      (\<forall>SK KK. SK \<in> symKeys \<longrightarrow> (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C)) -->
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   284
               (Key SK \<in> analz (Key`KK Un (knows Spy evs))) =
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   285
               (SK \<in> KK | Key SK \<in> analz (knows Spy evs)))"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   286
apply (erule set_mr.induct)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   287
apply (safe del: impI intro!: Key_analz_image_Key_lemma [THEN impI])
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   288
apply (drule_tac [7] msg4_priEK_disj)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   289
apply (frule_tac [6] Gets_certificate_valid)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   290
apply (safe del: impI)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   291
apply (simp_all del: image_insert image_Un imp_disjL
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   292
         add: analz_image_keys_simps abbrev_simps analz_knows_absorb
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   293
              analz_knows_absorb2 analz_Key_image_insert_eq notin_image_iff
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   294
              Spy_analz_private_Key analz_image_priEK)
24123
a0fc58900606 tuned ML bindings (for multithreading);
wenzelm
parents: 23755
diff changeset
   295
  --{*5 seconds on a 1.6GHz machine*}
14218
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14199
diff changeset
   296
apply spy_analz  --{*Fake*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14199
diff changeset
   297
apply auto  --{*Message 3*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   298
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   299
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   300
lemma symKey_secrecy [rule_format]:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   301
     "[|CA i \<notin> bad; K \<in> symKeys;  evs \<in> set_mr|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   302
      ==> \<forall>X m. Says (Merchant m) (CA i) X \<in> set evs -->
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   303
                Key K \<in> parts{X} -->
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   304
                Merchant m \<notin> bad -->
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   305
                Key K \<notin> analz (knows Spy evs)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   306
apply (erule set_mr.induct)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   307
apply (drule_tac [7] msg4_priEK_disj)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   308
apply (frule_tac [6] Gets_certificate_valid)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   309
apply (safe del: impI)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   310
apply (simp_all del: image_insert image_Un imp_disjL
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   311
         add: analz_image_keys_simps abbrev_simps analz_knows_absorb
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   312
              analz_knows_absorb2 analz_Key_image_insert_eq
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   313
              symKey_compromise notin_image_iff Spy_analz_private_Key
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   314
              analz_image_priEK)
14218
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14199
diff changeset
   315
apply spy_analz  --{*Fake*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14199
diff changeset
   316
apply force  --{*Message 1*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14199
diff changeset
   317
apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used)  --{*Message 3*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   318
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   319
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   320
subsection{*Unicity *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   321
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   322
lemma msg4_Says_imp_Notes:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   323
 "[|Says (CA i) M {|sign (priSK (CA i)) {|Agent M, Nonce NM2, Agent (CA i)|},
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
   324
                    cert  M      merSK    onlySig (priSK (CA i)),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
   325
                    cert  M      merEK    onlyEnc (priSK (CA i)),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
   326
                    cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|} \<in> set evs;
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   327
    evs \<in> set_mr |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   328
  ==> Notes (CA i) (Key merSK) \<in> set evs
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   329
   &  Notes (CA i) (Key merEK) \<in> set evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   330
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   331
apply (erule set_mr.induct)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   332
apply (simp_all (no_asm_simp))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   333
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   334
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   335
text{*Unicity of merSK wrt a given CA:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   336
  merSK uniquely identifies the other components, including merEK*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   337
lemma merSK_unicity:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   338
 "[|Says (CA i) M {|sign (priSK(CA i)) {|Agent M, Nonce NM2, Agent (CA i)|},
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
   339
                    cert  M      merSK    onlySig (priSK (CA i)),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
   340
                    cert  M      merEK    onlyEnc (priSK (CA i)),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
   341
                    cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|} \<in> set evs;
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   342
    Says (CA i) M' {|sign (priSK(CA i)) {|Agent M', Nonce NM2', Agent (CA i)|},
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
   343
                    cert  M'      merSK    onlySig (priSK (CA i)),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
   344
                    cert  M'      merEK'    onlyEnc (priSK (CA i)),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
   345
                    cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)|} \<in> set evs;
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   346
    evs \<in> set_mr |] ==> M=M' & NM2=NM2' & merEK=merEK'"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   347
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   348
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   349
apply (erule set_mr.induct)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   350
apply (simp_all (no_asm_simp))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   351
apply (blast dest!: msg4_Says_imp_Notes)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   352
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   353
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   354
text{*Unicity of merEK wrt a given CA:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   355
  merEK uniquely identifies the other components, including merSK*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   356
lemma merEK_unicity:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   357
 "[|Says (CA i) M {|sign (priSK(CA i)) {|Agent M, Nonce NM2, Agent (CA i)|},
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
   358
                    cert  M      merSK    onlySig (priSK (CA i)),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
   359
                    cert  M      merEK    onlyEnc (priSK (CA i)),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
   360
                    cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|} \<in> set evs;
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   361
    Says (CA i) M' {|sign (priSK(CA i)) {|Agent M', Nonce NM2', Agent (CA i)|},
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
   362
                     cert  M'      merSK'    onlySig (priSK (CA i)),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
   363
                     cert  M'      merEK    onlyEnc (priSK (CA i)),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24123
diff changeset
   364
                     cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)|} \<in> set evs;
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   365
    evs \<in> set_mr |] 
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   366
  ==> M=M' & NM2=NM2' & merSK=merSK'"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   367
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   368
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   369
apply (erule set_mr.induct)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   370
apply (simp_all (no_asm_simp))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   371
apply (blast dest!: msg4_Says_imp_Notes)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   372
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   373
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   374
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   375
text{* -No interest on secrecy of nonces: they appear to be used
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   376
    only for freshness.
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   377
   -No interest on secrecy of merSK or merEK, as in CR.
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   378
   -There's no equivalent of the PAN*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   379
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   380
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   381
subsection{*Primary Goals of Merchant Registration *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   382
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   383
subsubsection{*The merchant's certificates really were created by the CA,
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   384
provided the CA is uncompromised *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   385
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   386
text{*The assumption @{term "CA i \<noteq> RCA"} is required: step 2 uses 
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   387
  certificates of the same form.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   388
lemma certificate_merSK_valid_lemma [intro]:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   389
     "[|Crypt (priSK (CA i)) {|Agent M, Key merSK, onlySig|}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   390
          \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   391
        CA i \<notin> bad;  CA i \<noteq> RCA;  evs \<in> set_mr|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   392
 ==> \<exists>X Y Z. Says (CA i) M
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   393
                  {|X, cert M merSK onlySig (priSK (CA i)), Y, Z|} \<in> set evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   394
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   395
apply (erule set_mr.induct)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   396
apply (simp_all (no_asm_simp))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   397
apply auto
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   398
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   399
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   400
lemma certificate_merSK_valid:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   401
     "[| cert M merSK onlySig (priSK (CA i)) \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   402
         CA i \<notin> bad;  CA i \<noteq> RCA;  evs \<in> set_mr|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   403
 ==> \<exists>X Y Z. Says (CA i) M
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   404
                  {|X, cert M merSK onlySig (priSK (CA i)), Y, Z|} \<in> set evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   405
by auto
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   406
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   407
lemma certificate_merEK_valid_lemma [intro]:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   408
     "[|Crypt (priSK (CA i)) {|Agent M, Key merEK, onlyEnc|}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   409
          \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   410
        CA i \<notin> bad;  CA i \<noteq> RCA;  evs \<in> set_mr|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   411
 ==> \<exists>X Y Z. Says (CA i) M
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   412
                  {|X, Y, cert M merEK onlyEnc (priSK (CA i)), Z|} \<in> set evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   413
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   414
apply (erule set_mr.induct)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   415
apply (simp_all (no_asm_simp))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   416
apply auto
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   417
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   418
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   419
lemma certificate_merEK_valid:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   420
     "[| cert M merEK onlyEnc (priSK (CA i)) \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   421
         CA i \<notin> bad;  CA i \<noteq> RCA;  evs \<in> set_mr|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   422
 ==> \<exists>X Y Z. Says (CA i) M
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   423
                  {|X, Y, cert M merEK onlyEnc (priSK (CA i)), Z|} \<in> set evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   424
by auto
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   425
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   426
text{*The two certificates - for merSK and for merEK - cannot be proved to
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   427
  have originated together*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   428
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   429
end