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