src/HOL/Auth/KerberosV.thy
author blanchet
Tue, 20 Mar 2012 13:53:09 +0100
changeset 47050 7be54568efa1
parent 43587 0dd418de22ce
child 55417 01fbfb60c33e
permissions -rw-r--r--
optimized "metis" call
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37936
1e4c5015a72e updated some headers;
wenzelm
parents: 36866
diff changeset
     1
(*  Title:      HOL/Auth/KerberosV.thy
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
     2
    Author:     Giampaolo Bella, Catania University
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
     3
*)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
     4
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
     5
header{*The Kerberos Protocol, Version V*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
     6
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
     7
theory KerberosV imports Public begin
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
     8
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
     9
text{*The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    10
20768
1d478c2d621f replaced syntax/translations by abbreviation;
wenzelm
parents: 18886
diff changeset
    11
abbreviation
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20768
diff changeset
    12
  Kas :: agent where
20768
1d478c2d621f replaced syntax/translations by abbreviation;
wenzelm
parents: 18886
diff changeset
    13
  "Kas == Server"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    14
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20768
diff changeset
    15
abbreviation
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20768
diff changeset
    16
  Tgs :: agent where
20768
1d478c2d621f replaced syntax/translations by abbreviation;
wenzelm
parents: 18886
diff changeset
    17
  "Tgs == Friend 0"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    18
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    19
41774
13b97824aec6 modernized specifications;
wenzelm
parents: 37936
diff changeset
    20
axiomatization where
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    21
  Tgs_not_bad [iff]: "Tgs \<notin> bad"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    22
   --{*Tgs is secure --- we already know that Kas is secure*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    23
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 35416
diff changeset
    24
definition
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    25
 (* authKeys are those contained in an authTicket *)
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 35416
diff changeset
    26
    authKeys :: "event list => key set" where
426d5781bb25 modernized specifications;
wenzelm
parents: 35416
diff changeset
    27
    "authKeys evs = {authK. \<exists>A Peer Ta. 
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    28
        Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Peer, Ta\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    29
                     Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key authK, Ta\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    30
                   \<rbrace> \<in> set evs}"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    31
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 35416
diff changeset
    32
definition
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    33
 (* A is the true creator of X if she has sent X and X never appeared on
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    34
    the trace before this event. Recall that traces grow from head. *)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    35
  Issues :: "[agent, agent, msg, event list] => bool"
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 35416
diff changeset
    36
             ("_ Issues _ with _ on _") where
426d5781bb25 modernized specifications;
wenzelm
parents: 35416
diff changeset
    37
   "A Issues B with X on evs =
426d5781bb25 modernized specifications;
wenzelm
parents: 35416
diff changeset
    38
      (\<exists>Y. Says A B Y \<in> set evs \<and> X \<in> parts {Y} \<and>
426d5781bb25 modernized specifications;
wenzelm
parents: 35416
diff changeset
    39
        X \<notin> parts (spies (takeWhile (% z. z  \<noteq> Says A B Y) (rev evs))))"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    40
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    41
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    42
consts
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    43
    (*Duration of the authentication key*)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    44
    authKlife   :: nat
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    45
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    46
    (*Duration of the service key*)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    47
    servKlife   :: nat
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    48
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    49
    (*Duration of an authenticator*)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    50
    authlife   :: nat
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    51
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    52
    (*Upper bound on the time of reaction of a server*)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    53
    replylife   :: nat
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    54
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    55
specification (authKlife)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    56
  authKlife_LB [iff]: "2 \<le> authKlife"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    57
    by blast
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    58
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    59
specification (servKlife)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    60
  servKlife_LB [iff]: "2 + authKlife \<le> servKlife"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    61
    by blast
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    62
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    63
specification (authlife)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    64
  authlife_LB [iff]: "Suc 0 \<le> authlife"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    65
    by blast
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    66
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    67
specification (replylife)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    68
  replylife_LB [iff]: "Suc 0 \<le> replylife"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    69
    by blast
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    70
20768
1d478c2d621f replaced syntax/translations by abbreviation;
wenzelm
parents: 18886
diff changeset
    71
abbreviation
1d478c2d621f replaced syntax/translations by abbreviation;
wenzelm
parents: 18886
diff changeset
    72
  (*The current time is just the length of the trace!*)
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20768
diff changeset
    73
  CT :: "event list=>nat" where
20768
1d478c2d621f replaced syntax/translations by abbreviation;
wenzelm
parents: 18886
diff changeset
    74
  "CT == length"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    75
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20768
diff changeset
    76
abbreviation
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20768
diff changeset
    77
  expiredAK :: "[nat, event list] => bool" where
20768
1d478c2d621f replaced syntax/translations by abbreviation;
wenzelm
parents: 18886
diff changeset
    78
  "expiredAK T evs == authKlife + T < CT evs"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    79
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20768
diff changeset
    80
abbreviation
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20768
diff changeset
    81
  expiredSK :: "[nat, event list] => bool" where
20768
1d478c2d621f replaced syntax/translations by abbreviation;
wenzelm
parents: 18886
diff changeset
    82
  "expiredSK T evs == servKlife + T < CT evs"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    83
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20768
diff changeset
    84
abbreviation
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20768
diff changeset
    85
  expiredA :: "[nat, event list] => bool" where
20768
1d478c2d621f replaced syntax/translations by abbreviation;
wenzelm
parents: 18886
diff changeset
    86
  "expiredA T evs == authlife + T < CT evs"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    87
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20768
diff changeset
    88
abbreviation
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20768
diff changeset
    89
  valid :: "[nat, nat] => bool"  ("valid _ wrt _") where
20768
1d478c2d621f replaced syntax/translations by abbreviation;
wenzelm
parents: 18886
diff changeset
    90
  "valid T1 wrt T2 == T1 <= replylife + T2"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    91
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    92
(*---------------------------------------------------------------------*)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    93
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    94
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    95
(* Predicate formalising the association between authKeys and servKeys *)
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    96
definition AKcryptSK :: "[key, key, event list] => bool" where
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    97
  "AKcryptSK authK servK evs ==
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    98
     \<exists>A B tt.
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    99
       Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, tt\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   100
                    Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, tt\<rbrace> \<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   101
         \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   102
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   103
inductive_set kerbV :: "event list set"
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   104
  where
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   105
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   106
   Nil:  "[] \<in> kerbV"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   107
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   108
 | Fake: "\<lbrakk> evsf \<in> kerbV;  X \<in> synth (analz (spies evsf)) \<rbrakk>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   109
          \<Longrightarrow> Says Spy B X  # evsf \<in> kerbV"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   110
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   111
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   112
(*Authentication phase*)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   113
 | KV1:   "\<lbrakk> evs1 \<in> kerbV \<rbrakk>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   114
          \<Longrightarrow> Says A Kas \<lbrace>Agent A, Agent Tgs, Number (CT evs1)\<rbrace> # evs1
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   115
          \<in> kerbV"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   116
   (*Unlike version IV, authTicket is not re-encrypted*)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   117
 | KV2:  "\<lbrakk> evs2 \<in> kerbV; Key authK \<notin> used evs2; authK \<in> symKeys;
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   118
            Says A' Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs2 \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   119
          \<Longrightarrow> Says Kas A \<lbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   120
          Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number (CT evs2)\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   121
        Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number (CT evs2)\<rbrace> 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   122
                         \<rbrace> # evs2 \<in> kerbV"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   123
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   124
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   125
(* Authorisation phase *)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   126
 | KV3:  "\<lbrakk> evs3 \<in> kerbV; A \<noteq> Kas; A \<noteq> Tgs;
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   127
            Says A Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs3;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   128
            Says Kas' A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   129
                          authTicket\<rbrace> \<in> set evs3;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   130
            valid Ta wrt T1
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   131
         \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   132
          \<Longrightarrow> Says A Tgs \<lbrace>authTicket,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   133
                           (Crypt authK \<lbrace>Agent A, Number (CT evs3)\<rbrace>),
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   134
                           Agent B\<rbrace> # evs3 \<in> kerbV"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   135
   (*Unlike version IV, servTicket is not re-encrypted*)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   136
 | KV4:  "\<lbrakk> evs4 \<in> kerbV; Key servK \<notin> used evs4; servK \<in> symKeys;
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   137
            B \<noteq> Tgs;  authK \<in> symKeys;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   138
            Says A' Tgs \<lbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   139
             (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK,
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   140
                                 Number Ta\<rbrace>),
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   141
             (Crypt authK \<lbrace>Agent A, Number T2\<rbrace>), Agent B\<rbrace>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   142
                \<in> set evs4;
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   143
            \<not> expiredAK Ta evs4;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   144
            \<not> expiredA T2 evs4;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   145
            servKlife + (CT evs4) <= authKlife + Ta
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   146
         \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   147
          \<Longrightarrow> Says Tgs A \<lbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   148
             Crypt authK \<lbrace>Key servK, Agent B, Number (CT evs4)\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   149
   Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number (CT evs4)\<rbrace> 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   150
                          \<rbrace> # evs4 \<in> kerbV"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   151
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   152
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   153
(*Service phase*)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   154
 | KV5:  "\<lbrakk> evs5 \<in> kerbV; authK \<in> symKeys; servK \<in> symKeys;
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   155
            A \<noteq> Kas; A \<noteq> Tgs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   156
            Says A Tgs
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   157
                \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>,
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   158
                  Agent B\<rbrace>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   159
              \<in> set evs5;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   160
            Says Tgs' A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   161
                          servTicket\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   162
                \<in> set evs5;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   163
            valid Ts wrt T2 \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   164
          \<Longrightarrow> Says A B \<lbrace>servTicket,
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   165
                         Crypt servK \<lbrace>Agent A, Number (CT evs5)\<rbrace> \<rbrace>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   166
               # evs5 \<in> kerbV"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   167
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   168
  | KV6:  "\<lbrakk> evs6 \<in> kerbV; B \<noteq> Kas; B \<noteq> Tgs;
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   169
            Says A' B \<lbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   170
              (Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>),
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   171
              (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>)\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   172
            \<in> set evs6;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   173
            \<not> expiredSK Ts evs6;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   174
            \<not> expiredA T3 evs6
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   175
         \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   176
          \<Longrightarrow> Says B A (Crypt servK (Number Ta2))
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   177
               # evs6 \<in> kerbV"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   178
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   179
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   180
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   181
(* Leaking an authK... *)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   182
 | Oops1:"\<lbrakk> evsO1 \<in> kerbV;  A \<noteq> Spy;
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   183
             Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   184
                          authTicket\<rbrace>  \<in> set evsO1;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   185
              expiredAK Ta evsO1 \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   186
          \<Longrightarrow> Notes Spy \<lbrace>Agent A, Agent Tgs, Number Ta, Key authK\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   187
               # evsO1 \<in> kerbV"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   188
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   189
(*Leaking a servK... *)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   190
 | Oops2: "\<lbrakk> evsO2 \<in> kerbV;  A \<noteq> Spy;
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   191
              Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   192
                           servTicket\<rbrace>  \<in> set evsO2;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   193
              expiredSK Ts evsO2 \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   194
          \<Longrightarrow> Notes Spy \<lbrace>Agent A, Agent B, Number Ts, Key servK\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   195
               # evsO2 \<in> kerbV"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   196
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   197
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   198
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   199
declare Says_imp_knows_Spy [THEN parts.Inj, dest]
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   200
declare parts.Body [dest]
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   201
declare analz_into_parts [dest]
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   202
declare Fake_parts_insert_in_Un [dest]
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   203
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   204
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   205
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   206
subsection{*Lemmas about lists, for reasoning about  Issues*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   207
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   208
lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   209
apply (induct_tac "evs")
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   210
apply (induct_tac [2] "a", auto)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   211
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   212
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   213
lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   214
apply (induct_tac "evs")
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   215
apply (induct_tac [2] "a", auto)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   216
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   217
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   218
lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   219
          (if A:bad then insert X (spies evs) else spies evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   220
apply (induct_tac "evs")
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   221
apply (induct_tac [2] "a", auto)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   222
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   223
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   224
lemma spies_evs_rev: "spies evs = spies (rev evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   225
apply (induct_tac "evs")
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   226
apply (induct_tac [2] "a")
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   227
apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   228
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   229
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   230
lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono]
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   231
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   232
lemma spies_takeWhile: "spies (takeWhile P evs) <=  spies evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   233
apply (induct_tac "evs")
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   234
apply (induct_tac [2] "a", auto)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   235
txt{* Resembles @{text"used_subset_append"} in theory Event.*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   236
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   237
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   238
lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono]
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   239
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   240
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   241
subsection{*Lemmas about @{term authKeys}*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   242
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   243
lemma authKeys_empty: "authKeys [] = {}"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   244
  by (simp add: authKeys_def)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   245
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   246
lemma authKeys_not_insert:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   247
 "(\<forall>A Ta akey Peer.
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   248
   ev \<noteq> Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>akey, Agent Peer, Ta\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   249
                     Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, akey, Ta\<rbrace> \<rbrace>)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   250
       \<Longrightarrow> authKeys (ev # evs) = authKeys evs"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   251
  by (auto simp add: authKeys_def)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   252
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   253
lemma authKeys_insert:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   254
  "authKeys
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   255
     (Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent Peer, Number Ta\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   256
         Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K, Number Ta\<rbrace> \<rbrace> # evs)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   257
       = insert K (authKeys evs)"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   258
  by (auto simp add: authKeys_def)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   259
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   260
lemma authKeys_simp:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   261
   "K \<in> authKeys
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   262
    (Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key K', Agent Peer, Number Ta\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   263
        Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K', Number Ta\<rbrace> \<rbrace> # evs)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   264
        \<Longrightarrow> K = K' | K \<in> authKeys evs"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   265
  by (auto simp add: authKeys_def)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   266
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   267
lemma authKeysI:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   268
   "Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent Tgs, Number Ta\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   269
         Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key K, Number Ta\<rbrace> \<rbrace> \<in> set evs
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   270
        \<Longrightarrow> K \<in> authKeys evs"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   271
  by (auto simp add: authKeys_def)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   272
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   273
lemma authKeys_used: "K \<in> authKeys evs \<Longrightarrow> Key K \<in> used evs"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   274
  by (auto simp add: authKeys_def)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   275
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   276
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   277
subsection{*Forwarding Lemmas*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   278
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   279
lemma Says_ticket_parts:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   280
     "Says S A \<lbrace>Crypt K \<lbrace>SesKey, B, TimeStamp\<rbrace>, Ticket\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   281
               \<in> set evs \<Longrightarrow> Ticket \<in> parts (spies evs)"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   282
by blast
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   283
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   284
lemma Says_ticket_analz:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   285
     "Says S A \<lbrace>Crypt K \<lbrace>SesKey, B, TimeStamp\<rbrace>, Ticket\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   286
               \<in> set evs \<Longrightarrow> Ticket \<in> analz (spies evs)"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   287
by (blast dest: Says_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd])
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   288
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   289
lemma Oops_range_spies1:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   290
     "\<lbrakk> Says Kas A \<lbrace>Crypt KeyA \<lbrace>Key authK, Peer, Ta\<rbrace>, authTicket\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   291
           \<in> set evs ;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   292
         evs \<in> kerbV \<rbrakk> \<Longrightarrow> authK \<notin> range shrK & authK \<in> symKeys"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   293
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   294
apply (erule kerbV.induct, auto)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   295
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   296
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   297
lemma Oops_range_spies2:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   298
     "\<lbrakk> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, servTicket\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   299
           \<in> set evs ;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   300
         evs \<in> kerbV \<rbrakk> \<Longrightarrow> servK \<notin> range shrK \<and> servK \<in> symKeys"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   301
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   302
apply (erule kerbV.induct, auto)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   303
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   304
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   305
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   306
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   307
lemma Spy_see_shrK [simp]:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   308
     "evs \<in> kerbV \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   309
apply (erule kerbV.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   310
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   311
apply (frule_tac [5] Says_ticket_parts, simp_all)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   312
apply (blast+)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   313
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   314
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   315
lemma Spy_analz_shrK [simp]:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   316
     "evs \<in> kerbV \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   317
by auto
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   318
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   319
lemma Spy_see_shrK_D [dest!]:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   320
     "\<lbrakk> Key (shrK A) \<in> parts (spies evs);  evs \<in> kerbV \<rbrakk> \<Longrightarrow> A:bad"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   321
by (blast dest: Spy_see_shrK)
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   322
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   323
lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!]
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   324
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   325
text{*Nobody can have used non-existent keys!*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   326
lemma new_keys_not_used [simp]:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   327
    "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> kerbV\<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   328
     \<Longrightarrow> K \<notin> keysFor (parts (spies evs))"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   329
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   330
apply (erule kerbV.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   331
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   332
apply (frule_tac [5] Says_ticket_parts, simp_all)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   333
txt{*Fake*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   334
apply (force dest!: keysFor_parts_insert)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   335
txt{*Others*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   336
apply (force dest!: analz_shrK_Decrypt)+
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   337
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   338
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   339
(*Earlier, all protocol proofs declared this theorem.
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   340
  But few of them actually need it! (Another is Yahalom) *)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   341
lemma new_keys_not_analzd:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   342
 "\<lbrakk>evs \<in> kerbV; K \<in> symKeys; Key K \<notin> used evs\<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   343
  \<Longrightarrow> K \<notin> keysFor (analz (spies evs))"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   344
by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD])
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   345
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   346
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   347
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   348
subsection{*Regularity Lemmas*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   349
text{*These concern the form of items passed in messages*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   350
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   351
text{*Describes the form of all components sent by Kas*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   352
lemma Says_Kas_message_form:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   353
     "\<lbrakk> Says Kas A \<lbrace>Crypt K \<lbrace>Key authK, Agent Peer, Ta\<rbrace>, authTicket\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   354
           \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   355
         evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   356
      \<Longrightarrow> authK \<notin> range shrK \<and> authK \<in> authKeys evs \<and> authK \<in> symKeys \<and> 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   357
  authTicket = (Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Ta\<rbrace>) \<and>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   358
             K = shrK A  \<and> Peer = Tgs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   359
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   360
apply (erule kerbV.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   361
apply (simp_all (no_asm) add: authKeys_def authKeys_insert)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   362
apply blast+
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   363
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   364
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   365
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   366
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   367
(*This lemma is essential for proving Says_Tgs_message_form:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   368
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   369
  the session key authK
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   370
  supplied by Kas in the authentication ticket
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   371
  cannot be a long-term key!
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   372
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   373
  Generalised to any session keys (both authK and servK).
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   374
*)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   375
lemma SesKey_is_session_key:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   376
     "\<lbrakk> Crypt (shrK Tgs_B) \<lbrace>Agent A, Agent Tgs_B, Key SesKey, Number T\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   377
            \<in> parts (spies evs); Tgs_B \<notin> bad;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   378
         evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   379
      \<Longrightarrow> SesKey \<notin> range shrK"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   380
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   381
apply (erule kerbV.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   382
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   383
apply (frule_tac [5] Says_ticket_parts, simp_all, blast)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   384
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   385
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   386
lemma authTicket_authentic:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   387
     "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Ta\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   388
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   389
         evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   390
      \<Longrightarrow> Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Ta\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   391
                 Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Ta\<rbrace>\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   392
            \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   393
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   394
apply (erule kerbV.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   395
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   396
apply (frule_tac [5] Says_ticket_parts, simp_all)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   397
txt{*Fake, K4*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   398
apply (blast+)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   399
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   400
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   401
lemma authTicket_crypt_authK:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   402
     "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   403
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   404
         evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   405
      \<Longrightarrow> authK \<in> authKeys evs"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   406
by (metis authKeysI authTicket_authentic)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   407
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   408
text{*Describes the form of servK, servTicket and authK sent by Tgs*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   409
lemma Says_Tgs_message_form:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   410
     "\<lbrakk> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, servTicket\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   411
           \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   412
         evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   413
   \<Longrightarrow> B \<noteq> Tgs \<and> 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   414
       servK \<notin> range shrK \<and> servK \<notin> authKeys evs \<and> servK \<in> symKeys \<and>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   415
       servTicket = (Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>) \<and>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   416
       authK \<notin> range shrK \<and> authK \<in> authKeys evs \<and> authK \<in> symKeys"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   417
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   418
apply (erule kerbV.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   419
apply (simp_all add: authKeys_insert authKeys_not_insert authKeys_empty authKeys_simp, blast, auto)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   420
txt{*Three subcases of Message 4*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   421
apply (blast dest!: authKeys_used Says_Kas_message_form)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   422
apply (blast dest!: SesKey_is_session_key)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   423
apply (blast dest: authTicket_crypt_authK)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   424
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   425
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   426
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   427
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   428
(*
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   429
lemma authTicket_form:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   430
lemma servTicket_form:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   431
lemma Says_kas_message_form:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   432
lemma Says_tgs_message_form:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   433
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   434
cannot be proved for version V, but a new proof strategy can be used in their
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   435
place. The new strategy merely says that both the authTicket and the servTicket
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   436
are in parts and in analz as soon as they appear, using lemmas Says_ticket_parts and Says_ticket_analz. 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   437
The new strategy always lets the simplifier solve cases K3 and K5, saving on
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   438
long dedicated analyses, which seemed unavoidable. For this reason, lemma 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   439
servK_notin_authKeysD is no longer needed.
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   440
*)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   441
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   442
subsection{*Authenticity theorems: confirm origin of sensitive messages*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   443
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   444
lemma authK_authentic:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   445
     "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Peer, Ta\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   446
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   447
         A \<notin> bad;  evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   448
      \<Longrightarrow> \<exists> AT. Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Peer, Ta\<rbrace>, AT\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   449
            \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   450
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   451
apply (erule kerbV.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   452
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   453
apply (frule_tac [5] Says_ticket_parts, simp_all)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   454
apply blast+
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   455
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   456
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   457
text{*If a certain encrypted message appears then it originated with Tgs*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   458
lemma servK_authentic:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   459
     "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   460
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   461
         Key authK \<notin> analz (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   462
         authK \<notin> range shrK;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   463
         evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   464
 \<Longrightarrow> \<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   465
       \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   466
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   467
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   468
apply (erule kerbV.induct, analz_mono_contra)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   469
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   470
apply (frule_tac [5] Says_ticket_parts, simp_all)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   471
apply blast+
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   472
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   473
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   474
lemma servK_authentic_bis:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   475
     "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   476
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   477
         Key authK \<notin> analz (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   478
         B \<noteq> Tgs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   479
         evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   480
 \<Longrightarrow> \<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   481
       \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   482
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   483
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   484
apply (erule kerbV.induct, analz_mono_contra)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   485
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   486
apply (frule_tac [5] Says_ticket_parts, simp_all, blast+)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   487
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   488
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   489
text{*Authenticity of servK for B*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   490
lemma servTicket_authentic_Tgs:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   491
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   492
           \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   493
         evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   494
 \<Longrightarrow> \<exists>authK.
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   495
       Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   496
                    Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   497
       \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   498
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   499
apply (erule kerbV.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   500
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   501
apply (frule_tac [5] Says_ticket_parts, simp_all, blast+)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   502
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   503
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   504
text{*Anticipated here from next subsection*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   505
lemma K4_imp_K2:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   506
"\<lbrakk> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, servTicket\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   507
      \<in> set evs;  evs \<in> kerbV\<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   508
   \<Longrightarrow> \<exists>Ta. Says Kas A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   509
        \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   510
           Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace> \<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   511
        \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   512
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   513
apply (erule kerbV.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   514
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   515
apply (frule_tac [5] Says_ticket_parts, simp_all, auto)
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   516
apply (metis MPair_analz Says_imp_analz_Spy analz_conj_parts authTicket_authentic)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   517
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   518
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   519
text{*Anticipated here from next subsection*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   520
lemma u_K4_imp_K2:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   521
"\<lbrakk> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, servTicket\<rbrace>  \<in> set evs; evs \<in> kerbV\<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   522
   \<Longrightarrow> \<exists>Ta. Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   523
             Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace> \<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   524
             \<in> set evs
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   525
          \<and> servKlife + Ts <= authKlife + Ta"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   526
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   527
apply (erule kerbV.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   528
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   529
apply (frule_tac [5] Says_ticket_parts, simp_all, auto)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   530
apply (blast dest!: Says_imp_spies [THEN parts.Inj, THEN parts.Fst, THEN authTicket_authentic])
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   531
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   532
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   533
lemma servTicket_authentic_Kas:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   534
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   535
           \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   536
         evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   537
  \<Longrightarrow> \<exists>authK Ta.
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   538
       Says Kas A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   539
         \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   540
           Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace> \<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   541
        \<in> set evs"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   542
by (metis K4_imp_K2 servTicket_authentic_Tgs)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   543
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   544
lemma u_servTicket_authentic_Kas:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   545
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   546
           \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   547
         evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   548
  \<Longrightarrow> \<exists>authK Ta.
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   549
       Says Kas A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   550
         \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   551
           Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace> \<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   552
        \<in> set evs \<and> 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   553
      servKlife + Ts <= authKlife + Ta"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   554
by (metis servTicket_authentic_Tgs u_K4_imp_K2)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   555
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   556
lemma servTicket_authentic:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   557
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   558
           \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   559
         evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   560
 \<Longrightarrow> \<exists>Ta authK.
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   561
     Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   562
                  Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace> \<rbrace>  \<in> set evs
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   563
     \<and> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   564
                  Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   565
       \<in> set evs"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   566
by (metis K4_imp_K2 servTicket_authentic_Tgs)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   567
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   568
lemma u_servTicket_authentic:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   569
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   570
           \<in> parts (spies evs);  B \<noteq> Tgs;  B \<notin> bad;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   571
         evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   572
 \<Longrightarrow> \<exists>Ta authK.
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   573
     Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   574
                  Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace> \<in> set evs
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   575
     \<and> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   576
                 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   577
       \<in> set evs
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   578
     \<and> servKlife + Ts <= authKlife + Ta"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   579
by (metis servTicket_authentic_Tgs u_K4_imp_K2)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   580
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   581
lemma u_NotexpiredSK_NotexpiredAK:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   582
     "\<lbrakk> \<not> expiredSK Ts evs; servKlife + Ts <= authKlife + Ta \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   583
      \<Longrightarrow> \<not> expiredAK Ta evs"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   584
by (metis order_le_less_trans)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   585
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   586
subsection{* Reliability: friendly agents send somthing if something else happened*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   587
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   588
lemma K3_imp_K2:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   589
     "\<lbrakk> Says A Tgs
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   590
             \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   591
           \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   592
         A \<notin> bad;  evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   593
      \<Longrightarrow> \<exists>Ta AT. Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Ta\<rbrace>, 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   594
                               AT\<rbrace> \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   595
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   596
apply (erule kerbV.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   597
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   598
apply (frule_tac [5] Says_ticket_parts, simp_all, blast, blast)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   599
apply (blast dest: Says_imp_spies [THEN parts.Inj, THEN parts.Fst, THEN authK_authentic])
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   600
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   601
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   602
text{*Anticipated here from next subsection. An authK is encrypted by one and only one Shared key. A servK is encrypted by one and only one authK.*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   603
lemma Key_unique_SesKey:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   604
     "\<lbrakk> Crypt K  \<lbrace>Key SesKey,  Agent B, T\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   605
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   606
         Crypt K' \<lbrace>Key SesKey,  Agent B', T'\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   607
           \<in> parts (spies evs);  Key SesKey \<notin> analz (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   608
         evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   609
      \<Longrightarrow> K=K' \<and> B=B' \<and> T=T'"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   610
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   611
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   612
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   613
apply (erule kerbV.induct, analz_mono_contra)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   614
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   615
apply (frule_tac [5] Says_ticket_parts, simp_all)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   616
txt{*Fake, K2, K4*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   617
apply (blast+)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   618
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   619
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   620
text{*This inevitably has an existential form in version V*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   621
lemma Says_K5:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   622
     "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   623
         Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   624
                                     servTicket\<rbrace> \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   625
         Key servK \<notin> analz (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   626
         A \<notin> bad; B \<notin> bad; evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   627
 \<Longrightarrow> \<exists> ST. Says A B \<lbrace>ST, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   628
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   629
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   630
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   631
apply (erule kerbV.induct, analz_mono_contra)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   632
apply (frule_tac [5] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   633
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   634
apply (simp_all (no_asm_simp) add: all_conj_distrib)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   635
apply blast
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   636
txt{*K3*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   637
apply (blast dest: authK_authentic Says_Kas_message_form Says_Tgs_message_form)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   638
txt{*K4*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   639
apply (force dest!: Crypt_imp_keysFor)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   640
txt{*K5*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   641
apply (blast dest: Key_unique_SesKey)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   642
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   643
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   644
text{*Anticipated here from next subsection*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   645
lemma unique_CryptKey:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   646
     "\<lbrakk> Crypt (shrK B)  \<lbrace>Agent A,  Agent B,  Key SesKey, T\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   647
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   648
         Crypt (shrK B') \<lbrace>Agent A', Agent B', Key SesKey, T'\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   649
           \<in> parts (spies evs);  Key SesKey \<notin> analz (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   650
         evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   651
      \<Longrightarrow> A=A' & B=B' & T=T'"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   652
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   653
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   654
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   655
apply (erule kerbV.induct, analz_mono_contra)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   656
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   657
apply (frule_tac [5] Says_ticket_parts, simp_all)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   658
txt{*Fake, K2, K4*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   659
apply (blast+)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   660
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   661
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   662
lemma Says_K6:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   663
     "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   664
         Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   665
                      servTicket\<rbrace> \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   666
         Key servK \<notin> analz (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   667
         A \<notin> bad; B \<notin> bad; evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   668
      \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   669
apply (frule Says_Tgs_message_form, assumption, clarify)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   670
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   671
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   672
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   673
apply (erule kerbV.induct, analz_mono_contra)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   674
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   675
apply (frule_tac [5] Says_ticket_parts)
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   676
apply simp_all
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   677
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   678
txt{*fake*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   679
apply blast
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   680
txt{*K4*}
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   681
apply (force dest!: Crypt_imp_keysFor)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   682
txt{*K6*}
47050
7be54568efa1 optimized "metis" call
blanchet
parents: 43587
diff changeset
   683
apply (metis MPair_parts Says_imp_parts_knows_Spy unique_CryptKey)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   684
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   685
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   686
text{*Needs a unicity theorem, hence moved here*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   687
lemma servK_authentic_ter:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   688
 "\<lbrakk> Says Kas A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   689
       \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Ta\<rbrace>, authTicket\<rbrace> \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   690
     Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   691
       \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   692
     Key authK \<notin> analz (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   693
     evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   694
 \<Longrightarrow> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   695
                 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace> \<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   696
       \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   697
apply (frule Says_Kas_message_form, assumption)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   698
apply clarify
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   699
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   700
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   701
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   702
apply (erule kerbV.induct, analz_mono_contra)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   703
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   704
apply (frule_tac [5] Says_ticket_parts, simp_all, blast)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   705
txt{*K2 and K4 remain*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   706
apply (blast dest!: servK_authentic Says_Tgs_message_form authKeys_used)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   707
apply (blast dest!: unique_CryptKey)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   708
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   709
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   710
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   711
subsection{*Unicity Theorems*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   712
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   713
text{* The session key, if secure, uniquely identifies the Ticket
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   714
   whether authTicket or servTicket. As a matter of fact, one can read
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   715
   also Tgs in the place of B.                                     *}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   716
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   717
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   718
lemma unique_authKeys:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   719
     "\<lbrakk> Says Kas A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   720
              \<lbrace>Crypt Ka \<lbrace>Key authK, Agent Tgs, Ta\<rbrace>, X\<rbrace> \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   721
         Says Kas A'
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   722
              \<lbrace>Crypt Ka' \<lbrace>Key authK, Agent Tgs, Ta'\<rbrace>, X'\<rbrace> \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   723
         evs \<in> kerbV \<rbrakk> \<Longrightarrow> A=A' \<and> Ka=Ka' \<and> Ta=Ta' \<and> X=X'"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   724
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   725
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   726
apply (erule kerbV.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   727
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   728
apply (frule_tac [5] Says_ticket_parts, simp_all)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   729
apply blast+
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   730
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   731
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   732
text{* servK uniquely identifies the message from Tgs *}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   733
lemma unique_servKeys:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   734
     "\<lbrakk> Says Tgs A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   735
              \<lbrace>Crypt K \<lbrace>Key servK, Agent B, Ts\<rbrace>, X\<rbrace> \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   736
         Says Tgs A'
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   737
              \<lbrace>Crypt K' \<lbrace>Key servK, Agent B', Ts'\<rbrace>, X'\<rbrace> \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   738
         evs \<in> kerbV \<rbrakk> \<Longrightarrow> A=A' \<and> B=B' \<and> K=K' \<and> Ts=Ts' \<and> X=X'"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   739
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   740
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   741
apply (erule kerbV.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   742
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   743
apply (frule_tac [5] Says_ticket_parts, simp_all)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   744
apply blast+
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   745
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   746
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   747
subsection{*Lemmas About the Predicate @{term AKcryptSK}*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   748
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   749
lemma not_AKcryptSK_Nil [iff]: "\<not> AKcryptSK authK servK []"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   750
apply (simp add: AKcryptSK_def)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   751
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   752
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   753
lemma AKcryptSKI:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   754
 "\<lbrakk> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, tt\<rbrace>, X \<rbrace> \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   755
     evs \<in> kerbV \<rbrakk> \<Longrightarrow> AKcryptSK authK servK evs"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   756
by (metis AKcryptSK_def Says_Tgs_message_form)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   757
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   758
lemma AKcryptSK_Says [simp]:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   759
   "AKcryptSK authK servK (Says S A X # evs) =
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   760
     (S = Tgs \<and>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   761
      (\<exists>B tt. X = \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, tt\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   762
                    Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, tt\<rbrace> \<rbrace>)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   763
     | AKcryptSK authK servK evs)"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   764
by (auto simp add: AKcryptSK_def) 
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   765
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   766
lemma AKcryptSK_Notes [simp]:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   767
   "AKcryptSK authK servK (Notes A X # evs) =
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   768
      AKcryptSK authK servK evs"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   769
by (auto simp add: AKcryptSK_def) 
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   770
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   771
(*A fresh authK cannot be associated with any other
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   772
  (with respect to a given trace). *)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   773
lemma Auth_fresh_not_AKcryptSK:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   774
     "\<lbrakk> Key authK \<notin> used evs; evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   775
      \<Longrightarrow> \<not> AKcryptSK authK servK evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   776
apply (unfold AKcryptSK_def)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   777
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   778
apply (erule kerbV.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   779
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   780
apply (frule_tac [5] Says_ticket_parts, simp_all, blast)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   781
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   782
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   783
(*A fresh servK cannot be associated with any other
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   784
  (with respect to a given trace). *)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   785
lemma Serv_fresh_not_AKcryptSK:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   786
 "Key servK \<notin> used evs \<Longrightarrow> \<not> AKcryptSK authK servK evs"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   787
by (auto simp add: AKcryptSK_def) 
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   788
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   789
lemma authK_not_AKcryptSK:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   790
     "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, tk\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   791
           \<in> parts (spies evs);  evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   792
      \<Longrightarrow> \<not> AKcryptSK K authK evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   793
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   794
apply (erule kerbV.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   795
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   796
apply (frule_tac [5] Says_ticket_parts, simp_all)
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   797
txt{*Fake,K2,K4*}
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   798
apply (auto simp add: AKcryptSK_def)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   799
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   800
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   801
text{*A secure serverkey cannot have been used to encrypt others*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   802
lemma servK_not_AKcryptSK:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   803
 "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key SK, tt\<rbrace> \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   804
     Key SK \<notin> analz (spies evs);  SK \<in> symKeys;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   805
     B \<noteq> Tgs;  evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   806
  \<Longrightarrow> \<not> AKcryptSK SK K evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   807
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   808
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   809
apply (erule kerbV.induct, analz_mono_contra)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   810
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   811
apply (frule_tac [5] Says_ticket_parts, simp_all, blast)
32404
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 26300
diff changeset
   812
txt{*K4*}
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   813
apply (metis Auth_fresh_not_AKcryptSK MPair_parts Says_imp_parts_knows_Spy authKeys_used authTicket_crypt_authK unique_CryptKey)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   814
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   815
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   816
text{*Long term keys are not issued as servKeys*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   817
lemma shrK_not_AKcryptSK:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   818
     "evs \<in> kerbV \<Longrightarrow> \<not> AKcryptSK K (shrK A) evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   819
apply (unfold AKcryptSK_def)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   820
apply (erule kerbV.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   821
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   822
apply (frule_tac [5] Says_ticket_parts, auto)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   823
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   824
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   825
text{*The Tgs message associates servK with authK and therefore not with any
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   826
  other key authK.*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   827
lemma Says_Tgs_AKcryptSK:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   828
     "\<lbrakk> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, tt\<rbrace>, X \<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   829
           \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   830
         authK' \<noteq> authK;  evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   831
      \<Longrightarrow> \<not> AKcryptSK authK' servK evs"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   832
by (metis AKcryptSK_def unique_servKeys)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   833
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   834
lemma AKcryptSK_not_AKcryptSK:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   835
     "\<lbrakk> AKcryptSK authK servK evs;  evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   836
      \<Longrightarrow> \<not> AKcryptSK servK K evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   837
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   838
apply (erule kerbV.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   839
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   840
apply (frule_tac [5] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   841
apply (simp_all, safe)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   842
txt{*K4 splits into subcases*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   843
prefer 4 apply (blast dest!: authK_not_AKcryptSK)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   844
txt{*servK is fresh and so could not have been used, by
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   845
   @{text new_keys_not_used}*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   846
 prefer 2 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   847
 apply (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   848
txt{*Others by freshness*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   849
apply (blast+)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   850
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   851
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   852
lemma not_different_AKcryptSK:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   853
     "\<lbrakk> AKcryptSK authK servK evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   854
        authK' \<noteq> authK;  evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   855
      \<Longrightarrow> \<not> AKcryptSK authK' servK evs  \<and> servK \<in> symKeys"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   856
apply (simp add: AKcryptSK_def)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   857
apply (blast dest: unique_servKeys Says_Tgs_message_form)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   858
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   859
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   860
text{*The only session keys that can be found with the help of session keys are
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   861
  those sent by Tgs in step K4.  *}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   862
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   863
text{*We take some pains to express the property
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   864
  as a logical equivalence so that the simplifier can apply it.*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   865
lemma Key_analz_image_Key_lemma:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   866
     "P \<longrightarrow> (Key K \<in> analz (Key`KK Un H)) \<longrightarrow> (K:KK | Key K \<in> analz H)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   867
      \<Longrightarrow>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   868
      P \<longrightarrow> (Key K \<in> analz (Key`KK Un H)) = (K:KK | Key K \<in> analz H)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   869
by (blast intro: analz_mono [THEN subsetD])
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   870
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   871
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   872
lemma AKcryptSK_analz_insert:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   873
     "\<lbrakk> AKcryptSK K K' evs; K \<in> symKeys; evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   874
      \<Longrightarrow> Key K' \<in> analz (insert (Key K) (spies evs))"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   875
apply (simp add: AKcryptSK_def, clarify)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   876
apply (drule Says_imp_spies [THEN analz.Inj, THEN analz_insertI], auto)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   877
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   878
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   879
lemma authKeys_are_not_AKcryptSK:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   880
     "\<lbrakk> K \<in> authKeys evs Un range shrK;  evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   881
      \<Longrightarrow> \<forall>SK. \<not> AKcryptSK SK K evs \<and> K \<in> symKeys"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   882
apply (simp add: authKeys_def AKcryptSK_def)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   883
apply (blast dest: Says_Kas_message_form Says_Tgs_message_form)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   884
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   885
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   886
lemma not_authKeys_not_AKcryptSK:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   887
     "\<lbrakk> K \<notin> authKeys evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   888
         K \<notin> range shrK; evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   889
      \<Longrightarrow> \<forall>SK. \<not> AKcryptSK K SK evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   890
apply (simp add: AKcryptSK_def)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   891
apply (blast dest: Says_Tgs_message_form)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   892
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   893
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   894
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   895
subsection{*Secrecy Theorems*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   896
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   897
text{*For the Oops2 case of the next theorem*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   898
lemma Oops2_not_AKcryptSK:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   899
     "\<lbrakk> evs \<in> kerbV;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   900
         Says Tgs A \<lbrace>Crypt authK
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   901
                     \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, servTicket\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   902
           \<in> set evs \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   903
      \<Longrightarrow> \<not> AKcryptSK servK SK evs"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
   904
by (blast dest: AKcryptSKI AKcryptSK_not_AKcryptSK)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   905
   
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   906
text{* Big simplification law for keys SK that are not crypted by keys in KK
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   907
 It helps prove three, otherwise hard, facts about keys. These facts are
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   908
 exploited as simplification laws for analz, and also "limit the damage"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   909
 in case of loss of a key to the spy. See ESORICS98.*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   910
lemma Key_analz_image_Key [rule_format (no_asm)]:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   911
     "evs \<in> kerbV \<Longrightarrow>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   912
      (\<forall>SK KK. SK \<in> symKeys & KK <= -(range shrK) \<longrightarrow>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   913
       (\<forall>K \<in> KK. \<not> AKcryptSK K SK evs)   \<longrightarrow>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   914
       (Key SK \<in> analz (Key`KK Un (spies evs))) =
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   915
       (SK \<in> KK | Key SK \<in> analz (spies evs)))"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   916
apply (erule kerbV.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   917
apply (frule_tac [10] Oops_range_spies2)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   918
apply (frule_tac [9] Oops_range_spies1)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   919
(*Used to apply Says_tgs_message form, which is no longer available. 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   920
  Instead\<dots>*)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   921
apply (drule_tac [7] Says_ticket_analz)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   922
(*Used to apply Says_kas_message form, which is no longer available. 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   923
  Instead\<dots>*)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   924
apply (drule_tac [5] Says_ticket_analz)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   925
apply (safe del: impI intro!: Key_analz_image_Key_lemma [THEN impI])
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   926
txt{*Case-splits for Oops1 and message 5: the negated case simplifies using
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   927
 the induction hypothesis*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   928
apply (case_tac [9] "AKcryptSK authK SK evsO1")
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   929
apply (case_tac [7] "AKcryptSK servK SK evs5")
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   930
apply (simp_all del: image_insert
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   931
          add: analz_image_freshK_simps AKcryptSK_Says shrK_not_AKcryptSK
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   932
               Oops2_not_AKcryptSK Auth_fresh_not_AKcryptSK
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   933
               Serv_fresh_not_AKcryptSK Says_Tgs_AKcryptSK Spy_analz_shrK)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   934
txt{*Fake*} 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   935
apply spy_analz
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   936
txt{*K2*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   937
apply blast 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   938
txt{*Cases K3 and K5 solved by the simplifier thanks to the ticket being in 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   939
analz - this strategy is new wrt version IV*} 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   940
txt{*K4*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   941
apply (blast dest!: authK_not_AKcryptSK)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   942
txt{*Oops1*}
32404
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 26300
diff changeset
   943
apply (metis AKcryptSK_analz_insert insert_Key_singleton)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   944
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   945
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   946
text{* First simplification law for analz: no session keys encrypt
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   947
authentication keys or shared keys. *}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   948
lemma analz_insert_freshK1:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   949
     "\<lbrakk> evs \<in> kerbV;  K \<in> authKeys evs Un range shrK;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   950
        SesKey \<notin> range shrK \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   951
      \<Longrightarrow> (Key K \<in> analz (insert (Key SesKey) (spies evs))) =
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   952
          (K = SesKey | Key K \<in> analz (spies evs))"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   953
apply (frule authKeys_are_not_AKcryptSK, assumption)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   954
apply (simp del: image_insert
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   955
            add: analz_image_freshK_simps add: Key_analz_image_Key)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   956
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   957
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   958
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   959
text{* Second simplification law for analz: no service keys encrypt any other keys.*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   960
lemma analz_insert_freshK2:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   961
     "\<lbrakk> evs \<in> kerbV;  servK \<notin> (authKeys evs); servK \<notin> range shrK;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   962
        K \<in> symKeys \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   963
      \<Longrightarrow> (Key K \<in> analz (insert (Key servK) (spies evs))) =
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   964
          (K = servK | Key K \<in> analz (spies evs))"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   965
apply (frule not_authKeys_not_AKcryptSK, assumption, assumption)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   966
apply (simp del: image_insert
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   967
            add: analz_image_freshK_simps add: Key_analz_image_Key)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   968
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   969
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   970
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   971
text{* Third simplification law for analz: only one authentication key encrypts a certain service key.*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   972
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   973
lemma analz_insert_freshK3:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   974
 "\<lbrakk> AKcryptSK authK servK evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   975
    authK' \<noteq> authK; authK' \<notin> range shrK; evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   976
        \<Longrightarrow> (Key servK \<in> analz (insert (Key authK') (spies evs))) =
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   977
                (servK = authK' | Key servK \<in> analz (spies evs))"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   978
apply (drule_tac authK' = authK' in not_different_AKcryptSK, blast, assumption)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   979
apply (simp del: image_insert
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   980
            add: analz_image_freshK_simps add: Key_analz_image_Key)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   981
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   982
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   983
lemma analz_insert_freshK3_bis:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   984
 "\<lbrakk> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, servTicket\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   985
        \<in> set evs; 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   986
     authK \<noteq> authK'; authK' \<notin> range shrK; evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   987
        \<Longrightarrow> (Key servK \<in> analz (insert (Key authK') (spies evs))) =
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   988
                (servK = authK' | Key servK \<in> analz (spies evs))"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   989
apply (frule AKcryptSKI, assumption)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   990
apply (simp add: analz_insert_freshK3)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   991
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   992
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   993
text{*a weakness of the protocol*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   994
lemma authK_compromises_servK:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   995
     "\<lbrakk> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, servTicket\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   996
        \<in> set evs;  authK \<in> symKeys;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   997
         Key authK \<in> analz (spies evs); evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   998
      \<Longrightarrow> Key servK \<in> analz (spies evs)"
32404
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 26300
diff changeset
   999
  by (metis Says_imp_analz_Spy analz.Fst analz_Decrypt')
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 26300
diff changeset
  1000
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1001
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1002
text{*lemma @{text servK_notin_authKeysD} not needed in version V*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1003
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1004
text{*If Spy sees the Authentication Key sent in msg K2, then
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1005
    the Key has expired.*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1006
lemma Confidentiality_Kas_lemma [rule_format]:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1007
     "\<lbrakk> authK \<in> symKeys; A \<notin> bad;  evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1008
      \<Longrightarrow> Says Kas A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1009
               \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1010
          Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1011
            \<in> set evs \<longrightarrow>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1012
          Key authK \<in> analz (spies evs) \<longrightarrow>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1013
          expiredAK Ta evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1014
apply (erule kerbV.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1015
apply (frule_tac [10] Oops_range_spies2)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1016
apply (frule_tac [9] Oops_range_spies1)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1017
apply (frule_tac [7] Says_ticket_analz)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1018
apply (frule_tac [5] Says_ticket_analz)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1019
apply (safe del: impI conjI impCE)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1020
apply (simp_all (no_asm_simp) add: Says_Kas_message_form less_SucI analz_insert_eq not_parts_not_analz analz_insert_freshK1 pushes)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1021
txt{*Fake*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1022
apply spy_analz
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1023
txt{*K2*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1024
apply blast
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1025
txt{*K4*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1026
apply blast
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1027
txt{*Oops1*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1028
apply (blast dest!: unique_authKeys intro: less_SucI)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1029
txt{*Oops2*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1030
apply (blast dest: Says_Tgs_message_form Says_Kas_message_form)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1031
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1032
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1033
lemma Confidentiality_Kas:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1034
     "\<lbrakk> Says Kas A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1035
              \<lbrace>Crypt Ka \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>, authTicket\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1036
           \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1037
        \<not> expiredAK Ta evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1038
        A \<notin> bad;  evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1039
      \<Longrightarrow> Key authK \<notin> analz (spies evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1040
apply (blast dest: Says_Kas_message_form Confidentiality_Kas_lemma)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1041
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1042
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1043
text{*If Spy sees the Service Key sent in msg K4, then
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1044
    the Key has expired.*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1045
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1046
lemma Confidentiality_lemma [rule_format]:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1047
     "\<lbrakk> Says Tgs A
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
  1048
            \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>,
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
  1049
              Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
  1050
           \<in> set evs;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
  1051
        Key authK \<notin> analz (spies evs);
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1052
        servK \<in> symKeys;
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
  1053
        A \<notin> bad;  B \<notin> bad; evs \<in> kerbV \<rbrakk>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1054
      \<Longrightarrow> Key servK \<in> analz (spies evs) \<longrightarrow>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
  1055
          expiredSK Ts evs"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1056
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1057
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1058
apply (erule kerbV.induct)
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
  1059
apply (rule_tac [9] impI)+
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1060
  --{*The Oops1 case is unusual: must simplify
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1061
    @{term "Authkey \<notin> analz (spies (ev#evs))"}, not letting
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1062
   @{text analz_mono_contra} weaken it to
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1063
   @{term "Authkey \<notin> analz (spies evs)"},
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1064
  for we then conclude @{term "authK \<noteq> authKa"}.*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1065
apply analz_mono_contra
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1066
apply (frule_tac [10] Oops_range_spies2)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1067
apply (frule_tac [9] Oops_range_spies1)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1068
apply (frule_tac [7] Says_ticket_analz)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1069
apply (frule_tac [5] Says_ticket_analz)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1070
apply (safe del: impI conjI impCE)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1071
apply (simp_all add: less_SucI new_keys_not_analzd Says_Kas_message_form Says_Tgs_message_form analz_insert_eq not_parts_not_analz analz_insert_freshK1 analz_insert_freshK2 analz_insert_freshK3_bis pushes)
32404
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 26300
diff changeset
  1072
    txt{*Fake*}
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 26300
diff changeset
  1073
    apply spy_analz
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 26300
diff changeset
  1074
   txt{*K2*}
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 26300
diff changeset
  1075
   apply (blast intro: parts_insertI less_SucI)
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 26300
diff changeset
  1076
  txt{*K4*}
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 26300
diff changeset
  1077
  apply (blast dest: authTicket_authentic Confidentiality_Kas)
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 26300
diff changeset
  1078
 txt{*Oops1*}
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1079
 apply (blast dest: Says_Kas_message_form Says_Tgs_message_form intro: less_SucI)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1080
txt{*Oops2*}
32404
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 26300
diff changeset
  1081
apply (metis Suc_le_eq linorder_linear linorder_not_le msg.simps(2) unique_servKeys)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1082
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1083
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1084
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1085
text{* In the real world Tgs can't check wheter authK is secure! *}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1086
lemma Confidentiality_Tgs:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1087
     "\<lbrakk> Says Tgs A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1088
              \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, servTicket\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1089
           \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1090
         Key authK \<notin> analz (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1091
         \<not> expiredSK Ts evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1092
         A \<notin> bad;  B \<notin> bad; evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1093
      \<Longrightarrow> Key servK \<notin> analz (spies evs)"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
  1094
by (blast dest: Says_Tgs_message_form Confidentiality_lemma)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1095
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1096
text{* In the real world Tgs CAN check what Kas sends! *}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1097
lemma Confidentiality_Tgs_bis:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1098
     "\<lbrakk> Says Kas A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1099
               \<lbrace>Crypt Ka \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>, authTicket\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1100
           \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1101
         Says Tgs A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1102
              \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, servTicket\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1103
           \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1104
         \<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1105
         A \<notin> bad;  B \<notin> bad; evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1106
      \<Longrightarrow> Key servK \<notin> analz (spies evs)"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
  1107
by (blast dest!: Confidentiality_Kas Confidentiality_Tgs)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1108
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1109
text{*Most general form*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1110
lemmas Confidentiality_Tgs_ter = authTicket_authentic [THEN Confidentiality_Tgs_bis]
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1111
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1112
lemmas Confidentiality_Auth_A = authK_authentic [THEN exE, THEN Confidentiality_Kas]
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1113
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1114
text{*Needs a confidentiality guarantee, hence moved here.
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1115
      Authenticity of servK for A*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1116
lemma servK_authentic_bis_r:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1117
     "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1118
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1119
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1120
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1121
         \<not> expiredAK Ta evs; A \<notin> bad; evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1122
 \<Longrightarrow> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1123
                 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1124
       \<in> set evs"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
  1125
by (metis Confidentiality_Kas authK_authentic servK_authentic_ter)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1126
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1127
lemma Confidentiality_Serv_A:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1128
     "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1129
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1130
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1131
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1132
         \<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1133
         A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1134
      \<Longrightarrow> Key servK \<notin> analz (spies evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1135
apply (drule authK_authentic, assumption, assumption)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1136
apply (blast dest: Confidentiality_Kas Says_Kas_message_form servK_authentic_ter Confidentiality_Tgs_bis)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1137
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1138
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1139
lemma Confidentiality_B:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1140
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1141
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1142
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1143
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1144
         Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1145
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1146
         \<not> expiredSK Ts evs; \<not> expiredAK Ta evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1147
         A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1148
      \<Longrightarrow> Key servK \<notin> analz (spies evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1149
apply (frule authK_authentic)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1150
apply (erule_tac [3] exE)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1151
apply (frule_tac [3] Confidentiality_Kas)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1152
apply (frule_tac [6] servTicket_authentic, auto)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1153
apply (blast dest!: Confidentiality_Tgs_bis dest: Says_Kas_message_form servK_authentic unique_servKeys unique_authKeys)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1154
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1155
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1156
lemma u_Confidentiality_B:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1157
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1158
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1159
         \<not> expiredSK Ts evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1160
         A \<notin> bad;  B \<notin> bad;  B \<noteq> Tgs; evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1161
      \<Longrightarrow> Key servK \<notin> analz (spies evs)"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
  1162
by (blast dest: u_servTicket_authentic u_NotexpiredSK_NotexpiredAK Confidentiality_Tgs_bis)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1163
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1164
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1165
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1166
subsection{*Parties authentication: each party verifies "the identity of
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1167
       another party who generated some data" (quoted from Neuman and Ts'o).*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1168
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1169
text{*These guarantees don't assess whether two parties agree on
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1170
      the same session key: sending a message containing a key
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1171
      doesn't a priori state knowledge of the key.*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1172
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1173
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1174
text{*These didn't have existential form in version IV*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1175
lemma B_authenticates_A:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1176
     "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1177
        Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1178
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1179
        Key servK \<notin> analz (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1180
        A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1181
  \<Longrightarrow> \<exists> ST. Says A B \<lbrace>ST, Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<rbrace> \<in> set evs"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
  1182
by (blast dest: servTicket_authentic_Tgs intro: Says_K5)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1183
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1184
text{*The second assumption tells B what kind of key servK is.*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1185
lemma B_authenticates_A_r:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1186
     "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1187
         Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1188
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1189
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1190
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1191
         Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1192
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1193
         \<not> expiredSK Ts evs; \<not> expiredAK Ta evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1194
         B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1195
  \<Longrightarrow> \<exists> ST. Says A B \<lbrace>ST, Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<rbrace> \<in> set evs"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
  1196
by (blast intro: Says_K5 dest: Confidentiality_B servTicket_authentic_Tgs)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1197
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1198
text{* @{text u_B_authenticates_A} would be the same as @{text B_authenticates_A} because the
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1199
 servK confidentiality assumption is yet unrelaxed*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1200
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1201
lemma u_B_authenticates_A_r:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1202
     "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1203
         Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1204
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1205
         \<not> expiredSK Ts evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1206
         B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1207
  \<Longrightarrow> \<exists> ST. Says A B \<lbrace>ST, Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<rbrace> \<in> set evs"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
  1208
by (blast intro: Says_K5 dest: u_Confidentiality_B servTicket_authentic_Tgs)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1209
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1210
lemma A_authenticates_B:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1211
     "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1212
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1213
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1214
         Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1215
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1216
         Key authK \<notin> analz (spies evs); Key servK \<notin> analz (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1217
         A \<notin> bad;  B \<notin> bad; evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1218
      \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs"
32404
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 26300
diff changeset
  1219
  by (metis authK_authentic Oops_range_spies1 Says_K6 servK_authentic u_K4_imp_K2 unique_authKeys)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1220
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1221
lemma A_authenticates_B_r:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1222
     "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1223
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1224
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1225
         Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1226
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1227
         \<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1228
         A \<notin> bad;  B \<notin> bad; evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1229
      \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1230
apply (frule authK_authentic)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1231
apply (erule_tac [3] exE)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1232
apply (frule_tac [3] Says_Kas_message_form)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1233
apply (frule_tac [4] Confidentiality_Kas)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1234
apply (frule_tac [7] servK_authentic)
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
  1235
apply auto
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
  1236
apply (metis Confidentiality_Tgs K4_imp_K2 Says_K6 unique_authKeys) 
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1237
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1238
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1239
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1240
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1241
subsection{*Parties' knowledge of session keys. 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1242
       An agent knows a session key if he used it to issue a cipher. These
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1243
       guarantees can be interpreted both in terms of key distribution
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1244
       and of non-injective agreement on the session key.*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1245
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1246
lemma Kas_Issues_A:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1247
   "\<lbrakk> Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Peer, Ta\<rbrace>, authTicket\<rbrace> \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1248
      evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1249
  \<Longrightarrow> Kas Issues A with (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta\<rbrace>)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1250
          on evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1251
apply (simp (no_asm) add: Issues_def)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1252
apply (rule exI)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1253
apply (rule conjI, assumption)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1254
apply (simp (no_asm))
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1255
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1256
apply (erule kerbV.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1257
apply (frule_tac [5] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1258
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1259
apply (simp_all (no_asm_simp) add: all_conj_distrib)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1260
txt{*K2*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1261
apply (simp add: takeWhile_tail)
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
  1262
apply (metis MPair_parts parts.Body parts_idem parts_spies_takeWhile_mono parts_trans spies_evs_rev usedI)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1263
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1264
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1265
lemma A_authenticates_and_keydist_to_Kas:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1266
  "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Peer, Ta\<rbrace> \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1267
     A \<notin> bad; evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1268
 \<Longrightarrow> Kas Issues A with (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta\<rbrace>) 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1269
          on evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1270
by (blast dest!: authK_authentic Kas_Issues_A)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1271
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1272
lemma Tgs_Issues_A:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1273
    "\<lbrakk> Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, servTicket\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1274
         \<in> set evs; 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1275
       Key authK \<notin> analz (spies evs);  evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1276
  \<Longrightarrow> Tgs Issues A with 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1277
          (Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>) on evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1278
apply (simp (no_asm) add: Issues_def)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1279
apply (rule exI)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1280
apply (rule conjI, assumption)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1281
apply (simp (no_asm))
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1282
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1283
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1284
apply (erule kerbV.induct, analz_mono_contra)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1285
apply (frule_tac [5] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1286
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1287
apply (simp_all (no_asm_simp) add: all_conj_distrib)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1288
apply (simp add: takeWhile_tail)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1289
(*Last two thms installed only to derive authK \<notin> range shrK*)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1290
apply (blast dest: servK_authentic parts_spies_takeWhile_mono [THEN subsetD]
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1291
      parts_spies_evs_revD2 [THEN subsetD] authTicket_authentic 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1292
      Says_Kas_message_form)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1293
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1294
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1295
lemma A_authenticates_and_keydist_to_Tgs:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1296
     "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1297
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1298
       Key authK \<notin> analz (spies evs); B \<noteq> Tgs; evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1299
  \<Longrightarrow> \<exists>A. Tgs Issues A with 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1300
          (Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>) on evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1301
by (blast dest: Tgs_Issues_A servK_authentic_bis)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1302
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1303
lemma B_Issues_A:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1304
     "\<lbrakk> Says B A (Crypt servK (Number T3)) \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1305
         Key servK \<notin> analz (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1306
         A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1307
      \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1308
apply (simp (no_asm) add: Issues_def)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1309
apply (rule exI)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1310
apply (rule conjI, assumption)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1311
apply (simp (no_asm))
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1312
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1313
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1314
apply (erule kerbV.induct, analz_mono_contra)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1315
apply (simp_all (no_asm_simp) add: all_conj_distrib)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1316
apply blast
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1317
txt{*K6 requires numerous lemmas*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1318
apply (simp add: takeWhile_tail)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1319
apply (blast intro: Says_K6 dest: servTicket_authentic 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1320
        parts_spies_takeWhile_mono [THEN subsetD] 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1321
        parts_spies_evs_revD2 [THEN subsetD])
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1322
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1323
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1324
lemma A_authenticates_and_keydist_to_B:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1325
     "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1326
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1327
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1328
         Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1329
           \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1330
         Key authK \<notin> analz (spies evs); Key servK \<notin> analz (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1331
         A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1332
      \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1333
by (blast dest!: A_authenticates_B B_Issues_A)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1334
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1335
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1336
(*Must use \<le> rather than =, otherwise it cannot be proved inductively!*)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1337
(*This is too strong for version V but would hold for version IV if only B 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1338
  in K6 said a fresh timestamp.
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1339
lemma honest_never_says_newer_timestamp:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1340
     "\<lbrakk> (CT evs) \<le> T ; Number T \<in> parts {X}; evs \<in> kerbV \<rbrakk> 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1341
     \<Longrightarrow> \<forall> A B. A \<noteq> Spy \<longrightarrow> Says A B X \<notin> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1342
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1343
apply (erule kerbV.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1344
apply (simp_all)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1345
apply force
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1346
apply force
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1347
txt{*clarifying case K3*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1348
apply (rule impI)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1349
apply (rule impI)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1350
apply (frule Suc_leD)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1351
apply (clarify)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1352
txt{*cannot solve K3 or K5 because the spy might send CT evs as authTicket
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1353
or servTicket, which the honest agent would forward*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1354
prefer 2 apply force
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1355
prefer 4 apply force
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1356
prefer 4 apply force
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1357
txt{*cannot solve K6 unless B updates the timestamp - rather than bouncing T3*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1358
oops
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1359
*)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1360
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1361
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1362
text{*But can prove a less general fact conerning only authenticators!*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1363
lemma honest_never_says_newer_timestamp_in_auth:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1364
     "\<lbrakk> (CT evs) \<le> T; Number T \<in> parts {X}; A \<notin> bad; evs \<in> kerbV \<rbrakk> 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1365
     \<Longrightarrow> Says A B \<lbrace>Y, X\<rbrace> \<notin> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1366
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1367
apply (erule kerbV.induct)
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
  1368
apply auto
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1369
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1370
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1371
lemma honest_never_says_current_timestamp_in_auth:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1372
     "\<lbrakk> (CT evs) = T; Number T \<in> parts {X}; A \<notin> bad; evs \<in> kerbV \<rbrakk> 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1373
     \<Longrightarrow> Says A B \<lbrace>Y, X\<rbrace> \<notin> set evs"
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
  1374
by (metis honest_never_says_newer_timestamp_in_auth le_refl)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1375
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1376
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1377
lemma A_Issues_B:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1378
     "\<lbrakk> Says A B \<lbrace>ST, Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1379
         Key servK \<notin> analz (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1380
         B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbV \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1381
   \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1382
apply (simp (no_asm) add: Issues_def)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1383
apply (rule exI)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1384
apply (rule conjI, assumption)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1385
apply (simp (no_asm))
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1386
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1387
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1388
apply (erule kerbV.induct, analz_mono_contra)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1389
apply (frule_tac [7] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1390
apply (frule_tac [5] Says_ticket_parts)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1391
apply (simp_all (no_asm_simp))
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1392
txt{*K5*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1393
apply auto
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1394
apply (simp add: takeWhile_tail)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1395
txt{*Level 15: case study necessary because the assumption doesn't state
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1396
  the form of servTicket. The guarantee becomes stronger.*}
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1397
prefer 2 apply (simp add: takeWhile_tail)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1398
(**This single command of version IV...
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1399
apply (blast dest: Says_imp_spies [THEN analz.Inj, THEN analz_Decrypt']
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1400
                   K3_imp_K2 K4_trustworthy'
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1401
                   parts_spies_takeWhile_mono [THEN subsetD]
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1402
                   parts_spies_evs_revD2 [THEN subsetD]
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1403
             intro: Says_Auth)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1404
...expands as follows - including extra exE because of new form of lemmas*)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1405
apply (frule K3_imp_K2, assumption, assumption, erule exE, erule exE)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1406
apply (case_tac "Key authK \<in> analz (spies evs5)")
32404
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 26300
diff changeset
  1407
 apply (metis Says_imp_analz_Spy analz.Fst analz_Decrypt')
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1408
apply (frule K3_imp_K2, assumption, assumption, erule exE, erule exE)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1409
apply (drule Says_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst])
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1410
apply (frule servK_authentic_ter, blast, assumption+)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1411
apply (drule parts_spies_takeWhile_mono [THEN subsetD])
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1412
apply (drule parts_spies_evs_revD2 [THEN subsetD])
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1413
txt{* @{term Says_K5} closes the proof in version IV because it is clear which 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1414
servTicket an authenticator appears with in msg 5. In version V an authenticator can appear with any item that the spy could replace the servTicket with*}
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
  1415
apply (frule Says_K5, blast)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1416
txt{*We need to state that an honest agent wouldn't send the wrong timestamp
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1417
within an authenticator, wathever it is paired with*}
43587
0dd418de22ce tidied messy proofs
paulson
parents: 41774
diff changeset
  1418
apply (auto simp add: honest_never_says_current_timestamp_in_auth)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1419
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1420
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1421
lemma B_authenticates_and_keydist_to_A:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1422
     "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
  1423
         Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella <