src/HOL/Auth/Kerberos_BAN_Gets.thy
author paulson <lp15@cam.ac.uk>
Wed, 26 Apr 2017 15:53:35 +0100
changeset 65583 8d53b3bebab4
parent 61830 4f5ab843cf5b
child 67613 ce654b0e6d69
permissions -rw-r--r--
Further new material. The simprule status of some exp and ln identities was reverted.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37936
1e4c5015a72e updated some headers;
wenzelm
parents: 36866
diff changeset
     1
(*  Title:      HOL/Auth/Kerberos_BAN_Gets.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
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
     5
section\<open>The Kerberos Protocol, BAN Version, with Gets event\<close>
18886
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 Kerberos_BAN_Gets imports Public begin
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
     8
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
     9
text\<open>From page 251 of
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    10
  Burrows, Abadi and Needham (1989).  A Logic of Authentication.
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    11
  Proc. Royal Soc. 426
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    12
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    13
  Confidentiality (secrecy) and authentication properties rely on
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    14
  temporal checks: strong guarantees in a little abstracted - but
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    15
  very realistic - model.
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
    16
\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    17
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    18
(* Temporal modelization: session keys can be leaked
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    19
                          ONLY when they have expired *)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    20
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    21
consts
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    22
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    23
    (*Duration of the session key*)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    24
    sesKlife   :: nat
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    25
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    26
    (*Duration of the authenticator*)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    27
    authlife :: nat
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    28
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
    29
text\<open>The ticket should remain fresh for two journeys on the network at least\<close>
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
    30
text\<open>The Gets event causes longer traces for the protocol to reach its end\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    31
specification (sesKlife)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    32
  sesKlife_LB [iff]: "4 \<le> sesKlife"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    33
    by blast
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    34
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
    35
text\<open>The authenticator only for one journey\<close>
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
    36
text\<open>The Gets event causes longer traces for the protocol to reach its end\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    37
specification (authlife)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    38
  authlife_LB [iff]:    "2 \<le> authlife"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    39
    by blast
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
20768
1d478c2d621f replaced syntax/translations by abbreviation;
wenzelm
parents: 18886
diff changeset
    42
abbreviation
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20768
diff changeset
    43
  CT :: "event list=>nat" where
20768
1d478c2d621f replaced syntax/translations by abbreviation;
wenzelm
parents: 18886
diff changeset
    44
  "CT == length"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    45
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20768
diff changeset
    46
abbreviation
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20768
diff changeset
    47
  expiredK :: "[nat, event list] => bool" where
20768
1d478c2d621f replaced syntax/translations by abbreviation;
wenzelm
parents: 18886
diff changeset
    48
  "expiredK T evs == sesKlife + T < CT evs"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    49
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20768
diff changeset
    50
abbreviation
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20768
diff changeset
    51
  expiredA :: "[nat, event list] => bool" where
20768
1d478c2d621f replaced syntax/translations by abbreviation;
wenzelm
parents: 18886
diff changeset
    52
  "expiredA T evs == authlife + T < CT evs"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    53
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    54
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 32960
diff changeset
    55
definition
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    56
 (* Yields the subtrace of a given trace from its beginning to a given event *)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    57
  before :: "[event, event list] => event list" ("before _ on _")
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 32960
diff changeset
    58
  where "before ev on evs = takeWhile (% z. z ~= ev) (rev evs)"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    59
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 32960
diff changeset
    60
definition
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    61
 (* States than an event really appears only once on a trace *)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    62
  Unique :: "[event, event list] => bool" ("Unique _ on _")
36866
426d5781bb25 modernized specifications;
wenzelm
parents: 32960
diff changeset
    63
  where "Unique ev on evs = (ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs)))"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    64
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    65
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    66
inductive_set bankerb_gets :: "event list set"
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    67
 where
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    68
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    69
   Nil:  "[] \<in> bankerb_gets"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    70
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    71
 | Fake: "\<lbrakk> evsf \<in> bankerb_gets;  X \<in> synth (analz (knows Spy evsf)) \<rbrakk>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
    72
          \<Longrightarrow> Says Spy B X # evsf \<in> bankerb_gets"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    73
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    74
 | Reception: "\<lbrakk> evsr\<in> bankerb_gets; Says A B X \<in> set evsr \<rbrakk>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    75
                \<Longrightarrow> Gets B X # evsr \<in> bankerb_gets"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    76
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    77
 | BK1:  "\<lbrakk> evs1 \<in> bankerb_gets \<rbrakk>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
    78
          \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B\<rbrace> # evs1
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
    79
                \<in>  bankerb_gets"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    80
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    81
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    82
 | BK2:  "\<lbrakk> evs2 \<in> bankerb_gets;  Key K \<notin> used evs2; K \<in> symKeys;
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
    83
             Gets Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs2 \<rbrakk>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
    84
          \<Longrightarrow> Says Server A
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
    85
                (Crypt (shrK A)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
    86
                   \<lbrace>Number (CT evs2), Agent B, Key K,
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
    87
                    (Crypt (shrK B) \<lbrace>Number (CT evs2), Agent A, Key K\<rbrace>)\<rbrace>)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
    88
                # evs2 \<in> bankerb_gets"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    89
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    90
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    91
 | BK3:  "\<lbrakk> evs3 \<in> bankerb_gets;
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
    92
             Gets A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
    93
               \<in> set evs3;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
    94
             Says A Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs3;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
    95
             \<not> expiredK Tk evs3 \<rbrakk>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
    96
          \<Longrightarrow> Says A B \<lbrace>Ticket, Crypt K \<lbrace>Agent A, Number (CT evs3)\<rbrace> \<rbrace>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
    97
               # evs3 \<in> bankerb_gets"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    98
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
    99
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   100
 | BK4:  "\<lbrakk> evs4 \<in> bankerb_gets;
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
   101
             Gets B \<lbrace>(Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
   102
                         (Crypt K \<lbrace>Agent A, Number Ta\<rbrace>) \<rbrace>: set evs4;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
   103
             \<not> expiredK Tk evs4;  \<not> expiredA Ta evs4 \<rbrakk>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
   104
          \<Longrightarrow> Says B A (Crypt K (Number Ta)) # evs4
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
   105
                \<in> bankerb_gets"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   106
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
   107
        (*Old session keys may become compromised*)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   108
 | Oops: "\<lbrakk> evso \<in> bankerb_gets;
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   109
         Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
   110
               \<in> set evso;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
   111
             expiredK Tk evso \<rbrakk>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
   112
          \<Longrightarrow> Notes Spy \<lbrace>Number Tk, Key K\<rbrace> # evso \<in> bankerb_gets"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   113
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   114
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   115
declare Says_imp_knows_Spy [THEN parts.Inj, dest]
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   116
declare parts.Body [dest]
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   117
declare analz_into_parts [dest]
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   118
declare Fake_parts_insert_in_Un [dest]
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   119
declare knows_Spy_partsEs [elim]
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   120
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   121
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   122
text\<open>A "possibility property": there are traces that reach the end.\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   123
lemma "\<lbrakk>Key K \<notin> used []; K \<in> symKeys\<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   124
       \<Longrightarrow> \<exists>Timestamp. \<exists>evs \<in> bankerb_gets.
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   125
             Says B A (Crypt K (Number Timestamp))
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   126
                  \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   127
apply (cut_tac sesKlife_LB)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   128
apply (cut_tac authlife_LB)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   129
apply (intro exI bexI)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   130
apply (rule_tac [2]
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   131
           bankerb_gets.Nil [THEN bankerb_gets.BK1, THEN bankerb_gets.Reception,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   132
                            THEN bankerb_gets.BK2, THEN bankerb_gets.Reception,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   133
                            THEN bankerb_gets.BK3, THEN bankerb_gets.Reception,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   134
                            THEN bankerb_gets.BK4])
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   135
apply (possibility, simp_all (no_asm_simp) add: used_Cons)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   136
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   137
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   138
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   139
text\<open>Lemmas about reception invariant: if a message is received it certainly
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   140
was sent\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   141
lemma Gets_imp_Says :
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   142
     "\<lbrakk> Gets B X \<in> set evs; evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> \<exists>A. Says A B X \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   143
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   144
apply (erule bankerb_gets.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   145
apply auto
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   146
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   147
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   148
lemma Gets_imp_knows_Spy: 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   149
     "\<lbrakk> Gets B X \<in> set evs; evs \<in> bankerb_gets \<rbrakk>  \<Longrightarrow> X \<in> knows Spy evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   150
apply (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   151
done
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
lemma Gets_imp_knows_Spy_parts[dest]:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   154
    "\<lbrakk> Gets B X \<in> set evs; evs \<in> bankerb_gets \<rbrakk>  \<Longrightarrow> X \<in> parts (knows Spy evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   155
apply (blast dest: Gets_imp_knows_Spy [THEN parts.Inj])
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   156
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   157
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   158
lemma Gets_imp_knows:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   159
     "\<lbrakk> Gets B X \<in> set evs; evs \<in> bankerb_gets \<rbrakk>  \<Longrightarrow> X \<in> knows B evs"
39251
8756b44582e2 Tidied up proofs using sledgehammer, also deleting unnecessary semicolons
paulson
parents: 37936
diff changeset
   160
by (metis Gets_imp_knows_Spy Gets_imp_knows_agents)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   161
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   162
lemma Gets_imp_knows_analz:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   163
    "\<lbrakk> Gets B X \<in> set evs; evs \<in> bankerb_gets \<rbrakk>  \<Longrightarrow> X \<in> analz (knows B evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   164
apply (blast dest: Gets_imp_knows [THEN analz.Inj])
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   165
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   166
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   167
text\<open>Lemmas for reasoning about predicate "before"\<close>
39251
8756b44582e2 Tidied up proofs using sledgehammer, also deleting unnecessary semicolons
paulson
parents: 37936
diff changeset
   168
lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   169
apply (induct_tac "evs")
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   170
apply simp
55417
01fbfb60c33e adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents: 44890
diff changeset
   171
apply (rename_tac a b)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   172
apply (induct_tac "a")
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   173
apply auto
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   174
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   175
39251
8756b44582e2 Tidied up proofs using sledgehammer, also deleting unnecessary semicolons
paulson
parents: 37936
diff changeset
   176
lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   177
apply (induct_tac "evs")
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   178
apply simp
55417
01fbfb60c33e adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents: 44890
diff changeset
   179
apply (rename_tac a b)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   180
apply (induct_tac "a")
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   181
apply auto
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   182
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   183
39251
8756b44582e2 Tidied up proofs using sledgehammer, also deleting unnecessary semicolons
paulson
parents: 37936
diff changeset
   184
lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   185
apply (induct_tac "evs")
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   186
apply simp
55417
01fbfb60c33e adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents: 44890
diff changeset
   187
apply (rename_tac a b)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   188
apply (induct_tac "a")
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   189
apply auto
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   190
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   191
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   192
lemma used_evs_rev: "used evs = used (rev evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   193
apply (induct_tac "evs")
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   194
apply simp
55417
01fbfb60c33e adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents: 44890
diff changeset
   195
apply (rename_tac a b)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   196
apply (induct_tac "a")
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   197
apply (simp add: used_Says_rev)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   198
apply (simp add: used_Gets_rev)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   199
apply (simp add: used_Notes_rev)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   200
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   201
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   202
lemma used_takeWhile_used [rule_format]: 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   203
      "x : used (takeWhile P X) --> x : used X"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   204
apply (induct_tac "X")
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   205
apply simp
55417
01fbfb60c33e adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents: 44890
diff changeset
   206
apply (rename_tac a b)
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   207
apply (induct_tac "a")
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   208
apply (simp_all add: used_Nil)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   209
apply (blast dest!: initState_into_used)+
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   210
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   211
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   212
lemma set_evs_rev: "set evs = set (rev evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   213
apply auto
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   214
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   215
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   216
lemma takeWhile_void [rule_format]:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   217
      "x \<notin> set evs \<longrightarrow> takeWhile (\<lambda>z. z \<noteq> x) evs = evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   218
apply auto
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   219
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   220
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   221
(**** Inductive proofs about bankerb_gets ****)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   222
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   223
text\<open>Forwarding Lemma for reasoning about the encrypted portion of message BK3\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   224
lemma BK3_msg_in_parts_knows_Spy:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   225
     "\<lbrakk>Gets A (Crypt KA \<lbrace>Timestamp, B, K, X\<rbrace>) \<in> set evs; evs \<in> bankerb_gets \<rbrakk> 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   226
      \<Longrightarrow> X \<in> parts (knows Spy evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   227
apply blast
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
lemma Oops_parts_knows_Spy:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   231
     "Says Server A (Crypt (shrK A) \<lbrace>Timestamp, B, K, X\<rbrace>) \<in> set evs
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   232
      \<Longrightarrow> K \<in> parts (knows Spy evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   233
apply blast
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   234
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   235
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   236
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   237
text\<open>Spy never sees another agent's shared key! (unless it's bad at start)\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   238
lemma Spy_see_shrK [simp]:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   239
     "evs \<in> bankerb_gets \<Longrightarrow> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   240
apply (erule bankerb_gets.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   241
apply (frule_tac [8] Oops_parts_knows_Spy)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   242
apply (frule_tac [6] BK3_msg_in_parts_knows_Spy, simp_all, blast+)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   243
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   244
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 Spy_analz_shrK [simp]:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   247
     "evs \<in> bankerb_gets \<Longrightarrow> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   248
by auto
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   249
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   250
lemma Spy_see_shrK_D [dest!]:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   251
     "\<lbrakk> Key (shrK A) \<in> parts (knows Spy evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   252
                evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> A:bad"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   253
by (blast dest: Spy_see_shrK)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   254
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   255
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
   256
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   257
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   258
text\<open>Nobody can have used non-existent keys!\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   259
lemma new_keys_not_used [simp]:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   260
    "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> bankerb_gets\<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   261
     \<Longrightarrow> K \<notin> keysFor (parts (knows Spy evs))"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   262
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   263
apply (erule bankerb_gets.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   264
apply (frule_tac [8] Oops_parts_knows_Spy)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   265
apply (frule_tac [6] BK3_msg_in_parts_knows_Spy, simp_all)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   266
txt\<open>Fake\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   267
apply (force dest!: keysFor_parts_insert)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   268
txt\<open>BK2, BK3, BK4\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   269
apply (force dest!: analz_shrK_Decrypt)+
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   270
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   271
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   272
subsection\<open>Lemmas concerning the form of items passed in messages\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   273
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   274
text\<open>Describes the form of K, X and K' when the Server sends this message.\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   275
lemma Says_Server_message_form:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   276
     "\<lbrakk> Says Server A (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   277
         \<in> set evs; evs \<in> bankerb_gets \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   278
      \<Longrightarrow> K' = shrK A & K \<notin> range shrK &
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   279
          Ticket = (Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>) &
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   280
          Key K \<notin> used(before
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   281
                  Says Server A (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   282
                  on evs) &
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   283
          Tk = CT(before 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   284
                  Says Server A (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   285
                  on evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   286
apply (unfold before_def)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   287
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   288
apply (erule bankerb_gets.induct, simp_all)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   289
txt\<open>We need this simplification only for Message 2\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   290
apply (simp (no_asm) add: takeWhile_tail)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   291
apply auto
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   292
txt\<open>Two subcases of Message 2. Subcase: used before\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   293
apply (blast dest: used_evs_rev [THEN equalityD2, THEN contra_subsetD] 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   294
                   used_takeWhile_used)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   295
txt\<open>subcase: CT before\<close>
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 39251
diff changeset
   296
apply (fastforce dest!: set_evs_rev [THEN equalityD2, THEN contra_subsetD, THEN takeWhile_void])
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   297
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   298
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   299
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   300
text\<open>If the encrypted message appears then it originated with the Server
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   301
  PROVIDED that A is NOT compromised!
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   302
  This allows A to verify freshness of the session key.
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   303
\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   304
lemma Kab_authentic:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   305
     "\<lbrakk> Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   306
           \<in> parts (knows Spy evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   307
         A \<notin> bad;  evs \<in> bankerb_gets \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   308
       \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   309
             \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   310
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   311
apply (erule bankerb_gets.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   312
apply (frule_tac [8] Oops_parts_knows_Spy)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   313
apply (frule_tac [6] BK3_msg_in_parts_knows_Spy, simp_all, blast)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   314
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   315
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   316
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   317
text\<open>If the TICKET appears then it originated with the Server\<close>
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   318
text\<open>FRESHNESS OF THE SESSION KEY to B\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   319
lemma ticket_authentic:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   320
     "\<lbrakk> Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> \<in> parts (knows Spy evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   321
         B \<notin> bad;  evs \<in> bankerb_gets \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   322
       \<Longrightarrow> Says Server A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   323
            (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   324
                          Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>\<rbrace>)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   325
           \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   326
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   327
apply (erule bankerb_gets.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   328
apply (frule_tac [8] Oops_parts_knows_Spy)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   329
apply (frule_tac [6] BK3_msg_in_parts_knows_Spy, simp_all, blast)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   330
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   331
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   332
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   333
text\<open>EITHER describes the form of X when the following message is sent,
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   334
  OR     reduces it to the Fake case.
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   335
  Use \<open>Says_Server_message_form\<close> if applicable.\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   336
lemma Gets_Server_message_form:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   337
     "\<lbrakk> Gets A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   338
            \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   339
         evs \<in> bankerb_gets \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   340
 \<Longrightarrow> (K \<notin> range shrK & X = (Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>))
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   341
          | X \<in> analz (knows Spy evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   342
apply (case_tac "A \<in> bad")
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   343
apply (force dest!: Gets_imp_knows_Spy [THEN analz.Inj])
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   344
apply (blast dest!: Kab_authentic Says_Server_message_form)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   345
done
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
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   348
text\<open>Reliability guarantees: honest agents act as we expect\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   349
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   350
lemma BK3_imp_Gets:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   351
   "\<lbrakk> Says A B \<lbrace>Ticket, Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   352
      A \<notin> bad; evs \<in> bankerb_gets \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   353
    \<Longrightarrow> \<exists> Tk. Gets A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<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
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   356
apply (erule bankerb_gets.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   357
apply auto
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   358
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   359
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   360
lemma BK4_imp_Gets:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   361
   "\<lbrakk> Says B A (Crypt K (Number Ta)) \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   362
      B \<notin> bad; evs \<in> bankerb_gets \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   363
  \<Longrightarrow> \<exists> Tk. Gets B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>,
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23746
diff changeset
   364
                    Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs"
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   365
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   366
apply (erule bankerb_gets.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   367
apply auto
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   368
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   369
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   370
lemma Gets_A_knows_K:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   371
  "\<lbrakk> Gets A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   372
     evs \<in> bankerb_gets \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   373
 \<Longrightarrow> Key K \<in> analz (knows A evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   374
apply (force dest: Gets_imp_knows_analz)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   375
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   376
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   377
lemma Gets_B_knows_K:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   378
  "\<lbrakk> Gets B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   379
             Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   380
     evs \<in> bankerb_gets \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   381
 \<Longrightarrow> Key K \<in> analz (knows B evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   382
apply (force dest: Gets_imp_knows_analz)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   383
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   384
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
(****
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   387
 The following is to prove theorems of the form
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   388
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   389
  Key K \<in> analz (insert (Key KAB) (knows Spy evs)) \<Longrightarrow>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   390
  Key K \<in> analz (knows Spy evs)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   391
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   392
 A more general formula must be proved inductively.
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   393
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   394
****)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   395
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   396
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   397
text\<open>Session keys are not used to encrypt other session keys\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   398
lemma analz_image_freshK [rule_format (no_asm)]:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   399
     "evs \<in> bankerb_gets \<Longrightarrow>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   400
   \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   401
          (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   402
          (K \<in> KK | Key K \<in> analz (knows Spy evs))"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   403
apply (erule bankerb_gets.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   404
apply (drule_tac [8] Says_Server_message_form)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   405
apply (erule_tac [6] Gets_Server_message_form [THEN disjE], analz_freshK, spy_analz, auto) 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   406
done
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
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   409
lemma analz_insert_freshK:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   410
     "\<lbrakk> evs \<in> bankerb_gets;  KAB \<notin> range shrK \<rbrakk> \<Longrightarrow>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   411
      (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   412
      (K = KAB | Key K \<in> analz (knows Spy evs))"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   413
by (simp only: analz_image_freshK analz_image_freshK_simps)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   414
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   415
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   416
text\<open>The session key K uniquely identifies the message\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   417
lemma unique_session_keys:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   418
     "\<lbrakk> Says Server A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   419
           (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   420
         Says Server A'
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   421
          (Crypt (shrK A') \<lbrace>Number Tk', Agent B', Key K, X'\<rbrace>) \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   422
         evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> A=A' & Tk=Tk' & B=B' & X = X'"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   423
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   424
apply (erule rev_mp)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   425
apply (erule bankerb_gets.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   426
apply (frule_tac [8] Oops_parts_knows_Spy)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   427
apply (frule_tac [6] BK3_msg_in_parts_knows_Spy, simp_all)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   428
txt\<open>BK2: it can't be a new key\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   429
apply blast
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   430
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   431
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   432
lemma unique_session_keys_Gets:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   433
     "\<lbrakk> Gets A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   434
           (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   435
        Gets A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   436
          (Crypt (shrK A) \<lbrace>Number Tk', Agent B', Key K, X'\<rbrace>) \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   437
        A \<notin> bad; evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> Tk=Tk' & B=B' & X = X'"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   438
apply (blast dest!: Kab_authentic unique_session_keys)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   439
done
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
lemma Server_Unique:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   443
     "\<lbrakk> Says Server A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   444
            (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   445
        evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   446
   Unique Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   447
   on evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   448
apply (erule rev_mp, erule bankerb_gets.induct, simp_all add: Unique_def)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   449
apply blast
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   450
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   451
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   452
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   453
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   454
subsection\<open>Non-temporal guarantees, explicitly relying on non-occurrence of
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   455
oops events - refined below by temporal guarantees\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   456
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   457
text\<open>Non temporal treatment of confidentiality\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   458
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   459
text\<open>Lemma: the session key sent in msg BK2 would be lost by oops
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   460
    if the spy could see it!\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   461
lemma lemma_conf [rule_format (no_asm)]:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   462
     "\<lbrakk> A \<notin> bad;  B \<notin> bad;  evs \<in> bankerb_gets \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   463
  \<Longrightarrow> Says Server A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   464
          (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   465
                            Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>\<rbrace>)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   466
         \<in> set evs \<longrightarrow>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   467
      Key K \<in> analz (knows Spy evs) \<longrightarrow> Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   468
apply (erule bankerb_gets.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   469
apply (frule_tac [8] Says_Server_message_form)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   470
apply (frule_tac [6] Gets_Server_message_form [THEN disjE])
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   471
apply (simp_all (no_asm_simp) add: analz_insert_eq analz_insert_freshK pushes)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   472
txt\<open>Fake\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   473
apply spy_analz
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   474
txt\<open>BK2\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   475
apply (blast intro: parts_insertI)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   476
txt\<open>BK3\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   477
apply (case_tac "Aa \<in> bad")
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   478
 prefer 2 apply (blast dest: Kab_authentic unique_session_keys)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   479
apply (blast dest: Gets_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad elim!: MPair_analz)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   480
txt\<open>Oops\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   481
apply (blast dest: unique_session_keys)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   482
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   483
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   484
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   485
text\<open>Confidentiality for the Server: Spy does not see the keys sent in msg BK2
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   486
as long as they have not expired.\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   487
lemma Confidentiality_S:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   488
     "\<lbrakk> Says Server A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   489
          (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   490
        Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   491
         A \<notin> bad;  B \<notin> bad;  evs \<in> bankerb_gets
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   492
      \<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   493
apply (frule Says_Server_message_form, assumption)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   494
apply (blast intro: lemma_conf)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   495
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   496
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   497
text\<open>Confidentiality for Alice\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   498
lemma Confidentiality_A:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   499
     "\<lbrakk> Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> \<in> parts (knows Spy evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   500
        Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   501
        A \<notin> bad;  B \<notin> bad;  evs \<in> bankerb_gets
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   502
      \<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   503
by (blast dest!: Kab_authentic Confidentiality_S)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   504
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   505
text\<open>Confidentiality for Bob\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   506
lemma Confidentiality_B:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   507
     "\<lbrakk> Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   508
          \<in> parts (knows Spy evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   509
        Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   510
        A \<notin> bad;  B \<notin> bad;  evs \<in> bankerb_gets
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   511
      \<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   512
by (blast dest!: ticket_authentic Confidentiality_S)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   513
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   514
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   515
text\<open>Non temporal treatment of authentication\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   516
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   517
text\<open>Lemmas \<open>lemma_A\<close> and \<open>lemma_B\<close> in fact are common to both temporal and non-temporal treatments\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   518
lemma lemma_A [rule_format]:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   519
     "\<lbrakk> A \<notin> bad; B \<notin> bad; evs \<in> bankerb_gets \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   520
      \<Longrightarrow>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   521
         Key K \<notin> analz (knows Spy evs) \<longrightarrow>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   522
         Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   523
         \<in> set evs \<longrightarrow>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   524
          Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   525
         Says A B \<lbrace>X, Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   526
             \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   527
apply (erule bankerb_gets.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   528
apply (frule_tac [8] Oops_parts_knows_Spy)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   529
apply (frule_tac [6] Gets_Server_message_form)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   530
apply (frule_tac [7] BK3_msg_in_parts_knows_Spy, analz_mono_contra)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   531
apply (simp_all (no_asm_simp) add: all_conj_distrib)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   532
txt\<open>Fake\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   533
apply blast
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   534
txt\<open>BK2\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   535
apply (force dest: Crypt_imp_invKey_keysFor)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   536
txt\<open>BK3\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   537
apply (blast dest: Kab_authentic unique_session_keys)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   538
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   539
lemma lemma_B [rule_format]:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   540
     "\<lbrakk> B \<notin> bad;  evs \<in> bankerb_gets \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   541
      \<Longrightarrow> Key K \<notin> analz (knows Spy evs) \<longrightarrow>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   542
          Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   543
          \<in> set evs \<longrightarrow>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   544
          Crypt K (Number Ta) \<in> parts (knows Spy evs) \<longrightarrow>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   545
          Says B A (Crypt K (Number Ta)) \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   546
apply (erule bankerb_gets.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   547
apply (frule_tac [8] Oops_parts_knows_Spy)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   548
apply (frule_tac [6] Gets_Server_message_form)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   549
apply (drule_tac [7] BK3_msg_in_parts_knows_Spy, analz_mono_contra)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   550
apply (simp_all (no_asm_simp) add: all_conj_distrib)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   551
txt\<open>Fake\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   552
apply blast
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   553
txt\<open>BK2\<close> 
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   554
apply (force dest: Crypt_imp_invKey_keysFor)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   555
txt\<open>BK4\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   556
apply (blast dest: ticket_authentic unique_session_keys
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   557
                   Gets_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   558
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   559
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   560
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   561
text\<open>The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   562
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   563
text\<open>Authentication of A to B\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   564
lemma B_authenticates_A_r:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   565
     "\<lbrakk> Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (knows Spy evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   566
         Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>  \<in> parts (knows Spy evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   567
        Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   568
         A \<notin> bad;  B \<notin> bad;  evs \<in> bankerb_gets \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   569
      \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   570
                     Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   571
by (blast dest!: ticket_authentic
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   572
          intro!: lemma_A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   573
          elim!: Confidentiality_S [THEN [2] rev_notE])
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   574
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   575
text\<open>Authentication of B to A\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   576
lemma A_authenticates_B_r:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   577
     "\<lbrakk> Crypt K (Number Ta) \<in> parts (knows Spy evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   578
        Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> \<in> parts (knows Spy evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   579
        Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   580
        A \<notin> bad;  B \<notin> bad;  evs \<in> bankerb_gets \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   581
      \<Longrightarrow> Says B A (Crypt K (Number Ta)) \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   582
by (blast dest!: Kab_authentic
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   583
          intro!: lemma_B elim!: Confidentiality_S [THEN [2] rev_notE])
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   584
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   585
lemma B_authenticates_A:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   586
     "\<lbrakk> Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   587
         Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>  \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   588
        Key K \<notin> analz (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   589
         A \<notin> bad;  B \<notin> bad;  evs \<in> bankerb_gets \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   590
      \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   591
                     Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   592
apply (blast dest!: ticket_authentic intro!: lemma_A)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   593
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   594
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   595
lemma A_authenticates_B:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   596
     "\<lbrakk> Crypt K (Number Ta) \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   597
        Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   598
        Key K \<notin> analz (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   599
        A \<notin> bad;  B \<notin> bad;  evs \<in> bankerb_gets \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   600
      \<Longrightarrow> Says B A (Crypt K (Number Ta)) \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   601
apply (blast dest!: Kab_authentic intro!: lemma_B)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   602
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   603
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   604
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   605
subsection\<open>Temporal guarantees, relying on a temporal check that insures that
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   606
no oops event occurred. These are available in the sense of goal availability\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   607
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   608
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   609
text\<open>Temporal treatment of confidentiality\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   610
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   611
text\<open>Lemma: the session key sent in msg BK2 would be EXPIRED
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   612
    if the spy could see it!\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   613
lemma lemma_conf_temporal [rule_format (no_asm)]:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   614
     "\<lbrakk> A \<notin> bad;  B \<notin> bad;  evs \<in> bankerb_gets \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   615
  \<Longrightarrow> Says Server A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   616
          (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   617
                            Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>\<rbrace>)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   618
         \<in> set evs \<longrightarrow>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   619
      Key K \<in> analz (knows Spy evs) \<longrightarrow> expiredK Tk evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   620
apply (erule bankerb_gets.induct)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   621
apply (frule_tac [8] Says_Server_message_form)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   622
apply (frule_tac [6] Gets_Server_message_form [THEN disjE])
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   623
apply (simp_all (no_asm_simp) add: less_SucI analz_insert_eq analz_insert_freshK pushes)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   624
txt\<open>Fake\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   625
apply spy_analz
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   626
txt\<open>BK2\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   627
apply (blast intro: parts_insertI less_SucI)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   628
txt\<open>BK3\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   629
apply (case_tac "Aa \<in> bad")
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   630
 prefer 2 apply (blast dest: Kab_authentic unique_session_keys)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   631
apply (blast dest: Gets_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad elim!: MPair_analz intro: less_SucI)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   632
txt\<open>Oops: PROOF FAILS if unsafe intro below\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   633
apply (blast dest: unique_session_keys intro!: less_SucI)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   634
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   635
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   636
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   637
text\<open>Confidentiality for the Server: Spy does not see the keys sent in msg BK2
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   638
as long as they have not expired.\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   639
lemma Confidentiality_S_temporal:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   640
     "\<lbrakk> Says Server A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   641
          (Crypt K' \<lbrace>Number T, Agent B, Key K, X\<rbrace>) \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   642
         \<not> expiredK T evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   643
         A \<notin> bad;  B \<notin> bad;  evs \<in> bankerb_gets
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   644
      \<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   645
apply (frule Says_Server_message_form, assumption)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   646
apply (blast intro: lemma_conf_temporal)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   647
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   648
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   649
text\<open>Confidentiality for Alice\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   650
lemma Confidentiality_A_temporal:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   651
     "\<lbrakk> Crypt (shrK A) \<lbrace>Number T, Agent B, Key K, X\<rbrace> \<in> parts (knows Spy evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   652
         \<not> expiredK T evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   653
         A \<notin> bad;  B \<notin> bad;  evs \<in> bankerb_gets
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   654
      \<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   655
by (blast dest!: Kab_authentic Confidentiality_S_temporal)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   656
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   657
text\<open>Confidentiality for Bob\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   658
lemma Confidentiality_B_temporal:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   659
     "\<lbrakk> Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   660
          \<in> parts (knows Spy evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   661
        \<not> expiredK Tk evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   662
        A \<notin> bad;  B \<notin> bad;  evs \<in> bankerb_gets
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   663
      \<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   664
by (blast dest!: ticket_authentic Confidentiality_S_temporal)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   665
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   666
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   667
text\<open>Temporal treatment of authentication\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   668
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   669
text\<open>Authentication of A to B\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   670
lemma B_authenticates_A_temporal:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   671
     "\<lbrakk> Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (knows Spy evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   672
         Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   673
         \<in> parts (knows Spy evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   674
         \<not> expiredK Tk evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   675
         A \<notin> bad;  B \<notin> bad;  evs \<in> bankerb_gets \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   676
      \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   677
                     Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   678
by (blast dest!: ticket_authentic
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   679
          intro!: lemma_A
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   680
          elim!: Confidentiality_S_temporal [THEN [2] rev_notE])
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   681
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   682
text\<open>Authentication of B to A\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   683
lemma A_authenticates_B_temporal:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   684
     "\<lbrakk> Crypt K (Number Ta) \<in> parts (knows Spy evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   685
         Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   686
         \<in> parts (knows Spy evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   687
         \<not> expiredK Tk evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   688
         A \<notin> bad;  B \<notin> bad;  evs \<in> bankerb_gets \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   689
      \<Longrightarrow> Says B A (Crypt K (Number Ta)) \<in> set evs"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   690
by (blast dest!: Kab_authentic
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   691
          intro!: lemma_B elim!: Confidentiality_S_temporal [THEN [2] rev_notE])
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   692
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   693
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
   694
subsection\<open>Combined guarantees of key distribution and non-injective agreement on the session keys\<close>
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   695
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   696
lemma B_authenticates_and_keydist_to_A:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   697
     "\<lbrakk> Gets B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   698
                Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   699
        Key K \<notin> analz (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   700
        A \<notin> bad;  B \<notin> bad;  evs \<in> bankerb_gets \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   701
    \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>,
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   702
                  Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs 
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   703
     \<and>  Key K \<in> analz (knows A evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   704
apply (blast dest: B_authenticates_A BK3_imp_Gets Gets_A_knows_K)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   705
done
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   706
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   707
lemma A_authenticates_and_keydist_to_B:
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   708
     "\<lbrakk> Gets A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   709
        Gets A (Crypt K (Number Ta)) \<in> set evs;
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   710
        Key K \<notin> analz (spies evs);
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   711
        A \<notin> bad;  B \<notin> bad;  evs \<in> bankerb_gets \<rbrakk>
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   712
    \<Longrightarrow> Says B A (Crypt K (Number Ta)) \<in> set evs
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   713
    \<and>   Key K \<in> analz (knows B evs)"
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   714
apply (blast dest: A_authenticates_B BK4_imp_Gets Gets_B_knows_K)
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   715
done
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
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   719
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   720
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents:
diff changeset
   721
end