src/HOL/SET_Protocol/Cardholder_Registration.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 42814 5af15f1e2ef6
child 51798 ad3a241def73
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/Cardholder_Registration.thy
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
     2
    Author:     Giampaolo Bella
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
     3
    Author:     Fabio Massacci
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
     4
    Author:     Lawrence C Paulson
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
     5
    Author:     Piero Tramontano
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     6
*)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     7
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     8
header{*The SET Cardholder Registration Protocol*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
     9
33028
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 32960
diff changeset
    10
theory Cardholder_Registration
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 32960
diff changeset
    11
imports Public_SET
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 32960
diff changeset
    12
begin
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    13
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    14
text{*Note: nonces seem to consist of 20 bytes.  That includes both freshness
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    15
challenges (Chall-EE, etc.) and important secrets (CardSecret, PANsecret)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    16
*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    17
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    18
text{*Simplifications involving @{text analz_image_keys_simps} appear to
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    19
have become much slower. The cause is unclear. However, there is a big blow-up
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    20
and the rewriting is very sensitive to the set of rewrite rules given.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    21
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    22
subsection{*Predicate Formalizing the Encryption Association between Keys *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    23
39758
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 33028
diff changeset
    24
primrec KeyCryptKey :: "[key, key, event list] => bool"
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 33028
diff changeset
    25
where
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 33028
diff changeset
    26
  KeyCryptKey_Nil:
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 33028
diff changeset
    27
    "KeyCryptKey DK K [] = False"
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 33028
diff changeset
    28
| KeyCryptKey_Cons:
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    29
      --{*Says is the only important case.
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    30
        1st case: CR5, where KC3 encrypts KC2.
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    31
        2nd case: any use of priEK C.
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    32
        Revision 1.12 has a more complicated version with separate treatment of
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    33
          the dependency of KC1, KC2 and KC3 on priEK (CA i.)  Not needed since
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    34
          priEK C is never sent (and so can't be lost except at the start). *}
39758
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 33028
diff changeset
    35
    "KeyCryptKey DK K (ev # evs) =
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 33028
diff changeset
    36
     (KeyCryptKey DK K evs |
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 33028
diff changeset
    37
      (case ev of
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 33028
diff changeset
    38
        Says A B Z =>
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 33028
diff changeset
    39
         ((\<exists>N X Y. A \<noteq> Spy &
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    40
                 DK \<in> symKeys &
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    41
                 Z = {|Crypt DK {|Agent A, Nonce N, Key K, X|}, Y|}) |
39758
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 33028
diff changeset
    42
          (\<exists>C. DK = priEK C))
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 33028
diff changeset
    43
      | Gets A' X => False
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 33028
diff changeset
    44
      | Notes A' X => False))"
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    45
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    46
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    47
subsection{*Predicate formalizing the association between keys and nonces *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    48
39758
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 33028
diff changeset
    49
primrec KeyCryptNonce :: "[key, key, event list] => bool"
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 33028
diff changeset
    50
where
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 33028
diff changeset
    51
  KeyCryptNonce_Nil:
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 33028
diff changeset
    52
    "KeyCryptNonce EK K [] = False"
b8a53e3a0ee2 modernized primrecs
haftmann
parents: 33028
diff changeset
    53
| KeyCryptNonce_Cons:
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    54
  --{*Says is the only important case.
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    55
    1st case: CR3, where KC1 encrypts NC2 (distinct from CR5 due to EXH);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    56
    2nd case: CR5, where KC3 encrypts NC3;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    57
    3rd case: CR6, where KC2 encrypts NC3;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    58
    4th case: CR6, where KC2 encrypts NonceCCA;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    59
    5th case: any use of @{term "priEK C"} (including CardSecret).
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    60
    NB the only Nonces we need to keep secret are CardSecret and NonceCCA.
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    61
    But we can't prove @{text Nonce_compromise} unless the relation covers ALL
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    62
        nonces that the protocol keeps secret.
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    63
  *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    64
  "KeyCryptNonce DK N (ev # evs) =
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    65
   (KeyCryptNonce DK N evs |
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    66
    (case ev of
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    67
      Says A B Z =>
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    68
       A \<noteq> Spy &
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    69
       ((\<exists>X Y. DK \<in> symKeys &
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    70
               Z = (EXHcrypt DK X {|Agent A, Nonce N|} Y)) |
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    71
        (\<exists>X Y. DK \<in> symKeys &
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    72
               Z = {|Crypt DK {|Agent A, Nonce N, X|}, Y|}) |
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    73
        (\<exists>K i X Y.
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    74
          K \<in> symKeys &
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    75
          Z = Crypt K {|sign (priSK (CA i)) {|Agent B, Nonce N, X|}, Y|} &
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    76
          (DK=K | KeyCryptKey DK K evs)) |
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    77
        (\<exists>K C NC3 Y.
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    78
          K \<in> symKeys &
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    79
          Z = Crypt K
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    80
                {|sign (priSK C) {|Agent B, Nonce NC3, Agent C, Nonce N|},
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    81
                  Y|} &
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    82
          (DK=K | KeyCryptKey DK K evs)) |
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    83
        (\<exists>C. DK = priEK C))
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    84
    | Gets A' X => False
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    85
    | Notes A' X => False))"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    86
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    87
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    88
subsection{*Formal protocol definition *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    89
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    90
inductive_set
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    91
  set_cr :: "event list set"
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    92
where
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    93
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    94
  Nil:    --{*Initial trace is empty*}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    95
          "[] \<in> set_cr"
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
    96
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    97
| Fake:    --{*The spy MAY say anything he CAN say.*}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    98
           "[| evsf \<in> set_cr; X \<in> synth (analz (knows Spy evsf)) |]
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    99
            ==> Says Spy B X  # evsf \<in> set_cr"
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   100
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   101
| 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: 32404
diff changeset
   102
             "[| evsr \<in> set_cr; Says A B X \<in> set evsr |]
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   103
              ==> Gets B X  # evsr \<in> set_cr"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   104
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   105
| SET_CR1: --{*CardCInitReq: C initiates a run, sending a nonce to CCA*}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   106
             "[| evs1 \<in> set_cr;  C = Cardholder k;  Nonce NC1 \<notin> used evs1 |]
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   107
              ==> Says C (CA i) {|Agent C, Nonce NC1|} # evs1 \<in> set_cr"
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   108
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   109
| SET_CR2: --{*CardCInitRes: CA responds sending NC1 and its certificates*}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   110
             "[| evs2 \<in> set_cr;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   111
                 Gets (CA i) {|Agent C, Nonce NC1|} \<in> set evs2 |]
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   112
              ==> Says (CA i) C
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   113
                       {|sign (priSK (CA i)) {|Agent C, Nonce NC1|},
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   114
                         cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   115
                         cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   116
                    # evs2 \<in> set_cr"
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   117
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   118
| SET_CR3:
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   119
   --{*RegFormReq: C sends his PAN and a new nonce to CA.
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   120
   C verifies that
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   121
    - nonce received is the same as that sent;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   122
    - certificates are signed by RCA;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   123
    - certificates are an encryption certificate (flag is onlyEnc) and a
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   124
      signature certificate (flag is onlySig);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   125
    - certificates pertain to the CA that C contacted (this is done by
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   126
      checking the signature).
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   127
   C generates a fresh symmetric key KC1.
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   128
   The point of encrypting @{term "{|Agent C, Nonce NC2, Hash (Pan(pan C))|}"}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   129
   is not clear. *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   130
"[| evs3 \<in> set_cr;  C = Cardholder k;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   131
    Nonce NC2 \<notin> used evs3;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   132
    Key KC1 \<notin> used evs3; KC1 \<in> symKeys;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   133
    Gets C {|sign (invKey SKi) {|Agent X, Nonce NC1|},
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   134
             cert (CA i) EKi onlyEnc (priSK RCA),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   135
             cert (CA i) SKi onlySig (priSK RCA)|}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   136
       \<in> set evs3;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   137
    Says C (CA i) {|Agent C, Nonce NC1|} \<in> set evs3|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   138
 ==> Says C (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan C)))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   139
       # Notes C {|Key KC1, Agent (CA i)|}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   140
       # evs3 \<in> set_cr"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   141
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   142
| SET_CR4:
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   143
    --{*RegFormRes:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   144
    CA responds sending NC2 back with a new nonce NCA, after checking that
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   145
     - the digital envelope is correctly encrypted by @{term "pubEK (CA i)"}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   146
     - the entire message is encrypted with the same key found inside the
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   147
       envelope (here, KC1) *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   148
"[| evs4 \<in> set_cr;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   149
    Nonce NCA \<notin> used evs4;  KC1 \<in> symKeys;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   150
    Gets (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan X)))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   151
       \<in> set evs4 |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   152
  ==> Says (CA i) C
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   153
          {|sign (priSK (CA i)) {|Agent C, Nonce NC2, Nonce NCA|},
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   154
            cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   155
            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   156
       # evs4 \<in> set_cr"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   157
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   158
| SET_CR5:
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   159
   --{*CertReq: C sends his PAN, a new nonce, its proposed public signature key
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   160
       and its half of the secret value to CA.
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   161
       We now assume that C has a fixed key pair, and he submits (pubSK C).
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   162
       The protocol does not require this key to be fresh.
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   163
       The encryption below is actually EncX.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   164
"[| evs5 \<in> set_cr;  C = Cardholder k;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   165
    Nonce NC3 \<notin> used evs5;  Nonce CardSecret \<notin> used evs5; NC3\<noteq>CardSecret;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   166
    Key KC2 \<notin> used evs5; KC2 \<in> symKeys;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   167
    Key KC3 \<notin> used evs5; KC3 \<in> symKeys; KC2\<noteq>KC3;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   168
    Gets C {|sign (invKey SKi) {|Agent C, Nonce NC2, Nonce NCA|},
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   169
             cert (CA i) EKi onlyEnc (priSK RCA),
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   170
             cert (CA i) SKi onlySig (priSK RCA) |}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   171
        \<in> set evs5;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   172
    Says C (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan C)))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   173
         \<in> set evs5 |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   174
==> Says C (CA i)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   175
         {|Crypt KC3
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   176
             {|Agent C, Nonce NC3, Key KC2, Key (pubSK C),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   177
               Crypt (priSK C)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   178
                 (Hash {|Agent C, Nonce NC3, Key KC2,
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   179
                         Key (pubSK C), Pan (pan C), Nonce CardSecret|})|},
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   180
           Crypt EKi {|Key KC3, Pan (pan C), Nonce CardSecret|} |}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   181
    # Notes C {|Key KC2, Agent (CA i)|}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   182
    # Notes C {|Key KC3, Agent (CA i)|}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   183
    # evs5 \<in> set_cr"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   184
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   185
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   186
  --{* CertRes: CA responds sending NC3 back with its half of the secret value,
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   187
   its signature certificate and the new cardholder signature
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   188
   certificate.  CA checks to have never certified the key proposed by C.
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   189
   NOTE: In Merchant Registration, the corresponding rule (4)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   190
   uses the "sign" primitive. The encryption below is actually @{term EncK}, 
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   191
   which is just @{term "Crypt K (sign SK X)"}.
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   192
*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   193
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   194
| SET_CR6:
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   195
"[| evs6 \<in> set_cr;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   196
    Nonce NonceCCA \<notin> used evs6;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   197
    KC2 \<in> symKeys;  KC3 \<in> symKeys;  cardSK \<notin> symKeys;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   198
    Notes (CA i) (Key cardSK) \<notin> set evs6;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   199
    Gets (CA i)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   200
      {|Crypt KC3 {|Agent C, Nonce NC3, Key KC2, Key cardSK,
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   201
                    Crypt (invKey cardSK)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   202
                      (Hash {|Agent C, Nonce NC3, Key KC2,
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   203
                              Key cardSK, Pan (pan C), Nonce CardSecret|})|},
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   204
        Crypt (pubEK (CA i)) {|Key KC3, Pan (pan C), Nonce CardSecret|} |}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   205
      \<in> set evs6 |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   206
==> Says (CA i) C
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   207
         (Crypt KC2
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   208
          {|sign (priSK (CA i))
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   209
                 {|Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA|},
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   210
            certC (pan C) cardSK (XOR(CardSecret,NonceCCA)) onlySig (priSK (CA i)),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   211
            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   212
      # Notes (CA i) (Key cardSK)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   213
      # evs6 \<in> set_cr"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   214
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   215
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   216
declare Says_imp_knows_Spy [THEN parts.Inj, dest]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   217
declare parts.Body [dest]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   218
declare analz_into_parts [dest]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   219
declare Fake_parts_insert_in_Un [dest]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   220
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   221
text{*A "possibility property": there are traces that reach the end.
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   222
      An unconstrained proof with many subgoals.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   223
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   224
lemma Says_to_Gets:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   225
     "Says A B X # evs \<in> set_cr ==> Gets B X # Says A B X # evs \<in> set_cr"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   226
by (rule set_cr.Reception, auto)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   227
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   228
text{*The many nonces and keys generated, some simultaneously, force us to
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   229
  introduce them explicitly as shown below.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   230
lemma possibility_CR6:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   231
     "[|NC1 < (NC2::nat);  NC2 < NC3;  NC3 < NCA ;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   232
        NCA < NonceCCA;  NonceCCA < CardSecret;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   233
        KC1 < (KC2::key);  KC2 < KC3;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   234
        KC1 \<in> symKeys;  Key KC1 \<notin> used [];
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   235
        KC2 \<in> symKeys;  Key KC2 \<notin> used [];
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   236
        KC3 \<in> symKeys;  Key KC3 \<notin> used [];
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   237
        C = Cardholder k|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   238
   ==> \<exists>evs \<in> set_cr.
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   239
       Says (CA i) C
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   240
            (Crypt KC2
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   241
             {|sign (priSK (CA i))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   242
                    {|Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA|},
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   243
               certC (pan C) (pubSK (Cardholder k)) (XOR(CardSecret,NonceCCA))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   244
                     onlySig (priSK (CA i)),
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   245
               cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   246
          \<in> set evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   247
apply (intro exI bexI)
14206
77bf175f5145 Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents: 14199
diff changeset
   248
apply (rule_tac [2] 
77bf175f5145 Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents: 14199
diff changeset
   249
       set_cr.Nil 
77bf175f5145 Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents: 14199
diff changeset
   250
        [THEN set_cr.SET_CR1 [of concl: C i NC1], 
77bf175f5145 Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents: 14199
diff changeset
   251
         THEN Says_to_Gets, 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   252
         THEN set_cr.SET_CR2 [of concl: i C NC1], 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   253
         THEN Says_to_Gets,  
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   254
         THEN set_cr.SET_CR3 [of concl: C i KC1 _ NC2], 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   255
         THEN Says_to_Gets,  
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   256
         THEN set_cr.SET_CR4 [of concl: i C NC2 NCA], 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   257
         THEN Says_to_Gets,  
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   258
         THEN set_cr.SET_CR5 [of concl: C i KC3 NC3 KC2 CardSecret],
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   259
         THEN Says_to_Gets,  
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   260
         THEN set_cr.SET_CR6 [of concl: i C KC2]])
30607
c3d1590debd8 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents: 30549
diff changeset
   261
apply basic_possibility
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   262
apply (simp_all (no_asm_simp) add: symKeys_neq_imp_neq)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   263
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   264
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   265
text{*General facts about message reception*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   266
lemma Gets_imp_Says:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   267
     "[| Gets B X \<in> set evs; evs \<in> set_cr |] ==> \<exists>A. Says A B X \<in> set evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   268
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   269
apply (erule set_cr.induct, auto)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   270
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   271
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   272
lemma Gets_imp_knows_Spy:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   273
     "[| Gets B X \<in> set evs; evs \<in> set_cr |]  ==> X \<in> knows Spy evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   274
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   275
declare Gets_imp_knows_Spy [THEN parts.Inj, dest]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   276
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   277
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   278
subsection{*Proofs on keys *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   279
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   280
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
   281
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   282
lemma Spy_see_private_Key [simp]:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   283
     "evs \<in> set_cr
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   284
      ==> (Key(invKey (publicKey b A)) \<in> parts(knows Spy evs)) = (A \<in> bad)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   285
by (erule set_cr.induct, auto)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   286
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   287
lemma Spy_analz_private_Key [simp]:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   288
     "evs \<in> set_cr ==>
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   289
     (Key(invKey (publicKey b A)) \<in> analz(knows Spy evs)) = (A \<in> bad)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   290
by auto
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   291
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   292
declare Spy_see_private_Key [THEN [2] rev_iffD1, dest!]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   293
declare Spy_analz_private_Key [THEN [2] rev_iffD1, dest!]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   294
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   295
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   296
subsection{*Begin Piero's Theorems on Certificates*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   297
text{*Trivial in the current model, where certificates by RCA are secure *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   298
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   299
lemma Crypt_valid_pubEK:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   300
     "[| Crypt (priSK RCA) {|Agent C, Key EKi, onlyEnc|}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   301
           \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   302
         evs \<in> set_cr |] ==> EKi = pubEK C"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   303
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   304
apply (erule set_cr.induct, auto)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   305
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   306
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   307
lemma certificate_valid_pubEK:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   308
    "[| cert C EKi onlyEnc (priSK RCA) \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   309
        evs \<in> set_cr |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   310
     ==> EKi = pubEK C"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   311
apply (unfold cert_def signCert_def)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   312
apply (blast dest!: Crypt_valid_pubEK)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   313
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   314
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   315
lemma Crypt_valid_pubSK:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   316
     "[| Crypt (priSK RCA) {|Agent C, Key SKi, onlySig|}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   317
           \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   318
         evs \<in> set_cr |] ==> SKi = pubSK C"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   319
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   320
apply (erule set_cr.induct, auto)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   321
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   322
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   323
lemma certificate_valid_pubSK:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   324
    "[| cert C SKi onlySig (priSK RCA) \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   325
        evs \<in> set_cr |] ==> SKi = pubSK C"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   326
apply (unfold cert_def signCert_def)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   327
apply (blast dest!: Crypt_valid_pubSK)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   328
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   329
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   330
lemma Gets_certificate_valid:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   331
     "[| Gets A {| X, cert C EKi onlyEnc (priSK RCA),
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   332
                      cert C SKi onlySig (priSK RCA)|} \<in> set evs;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   333
         evs \<in> set_cr |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   334
      ==> EKi = pubEK C & SKi = pubSK C"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   335
by (blast dest: certificate_valid_pubEK certificate_valid_pubSK)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   336
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   337
text{*Nobody can have used non-existent keys!*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   338
lemma new_keys_not_used:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   339
     "[|K \<in> symKeys; Key K \<notin> used evs; evs \<in> set_cr|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   340
      ==> K \<notin> keysFor (parts (knows Spy evs))"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   341
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   342
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   343
apply (erule set_cr.induct)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   344
apply (frule_tac [8] Gets_certificate_valid)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   345
apply (frule_tac [6] Gets_certificate_valid, simp_all)
14218
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   346
apply (force dest!: usedI keysFor_parts_insert) --{*Fake*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   347
apply (blast,auto)  --{*Others*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   348
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   349
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   350
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   351
subsection{*New versions: as above, but generalized to have the KK argument *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   352
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   353
lemma gen_new_keys_not_used:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   354
     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_cr |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   355
      ==> Key K \<notin> used evs --> K \<in> symKeys -->
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   356
          K \<notin> keysFor (parts (Key`KK Un knows Spy evs))"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   357
by (auto simp add: new_keys_not_used)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   358
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   359
lemma gen_new_keys_not_analzd:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   360
     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_cr |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   361
      ==> K \<notin> keysFor (analz (Key`KK Un knows Spy evs))"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   362
by (blast intro: keysFor_mono [THEN [2] rev_subsetD]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   363
          dest: gen_new_keys_not_used)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   364
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   365
lemma analz_Key_image_insert_eq:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   366
     "[|K \<in> symKeys; Key K \<notin> used evs; evs \<in> set_cr |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   367
      ==> analz (Key ` (insert K KK) \<union> knows Spy evs) =
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   368
          insert (Key K) (analz (Key ` KK \<union> knows Spy evs))"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   369
by (simp add: gen_new_keys_not_analzd)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   370
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   371
lemma Crypt_parts_imp_used:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   372
     "[|Crypt K X \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   373
        K \<in> symKeys; evs \<in> set_cr |] ==> Key K \<in> used evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   374
apply (rule ccontr)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   375
apply (force dest: new_keys_not_used Crypt_imp_invKey_keysFor)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   376
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   377
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   378
lemma Crypt_analz_imp_used:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   379
     "[|Crypt K X \<in> analz (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   380
        K \<in> symKeys; evs \<in> set_cr |] ==> Key K \<in> used evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   381
by (blast intro: Crypt_parts_imp_used)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   382
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   383
14218
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   384
(*<*) 
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   385
subsection{*Messages signed by CA*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   386
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   387
text{*Message @{text SET_CR2}: C can check CA's signature if he has received
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   388
     CA's certificate.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   389
lemma CA_Says_2_lemma:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   390
     "[| Crypt (priSK (CA i)) (Hash{|Agent C, Nonce NC1|})
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   391
           \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   392
         evs \<in> set_cr; (CA i) \<notin> bad |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   393
     ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i)) {|Agent C, Nonce NC1|}, Y|}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   394
                 \<in> set evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   395
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   396
apply (erule set_cr.induct, auto)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   397
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   398
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   399
text{*Ever used?*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   400
lemma CA_Says_2:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   401
     "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC1|})
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   402
           \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   403
         cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   404
         evs \<in> set_cr; (CA i) \<notin> bad |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   405
      ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i)) {|Agent C, Nonce NC1|}, Y|}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   406
                  \<in> set evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   407
by (blast dest!: certificate_valid_pubSK intro!: CA_Says_2_lemma)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   408
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   409
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   410
text{*Message @{text SET_CR4}: C can check CA's signature if he has received
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   411
      CA's certificate.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   412
lemma CA_Says_4_lemma:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   413
     "[| Crypt (priSK (CA i)) (Hash{|Agent C, Nonce NC2, Nonce NCA|})
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   414
           \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   415
         evs \<in> set_cr; (CA i) \<notin> bad |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   416
      ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   417
                     {|Agent C, Nonce NC2, Nonce NCA|}, Y|} \<in> set evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   418
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   419
apply (erule set_cr.induct, auto)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   420
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   421
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   422
text{*NEVER USED*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   423
lemma CA_Says_4:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   424
     "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC2, Nonce NCA|})
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   425
           \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   426
         cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   427
         evs \<in> set_cr; (CA i) \<notin> bad |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   428
      ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   429
                   {|Agent C, Nonce NC2, Nonce NCA|}, Y|} \<in> set evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   430
by (blast dest!: certificate_valid_pubSK intro!: CA_Says_4_lemma)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   431
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   432
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   433
text{*Message @{text SET_CR6}: C can check CA's signature if he has
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   434
      received CA's certificate.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   435
lemma CA_Says_6_lemma:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   436
     "[| Crypt (priSK (CA i)) 
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   437
               (Hash{|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|})
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   438
           \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   439
         evs \<in> set_cr; (CA i) \<notin> bad |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   440
      ==> \<exists>Y K. Says (CA i) C (Crypt K {|sign (priSK (CA i))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   441
      {|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|}, Y|}) \<in> set evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   442
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   443
apply (erule set_cr.induct, auto)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   444
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   445
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   446
text{*NEVER USED*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   447
lemma CA_Says_6:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   448
     "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|})
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   449
           \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   450
         cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   451
         evs \<in> set_cr; (CA i) \<notin> bad |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   452
      ==> \<exists>Y K. Says (CA i) C (Crypt K {|sign (priSK (CA i))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   453
                    {|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|}, Y|}) \<in> set evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   454
by (blast dest!: certificate_valid_pubSK intro!: CA_Says_6_lemma)
14218
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   455
(*>*)
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   456
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   457
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   458
subsection{*Useful lemmas *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   459
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   460
text{*Rewriting rule for private encryption keys.  Analogous rewriting rules
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   461
for other keys aren't needed.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   462
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   463
lemma parts_image_priEK:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   464
     "[|Key (priEK C) \<in> parts (Key`KK Un (knows Spy evs));
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   465
        evs \<in> set_cr|] ==> priEK C \<in> KK | C \<in> bad"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   466
by auto
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   467
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   468
text{*trivial proof because (priEK C) never appears even in (parts evs)*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   469
lemma analz_image_priEK:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   470
     "evs \<in> set_cr ==>
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   471
          (Key (priEK C) \<in> analz (Key`KK Un (knows Spy evs))) =
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   472
          (priEK C \<in> KK | C \<in> bad)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   473
by (blast dest!: parts_image_priEK intro: analz_mono [THEN [2] rev_subsetD])
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   474
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   475
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   476
subsection{*Secrecy of Session Keys *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   477
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   478
subsubsection{*Lemmas about the predicate KeyCryptKey *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   479
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   480
text{*A fresh DK cannot be associated with any other
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   481
  (with respect to a given trace). *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   482
lemma DK_fresh_not_KeyCryptKey:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   483
     "[| Key DK \<notin> used evs; evs \<in> set_cr |] ==> ~ KeyCryptKey DK K evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   484
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   485
apply (erule set_cr.induct)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   486
apply (simp_all (no_asm_simp))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   487
apply (blast dest: Crypt_analz_imp_used)+
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   488
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   489
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   490
text{*A fresh K cannot be associated with any other.  The assumption that
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   491
  DK isn't a private encryption key may be an artifact of the particular
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   492
  definition of KeyCryptKey.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   493
lemma K_fresh_not_KeyCryptKey:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   494
     "[|\<forall>C. DK \<noteq> priEK C; Key K \<notin> used evs|] ==> ~ KeyCryptKey DK K evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   495
apply (induct evs)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   496
apply (auto simp add: parts_insert2 split add: event.split)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   497
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   498
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   499
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   500
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
   501
  be known to the Spy, by @{term Spy_see_private_Key}*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   502
lemma cardSK_neq_priEK:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   503
     "[|Key cardSK \<notin> analz (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   504
        Key cardSK : parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   505
        evs \<in> set_cr|] ==> cardSK \<noteq> priEK C"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   506
by blast
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   507
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   508
lemma not_KeyCryptKey_cardSK [rule_format (no_asm)]:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   509
     "[|cardSK \<notin> symKeys;  \<forall>C. cardSK \<noteq> priEK C;  evs \<in> set_cr|] ==>
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   510
      Key cardSK \<notin> analz (knows Spy evs) --> ~ KeyCryptKey cardSK K evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   511
by (erule set_cr.induct, analz_mono_contra, auto)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   512
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   513
text{*Lemma for message 5: pubSK C is never used to encrypt Keys.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   514
lemma pubSK_not_KeyCryptKey [simp]: "~ KeyCryptKey (pubSK C) K evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   515
apply (induct_tac "evs")
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   516
apply (auto simp add: parts_insert2 split add: event.split)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   517
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   518
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   519
text{*Lemma for message 6: either cardSK is compromised (when we don't care)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   520
  or else cardSK hasn't been used to encrypt K.  Previously we treated
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   521
  message 5 in the same way, but the current model assumes that rule
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   522
  @{text SET_CR5} is executed only by honest agents.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   523
lemma msg6_KeyCryptKey_disj:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   524
     "[|Gets B {|Crypt KC3 {|Agent C, Nonce N, Key KC2, Key cardSK, X|}, Y|}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   525
          \<in> set evs;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   526
        cardSK \<notin> symKeys;  evs \<in> set_cr|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   527
      ==> Key cardSK \<in> analz (knows Spy evs) |
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   528
          (\<forall>K. ~ KeyCryptKey cardSK K evs)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   529
by (blast dest: not_KeyCryptKey_cardSK intro: cardSK_neq_priEK)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   530
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   531
text{*As usual: we express the property as a logical equivalence*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   532
lemma Key_analz_image_Key_lemma:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   533
     "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
   534
      ==>
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   535
      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
   536
by (blast intro: analz_mono [THEN [2] rev_subsetD])
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   537
24123
a0fc58900606 tuned ML bindings (for multithreading);
wenzelm
parents: 23755
diff changeset
   538
method_setup valid_certificate_tac = {*
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 24123
diff changeset
   539
  Args.goal_spec >> (fn quant => K (SIMPLE_METHOD'' quant
d2d7874648bd simplified method setup;
wenzelm
parents: 24123
diff changeset
   540
    (fn i =>
d2d7874648bd simplified method setup;
wenzelm
parents: 24123
diff changeset
   541
      EVERY [ftac @{thm Gets_certificate_valid} i,
d2d7874648bd simplified method setup;
wenzelm
parents: 24123
diff changeset
   542
             assume_tac i,
d2d7874648bd simplified method setup;
wenzelm
parents: 24123
diff changeset
   543
             etac conjE i, REPEAT (hyp_subst_tac i)])))
42814
5af15f1e2ef6 simplified/unified method_setup/attribute_setup;
wenzelm
parents: 39758
diff changeset
   544
*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   545
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   546
text{*The @{text "(no_asm)"} attribute is essential, since it retains
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   547
  the quantifier and allows the simprule's condition to itself be simplified.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   548
lemma symKey_compromise [rule_format (no_asm)]:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   549
     "evs \<in> set_cr ==>
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   550
      (\<forall>SK KK. SK \<in> symKeys \<longrightarrow> (\<forall>K \<in> KK. ~ KeyCryptKey K SK evs)   -->
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   551
               (Key SK \<in> analz (Key`KK Un (knows Spy evs))) =
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   552
               (SK \<in> KK | Key SK \<in> analz (knows Spy evs)))"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   553
apply (erule set_cr.induct)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   554
apply (rule_tac [!] allI) +
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   555
apply (rule_tac [!] impI [THEN Key_analz_image_Key_lemma, THEN impI])+
24123
a0fc58900606 tuned ML bindings (for multithreading);
wenzelm
parents: 23755
diff changeset
   556
apply (valid_certificate_tac [8]) --{*for message 5*}
a0fc58900606 tuned ML bindings (for multithreading);
wenzelm
parents: 23755
diff changeset
   557
apply (valid_certificate_tac [6]) --{*for message 5*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   558
apply (erule_tac [9] msg6_KeyCryptKey_disj [THEN disjE])
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   559
apply (simp_all
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   560
         del: image_insert image_Un imp_disjL
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   561
         add: analz_image_keys_simps analz_knows_absorb
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   562
              analz_Key_image_insert_eq notin_image_iff
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   563
              K_fresh_not_KeyCryptKey
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   564
              DK_fresh_not_KeyCryptKey ball_conj_distrib
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   565
              analz_image_priEK disj_simps)
24123
a0fc58900606 tuned ML bindings (for multithreading);
wenzelm
parents: 23755
diff changeset
   566
  --{*9 seconds on a 1.6GHz machine*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   567
apply spy_analz
14218
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   568
apply blast  --{*3*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   569
apply blast  --{*5*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   570
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   571
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   572
text{*The remaining quantifiers seem to be essential.
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   573
  NO NEED to assume the cardholder's OK: bad cardholders don't do anything
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   574
  wrong!!*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   575
lemma symKey_secrecy [rule_format]:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   576
     "[|CA i \<notin> bad;  K \<in> symKeys;  evs \<in> set_cr|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   577
      ==> \<forall>X c. Says (Cardholder c) (CA i) X \<in> set evs -->
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   578
                Key K \<in> parts{X} -->
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   579
                Cardholder c \<notin> bad -->
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   580
                Key K \<notin> analz (knows Spy evs)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   581
apply (erule set_cr.induct)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   582
apply (frule_tac [8] Gets_certificate_valid) --{*for message 5*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   583
apply (frule_tac [6] Gets_certificate_valid) --{*for message 3*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   584
apply (erule_tac [11] msg6_KeyCryptKey_disj [THEN disjE])
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   585
apply (simp_all del: image_insert image_Un imp_disjL
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   586
         add: symKey_compromise fresh_notin_analz_knows_Spy
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   587
              analz_image_keys_simps analz_knows_absorb
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   588
              analz_Key_image_insert_eq notin_image_iff
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   589
              K_fresh_not_KeyCryptKey
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   590
              DK_fresh_not_KeyCryptKey
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   591
              analz_image_priEK)
24123
a0fc58900606 tuned ML bindings (for multithreading);
wenzelm
parents: 23755
diff changeset
   592
  --{*2.5 seconds on a 1.6GHz machine*}
14218
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   593
apply spy_analz  --{*Fake*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   594
apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   595
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   596
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   597
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   598
subsection{*Primary Goals of Cardholder Registration *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   599
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   600
text{*The cardholder's certificate really was created by the CA, provided the
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   601
    CA is uncompromised *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   602
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   603
text{*Lemma concerning the actual signed message digest*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   604
lemma cert_valid_lemma:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   605
     "[|Crypt (priSK (CA i)) {|Hash {|Nonce N, Pan(pan C)|}, Key cardSK, N1|}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   606
          \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   607
        CA i \<notin> bad; evs \<in> set_cr|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   608
  ==> \<exists>KC2 X Y. Says (CA i) C
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   609
                     (Crypt KC2 
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   610
                       {|X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y|})
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   611
                  \<in> set evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   612
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   613
apply (erule set_cr.induct)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   614
apply (simp_all (no_asm_simp))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   615
apply auto
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   616
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   617
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   618
text{*Pre-packaged version for cardholder.  We don't try to confirm the values
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   619
  of KC2, X and Y, since they are not important.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   620
lemma certificate_valid_cardSK:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   621
    "[|Gets C (Crypt KC2 {|X, certC (pan C) cardSK N onlySig (invKey SKi),
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   622
                              cert (CA i) SKi onlySig (priSK RCA)|}) \<in> set evs;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   623
        CA i \<notin> bad; evs \<in> set_cr|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   624
  ==> \<exists>KC2 X Y. Says (CA i) C
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   625
                     (Crypt KC2 
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   626
                       {|X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y|})
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   627
                   \<in> set evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   628
by (force dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Body]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   629
                    certificate_valid_pubSK cert_valid_lemma)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   630
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   631
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   632
lemma Hash_imp_parts [rule_format]:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   633
     "evs \<in> set_cr
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   634
      ==> Hash{|X, Nonce N|} \<in> parts (knows Spy evs) -->
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   635
          Nonce N \<in> parts (knows Spy evs)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   636
apply (erule set_cr.induct, force)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   637
apply (simp_all (no_asm_simp))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   638
apply (blast intro: parts_mono [THEN [2] rev_subsetD])
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   639
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   640
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   641
lemma Hash_imp_parts2 [rule_format]:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   642
     "evs \<in> set_cr
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   643
      ==> Hash{|X, Nonce M, Y, Nonce N|} \<in> parts (knows Spy evs) -->
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   644
          Nonce M \<in> parts (knows Spy evs) & Nonce N \<in> parts (knows Spy evs)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   645
apply (erule set_cr.induct, force)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   646
apply (simp_all (no_asm_simp))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   647
apply (blast intro: parts_mono [THEN [2] rev_subsetD])
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   648
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   649
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   650
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   651
subsection{*Secrecy of Nonces*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   652
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   653
subsubsection{*Lemmas about the predicate KeyCryptNonce *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   654
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   655
text{*A fresh DK cannot be associated with any other
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   656
  (with respect to a given trace). *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   657
lemma DK_fresh_not_KeyCryptNonce:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   658
     "[| DK \<in> symKeys; Key DK \<notin> used evs; evs \<in> set_cr |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   659
      ==> ~ KeyCryptNonce DK K evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   660
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   661
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   662
apply (erule set_cr.induct)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   663
apply (simp_all (no_asm_simp))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   664
apply blast
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   665
apply blast
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   666
apply (auto simp add: DK_fresh_not_KeyCryptKey)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   667
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   668
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   669
text{*A fresh N cannot be associated with any other
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   670
      (with respect to a given trace). *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   671
lemma N_fresh_not_KeyCryptNonce:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   672
     "\<forall>C. DK \<noteq> priEK C ==> Nonce N \<notin> used evs --> ~ KeyCryptNonce DK N evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   673
apply (induct_tac "evs")
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   674
apply (case_tac [2] "a")
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   675
apply (auto simp add: parts_insert2)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   676
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   677
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   678
lemma not_KeyCryptNonce_cardSK [rule_format (no_asm)]:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   679
     "[|cardSK \<notin> symKeys;  \<forall>C. cardSK \<noteq> priEK C;  evs \<in> set_cr|] ==>
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   680
      Key cardSK \<notin> analz (knows Spy evs) --> ~ KeyCryptNonce cardSK N evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   681
apply (erule set_cr.induct, analz_mono_contra, simp_all)
14218
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   682
apply (blast dest: not_KeyCryptKey_cardSK)  --{*6*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   683
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   684
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   685
subsubsection{*Lemmas for message 5 and 6:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   686
  either cardSK is compromised (when we don't care)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   687
  or else cardSK hasn't been used to encrypt K. *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   688
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   689
text{*Lemma for message 5: pubSK C is never used to encrypt Nonces.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   690
lemma pubSK_not_KeyCryptNonce [simp]: "~ KeyCryptNonce (pubSK C) N evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   691
apply (induct_tac "evs")
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   692
apply (auto simp add: parts_insert2 split add: event.split)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   693
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   694
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   695
text{*Lemma for message 6: either cardSK is compromised (when we don't care)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   696
  or else cardSK hasn't been used to encrypt K.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   697
lemma msg6_KeyCryptNonce_disj:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   698
     "[|Gets B {|Crypt KC3 {|Agent C, Nonce N, Key KC2, Key cardSK, X|}, Y|}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   699
          \<in> set evs;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   700
        cardSK \<notin> symKeys;  evs \<in> set_cr|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   701
      ==> Key cardSK \<in> analz (knows Spy evs) |
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   702
          ((\<forall>K. ~ KeyCryptKey cardSK K evs) &
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   703
           (\<forall>N. ~ KeyCryptNonce cardSK N evs))"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   704
by (blast dest: not_KeyCryptKey_cardSK not_KeyCryptNonce_cardSK
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   705
          intro: cardSK_neq_priEK)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   706
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   707
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   708
text{*As usual: we express the property as a logical equivalence*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   709
lemma Nonce_analz_image_Key_lemma:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   710
     "P --> (Nonce N \<in> analz (Key`KK Un H)) --> (Nonce N \<in> analz H)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   711
      ==> P --> (Nonce N \<in> analz (Key`KK Un H)) = (Nonce N \<in> analz H)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   712
by (blast intro: analz_mono [THEN [2] rev_subsetD])
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   713
32404
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 30607
diff changeset
   714
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   715
text{*The @{text "(no_asm)"} attribute is essential, since it retains
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   716
  the quantifier and allows the simprule's condition to itself be simplified.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   717
lemma Nonce_compromise [rule_format (no_asm)]:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   718
     "evs \<in> set_cr ==>
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   719
      (\<forall>N KK. (\<forall>K \<in> KK. ~ KeyCryptNonce K N evs)   -->
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   720
               (Nonce N \<in> analz (Key`KK Un (knows Spy evs))) =
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   721
               (Nonce N \<in> analz (knows Spy evs)))"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   722
apply (erule set_cr.induct)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   723
apply (rule_tac [!] allI)+
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   724
apply (rule_tac [!] impI [THEN Nonce_analz_image_Key_lemma])+
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   725
apply (frule_tac [8] Gets_certificate_valid) --{*for message 5*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   726
apply (frule_tac [6] Gets_certificate_valid) --{*for message 3*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   727
apply (frule_tac [11] msg6_KeyCryptNonce_disj)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   728
apply (erule_tac [13] disjE)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   729
apply (simp_all del: image_insert image_Un
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   730
         add: symKey_compromise
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   731
              analz_image_keys_simps analz_knows_absorb
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   732
              analz_Key_image_insert_eq notin_image_iff
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   733
              N_fresh_not_KeyCryptNonce
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   734
              DK_fresh_not_KeyCryptNonce K_fresh_not_KeyCryptKey
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   735
              ball_conj_distrib analz_image_priEK)
24123
a0fc58900606 tuned ML bindings (for multithreading);
wenzelm
parents: 23755
diff changeset
   736
  --{*14 seconds on a 1.6GHz machine*}
14218
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   737
apply spy_analz  --{*Fake*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   738
apply blast  --{*3*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   739
apply blast  --{*5*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   740
txt{*Message 6*}
32404
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 30607
diff changeset
   741
apply (metis symKey_compromise)
14218
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   742
  --{*cardSK compromised*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   743
txt{*Simplify again--necessary because the previous simplification introduces
32404
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 30607
diff changeset
   744
  some logical connectives*} 
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 30607
diff changeset
   745
apply (force simp del: image_insert image_Un imp_disjL
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   746
          simp add: analz_image_keys_simps symKey_compromise)
14218
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   747
done
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   748
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   749
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   750
subsection{*Secrecy of CardSecret: the Cardholder's secret*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   751
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   752
lemma NC2_not_CardSecret:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   753
     "[|Crypt EKj {|Key K, Pan p, Hash {|Agent D, Nonce N|}|}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   754
          \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   755
        Key K \<notin> analz (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   756
        Nonce N \<notin> analz (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   757
       evs \<in> set_cr|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   758
      ==> Crypt EKi {|Key K', Pan p', Nonce N|} \<notin> parts (knows Spy evs)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   759
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   760
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   761
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   762
apply (erule set_cr.induct, analz_mono_contra, simp_all)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   763
apply (blast dest: Hash_imp_parts)+
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   764
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   765
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   766
lemma KC2_secure_lemma [rule_format]:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   767
     "[|U = Crypt KC3 {|Agent C, Nonce N, Key KC2, X|};
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   768
        U \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   769
        evs \<in> set_cr|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   770
  ==> Nonce N \<notin> analz (knows Spy evs) -->
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   771
      (\<exists>k i W. Says (Cardholder k) (CA i) {|U,W|} \<in> set evs & 
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   772
               Cardholder k \<notin> bad & CA i \<notin> bad)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   773
apply (erule_tac P = "U \<in> ?H" in rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   774
apply (erule set_cr.induct)
24123
a0fc58900606 tuned ML bindings (for multithreading);
wenzelm
parents: 23755
diff changeset
   775
apply (valid_certificate_tac [8])  --{*for message 5*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   776
apply (simp_all del: image_insert image_Un imp_disjL
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   777
         add: analz_image_keys_simps analz_knows_absorb
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   778
              analz_knows_absorb2 notin_image_iff)
24123
a0fc58900606 tuned ML bindings (for multithreading);
wenzelm
parents: 23755
diff changeset
   779
  --{*4 seconds on a 1.6GHz machine*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   780
apply (simp_all (no_asm_simp)) --{*leaves 4 subgoals*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   781
apply (blast intro!: analz_insertI)+
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   782
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   783
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   784
lemma KC2_secrecy:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   785
     "[|Gets B {|Crypt K {|Agent C, Nonce N, Key KC2, X|}, Y|} \<in> set evs;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   786
        Nonce N \<notin> analz (knows Spy evs);  KC2 \<in> symKeys;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   787
        evs \<in> set_cr|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   788
       ==> Key KC2 \<notin> analz (knows Spy evs)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   789
by (force dest!: refl [THEN KC2_secure_lemma] symKey_secrecy)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   790
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   791
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   792
text{*Inductive version*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   793
lemma CardSecret_secrecy_lemma [rule_format]:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   794
     "[|CA i \<notin> bad;  evs \<in> set_cr|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   795
      ==> Key K \<notin> analz (knows Spy evs) -->
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   796
          Crypt (pubEK (CA i)) {|Key K, Pan p, Nonce CardSecret|}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   797
             \<in> parts (knows Spy evs) -->
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   798
          Nonce CardSecret \<notin> analz (knows Spy evs)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   799
apply (erule set_cr.induct, analz_mono_contra)
24123
a0fc58900606 tuned ML bindings (for multithreading);
wenzelm
parents: 23755
diff changeset
   800
apply (valid_certificate_tac [8]) --{*for message 5*}
a0fc58900606 tuned ML bindings (for multithreading);
wenzelm
parents: 23755
diff changeset
   801
apply (valid_certificate_tac [6]) --{*for message 5*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   802
apply (frule_tac [9] msg6_KeyCryptNonce_disj [THEN disjE])
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   803
apply (simp_all
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   804
         del: image_insert image_Un imp_disjL
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   805
         add: analz_image_keys_simps analz_knows_absorb
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   806
              analz_Key_image_insert_eq notin_image_iff
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   807
              EXHcrypt_def Crypt_notin_image_Key
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   808
              N_fresh_not_KeyCryptNonce DK_fresh_not_KeyCryptNonce
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   809
              ball_conj_distrib Nonce_compromise symKey_compromise
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   810
              analz_image_priEK)
24123
a0fc58900606 tuned ML bindings (for multithreading);
wenzelm
parents: 23755
diff changeset
   811
  --{*2.5 seconds on a 1.6GHz machine*}
14218
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   812
apply spy_analz  --{*Fake*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   813
apply (simp_all (no_asm_simp))
14218
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   814
apply blast  --{*1*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   815
apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])  --{*2*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   816
apply blast  --{*3*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   817
apply (blast dest: NC2_not_CardSecret Gets_imp_knows_Spy [THEN analz.Inj] analz_symKeys_Decrypt)  --{*4*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   818
apply blast  --{*5*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   819
apply (blast dest: KC2_secrecy)+  --{*Message 6: two cases*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   820
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   821
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   822
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   823
text{*Packaged version for cardholder*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   824
lemma CardSecret_secrecy:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   825
     "[|Cardholder k \<notin> bad;  CA i \<notin> bad;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   826
        Says (Cardholder k) (CA i)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   827
           {|X, Crypt EKi {|Key KC3, Pan p, Nonce CardSecret|}|} \<in> set evs;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   828
        Gets A {|Z, cert (CA i) EKi onlyEnc (priSK RCA),
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   829
                    cert (CA i) SKi onlySig (priSK RCA)|} \<in> set evs;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   830
        KC3 \<in> symKeys;  evs \<in> set_cr|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   831
      ==> Nonce CardSecret \<notin> analz (knows Spy evs)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   832
apply (frule Gets_certificate_valid, assumption)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   833
apply (subgoal_tac "Key KC3 \<notin> analz (knows Spy evs) ")
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   834
apply (blast dest: CardSecret_secrecy_lemma)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   835
apply (rule symKey_secrecy)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   836
apply (auto simp add: parts_insert2)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   837
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   838
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   839
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   840
subsection{*Secrecy of NonceCCA [the CA's secret] *}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   841
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   842
lemma NC2_not_NonceCCA:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   843
     "[|Hash {|Agent C', Nonce N', Agent C, Nonce N|}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   844
          \<in> parts (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   845
        Nonce N \<notin> analz (knows Spy evs);
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   846
       evs \<in> set_cr|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   847
      ==> Crypt KC1 {|{|Agent B, Nonce N|}, Hash p|} \<notin> parts (knows Spy evs)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   848
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   849
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   850
apply (erule set_cr.induct, analz_mono_contra, simp_all)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   851
apply (blast dest: Hash_imp_parts2)+
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   852
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   853
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   854
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   855
text{*Inductive version*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   856
lemma NonceCCA_secrecy_lemma [rule_format]:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   857
     "[|CA i \<notin> bad;  evs \<in> set_cr|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   858
      ==> Key K \<notin> analz (knows Spy evs) -->
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   859
          Crypt K
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   860
            {|sign (priSK (CA i))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   861
                   {|Agent C, Nonce N, Agent(CA i), Nonce NonceCCA|},
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   862
              X, Y|}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   863
             \<in> parts (knows Spy evs) -->
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   864
          Nonce NonceCCA \<notin> analz (knows Spy evs)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   865
apply (erule set_cr.induct, analz_mono_contra)
24123
a0fc58900606 tuned ML bindings (for multithreading);
wenzelm
parents: 23755
diff changeset
   866
apply (valid_certificate_tac [8]) --{*for message 5*}
a0fc58900606 tuned ML bindings (for multithreading);
wenzelm
parents: 23755
diff changeset
   867
apply (valid_certificate_tac [6]) --{*for message 5*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   868
apply (frule_tac [9] msg6_KeyCryptNonce_disj [THEN disjE])
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   869
apply (simp_all
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   870
         del: image_insert image_Un imp_disjL
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   871
         add: analz_image_keys_simps analz_knows_absorb sign_def
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   872
              analz_Key_image_insert_eq notin_image_iff
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   873
              EXHcrypt_def Crypt_notin_image_Key
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   874
              N_fresh_not_KeyCryptNonce DK_fresh_not_KeyCryptNonce
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   875
              ball_conj_distrib Nonce_compromise symKey_compromise
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   876
              analz_image_priEK)
24123
a0fc58900606 tuned ML bindings (for multithreading);
wenzelm
parents: 23755
diff changeset
   877
  --{*3 seconds on a 1.6GHz machine*}
14218
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   878
apply spy_analz  --{*Fake*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   879
apply blast  --{*1*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   880
apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])  --{*2*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   881
apply blast  --{*3*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   882
apply (blast dest: NC2_not_NonceCCA)  --{*4*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   883
apply blast  --{*5*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   884
apply (blast dest: KC2_secrecy)+  --{*Message 6: two cases*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   885
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   886
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   887
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   888
text{*Packaged version for cardholder*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   889
lemma NonceCCA_secrecy:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   890
     "[|Cardholder k \<notin> bad;  CA i \<notin> bad;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   891
        Gets (Cardholder k)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   892
           (Crypt KC2
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   893
            {|sign (priSK (CA i)) {|Agent C, Nonce N, Agent(CA i), Nonce NonceCCA|},
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   894
              X, Y|}) \<in> set evs;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   895
        Says (Cardholder k) (CA i)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   896
           {|Crypt KC3 {|Agent C, Nonce NC3, Key KC2, X'|}, Y'|} \<in> set evs;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   897
        Gets A {|Z, cert (CA i) EKi onlyEnc (priSK RCA),
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   898
                    cert (CA i) SKi onlySig (priSK RCA)|} \<in> set evs;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   899
        KC2 \<in> symKeys;  evs \<in> set_cr|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   900
      ==> Nonce NonceCCA \<notin> analz (knows Spy evs)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   901
apply (frule Gets_certificate_valid, assumption)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   902
apply (subgoal_tac "Key KC2 \<notin> analz (knows Spy evs) ")
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   903
apply (blast dest: NonceCCA_secrecy_lemma)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   904
apply (rule symKey_secrecy)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   905
apply (auto simp add: parts_insert2)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   906
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   907
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   908
text{*We don't bother to prove guarantees for the CA.  He doesn't care about
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   909
  the PANSecret: it isn't his credit card!*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   910
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   911
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   912
subsection{*Rewriting Rule for PANs*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   913
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   914
text{*Lemma for message 6: either cardSK isn't a CA's private encryption key,
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   915
  or if it is then (because it appears in traffic) that CA is bad,
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   916
  and so the Spy knows that key already.  Either way, we can simplify
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   917
  the expression @{term "analz (insert (Key cardSK) X)"}.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   918
lemma msg6_cardSK_disj:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   919
     "[|Gets A {|Crypt K {|c, n, k', Key cardSK, X|}, Y|}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   920
          \<in> set evs;  evs \<in> set_cr |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   921
      ==> cardSK \<notin> range(invKey o pubEK o CA) | Key cardSK \<in> knows Spy evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   922
by auto
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   923
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   924
lemma analz_image_pan_lemma:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   925
     "(Pan P \<in> analz (Key`nE Un H)) --> (Pan P \<in> analz H)  ==>
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   926
      (Pan P \<in> analz (Key`nE Un H)) =   (Pan P \<in> analz H)"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   927
by (blast intro: analz_mono [THEN [2] rev_subsetD])
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   928
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   929
lemma analz_image_pan [rule_format]:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   930
     "evs \<in> set_cr ==>
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   931
       \<forall>KK. KK <= - invKey ` pubEK ` range CA -->
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   932
            (Pan P \<in> analz (Key`KK Un (knows Spy evs))) =
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   933
            (Pan P \<in> analz (knows Spy evs))"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   934
apply (erule set_cr.induct)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   935
apply (rule_tac [!] allI impI)+
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   936
apply (rule_tac [!] analz_image_pan_lemma)
24123
a0fc58900606 tuned ML bindings (for multithreading);
wenzelm
parents: 23755
diff changeset
   937
apply (valid_certificate_tac [8]) --{*for message 5*}
a0fc58900606 tuned ML bindings (for multithreading);
wenzelm
parents: 23755
diff changeset
   938
apply (valid_certificate_tac [6]) --{*for message 5*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   939
apply (erule_tac [9] msg6_cardSK_disj [THEN disjE])
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   940
apply (simp_all
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   941
         del: image_insert image_Un
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   942
         add: analz_image_keys_simps disjoint_image_iff
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   943
              notin_image_iff analz_image_priEK)
24123
a0fc58900606 tuned ML bindings (for multithreading);
wenzelm
parents: 23755
diff changeset
   944
  --{*6 seconds on a 1.6GHz machine*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   945
apply spy_analz
14218
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   946
apply (simp add: insert_absorb)  --{*6*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   947
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   948
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   949
lemma analz_insert_pan:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   950
     "[| evs \<in> set_cr;  K \<notin> invKey ` pubEK ` range CA |] ==>
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   951
          (Pan P \<in> analz (insert (Key K) (knows Spy evs))) =
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   952
          (Pan P \<in> analz (knows Spy evs))"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   953
by (simp del: image_insert image_Un
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   954
         add: analz_image_keys_simps analz_image_pan)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   955
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   956
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   957
text{*Confidentiality of the PAN\@.  Maybe we could combine the statements of
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   958
  this theorem with @{term analz_image_pan}, requiring a single induction but
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   959
  a much more difficult proof.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   960
lemma pan_confidentiality:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   961
     "[| Pan (pan C) \<in> analz(knows Spy evs); C \<noteq>Spy; evs :set_cr|]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   962
    ==> \<exists>i X K HN.
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   963
        Says C (CA i) {|X, Crypt (pubEK (CA i)) {|Key K, Pan (pan C), HN|} |}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   964
           \<in> set evs
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   965
      & (CA i) \<in> bad"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   966
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   967
apply (erule set_cr.induct)
24123
a0fc58900606 tuned ML bindings (for multithreading);
wenzelm
parents: 23755
diff changeset
   968
apply (valid_certificate_tac [8]) --{*for message 5*}
a0fc58900606 tuned ML bindings (for multithreading);
wenzelm
parents: 23755
diff changeset
   969
apply (valid_certificate_tac [6]) --{*for message 5*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   970
apply (erule_tac [9] msg6_cardSK_disj [THEN disjE])
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   971
apply (simp_all
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   972
         del: image_insert image_Un
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   973
         add: analz_image_keys_simps analz_insert_pan analz_image_pan
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   974
              notin_image_iff analz_image_priEK)
24123
a0fc58900606 tuned ML bindings (for multithreading);
wenzelm
parents: 23755
diff changeset
   975
  --{*3.5 seconds on a 1.6GHz machine*}
14218
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   976
apply spy_analz  --{*fake*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   977
apply blast  --{*3*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   978
apply blast  --{*5*}
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
   979
apply (simp (no_asm_simp) add: insert_absorb)  --{*6*}
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   980
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   981
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   982
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   983
subsection{*Unicity*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   984
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   985
lemma CR6_Says_imp_Notes:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   986
     "[|Says (CA i) C (Crypt KC2
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   987
          {|sign (priSK (CA i)) {|Agent C, Nonce NC3, Agent (CA i), Nonce Y|},
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   988
            certC (pan C) cardSK X onlySig (priSK (CA i)),
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   989
            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})  \<in> set evs;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   990
        evs \<in> set_cr |]
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   991
      ==> Notes (CA i) (Key cardSK) \<in> set evs"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   992
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   993
apply (erule set_cr.induct)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   994
apply (simp_all (no_asm_simp))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   995
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   996
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   997
text{*Unicity of cardSK: it uniquely identifies the other components.  
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   998
      This holds because a CA accepts a cardSK at most once.*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
   999
lemma cardholder_key_unicity:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1000
     "[|Says (CA i) C (Crypt KC2
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1001
          {|sign (priSK (CA i)) {|Agent C, Nonce NC3, Agent (CA i), Nonce Y|},
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1002
            certC (pan C) cardSK X onlySig (priSK (CA i)),
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1003
            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1004
          \<in> set evs;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1005
        Says (CA i) C' (Crypt KC2'
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1006
          {|sign (priSK (CA i)) {|Agent C', Nonce NC3', Agent (CA i), Nonce Y'|},
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1007
            certC (pan C') cardSK X' onlySig (priSK (CA i)),
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1008
            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1009
          \<in> set evs;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1010
        evs \<in> set_cr |] ==> C=C' & NC3=NC3' & X=X' & KC2=KC2' & Y=Y'"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1011
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1012
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1013
apply (erule set_cr.induct)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1014
apply (simp_all (no_asm_simp))
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1015
apply (blast dest!: CR6_Says_imp_Notes)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1016
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1017
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1018
14218
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
  1019
(*<*)
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1020
text{*UNUSED unicity result*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1021
lemma unique_KC1:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1022
     "[|Says C B {|Crypt KC1 X, Crypt EK {|Key KC1, Y|}|}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1023
          \<in> set evs;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1024
        Says C B' {|Crypt KC1 X', Crypt EK' {|Key KC1, Y'|}|}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1025
          \<in> set evs;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1026
        C \<notin> bad;  evs \<in> set_cr|] ==> B'=B & Y'=Y"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1027
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1028
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1029
apply (erule set_cr.induct, auto)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1030
done
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1031
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1032
text{*UNUSED unicity result*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1033
lemma unique_KC2:
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1034
     "[|Says C B {|Crypt K {|Agent C, nn, Key KC2, X|}, Y|} \<in> set evs;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1035
        Says C B' {|Crypt K' {|Agent C, nn', Key KC2, X'|}, Y'|} \<in> set evs;
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1036
        C \<notin> bad;  evs \<in> set_cr|] ==> B'=B & X'=X"
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1037
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1038
apply (erule rev_mp)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1039
apply (erule set_cr.induct, auto)
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1040
done
14218
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
  1041
(*>*)
db95d1c2f51b removal of junk and improvement of the document
paulson
parents: 14206
diff changeset
  1042
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1043
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1044
text{*Cannot show cardSK to be secret because it isn't assumed to be fresh
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1045
  it could be a previously compromised cardSK [e.g. involving a bad CA]*}
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1046
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1047
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents:
diff changeset
  1048
end