src/HOL/Auth/Guard/Guard_OtwayRees.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 58889 5b7a9633cfa8
child 61830 4f5ab843cf5b
permissions -rw-r--r--
prefer symbols;
wenzelm@41775
     1
(*  Title:      HOL/Auth/Guard/Guard_OtwayRees.thy
wenzelm@41775
     2
    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
wenzelm@41775
     3
    Copyright   2002  University of Cambridge
wenzelm@41775
     4
*)
wenzelm@17394
     5
wenzelm@58889
     6
section{*Otway-Rees Protocol*}
wenzelm@17394
     7
wenzelm@17394
     8
theory Guard_OtwayRees imports Guard_Shared begin
wenzelm@17394
     9
wenzelm@17394
    10
subsection{*messages used in the protocol*}
wenzelm@17394
    11
wenzelm@20768
    12
abbreviation
wenzelm@21404
    13
  nil :: "msg" where
wenzelm@20768
    14
  "nil == Number 0"
wenzelm@17394
    15
wenzelm@21404
    16
abbreviation
wenzelm@21404
    17
  or1 :: "agent => agent => nat => event" where
wenzelm@20768
    18
  "or1 A B NA ==
wenzelm@20768
    19
    Says A B {|Nonce NA, Agent A, Agent B, Ciph A {|Nonce NA, Agent A, Agent B|}|}"
wenzelm@17394
    20
wenzelm@21404
    21
abbreviation
wenzelm@21404
    22
  or1' :: "agent => agent => agent => nat => msg => event" where
wenzelm@20768
    23
  "or1' A' A B NA X == Says A' B {|Nonce NA, Agent A, Agent B, X|}"
wenzelm@17394
    24
wenzelm@21404
    25
abbreviation
wenzelm@21404
    26
  or2 :: "agent => agent => nat => nat => msg => event" where
wenzelm@20768
    27
  "or2 A B NA NB X ==
wenzelm@20768
    28
    Says B Server {|Nonce NA, Agent A, Agent B, X,
wenzelm@17394
    29
                    Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
wenzelm@17394
    30
wenzelm@21404
    31
abbreviation
wenzelm@21404
    32
  or2' :: "agent => agent => agent => nat => nat => event" where
wenzelm@20768
    33
  "or2' B' A B NA NB ==
wenzelm@20768
    34
    Says B' Server {|Nonce NA, Agent A, Agent B,
wenzelm@17394
    35
                     Ciph A {|Nonce NA, Agent A, Agent B|},
wenzelm@17394
    36
                     Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
wenzelm@17394
    37
wenzelm@21404
    38
abbreviation
wenzelm@21404
    39
  or3 :: "agent => agent => nat => nat => key => event" where
wenzelm@20768
    40
  "or3 A B NA NB K ==
wenzelm@20768
    41
    Says Server B {|Nonce NA, Ciph A {|Nonce NA, Key K|},
wenzelm@17394
    42
                    Ciph B {|Nonce NB, Key K|}|}"
wenzelm@17394
    43
wenzelm@21404
    44
abbreviation
wenzelm@21404
    45
  or3':: "agent => msg => agent => agent => nat => nat => key => event" where
wenzelm@20768
    46
  "or3' S Y A B NA NB K ==
wenzelm@20768
    47
    Says S B {|Nonce NA, Y, Ciph B {|Nonce NB, Key K|}|}"
wenzelm@17394
    48
wenzelm@21404
    49
abbreviation
wenzelm@21404
    50
  or4 :: "agent => agent => nat => msg => event" where
wenzelm@20768
    51
  "or4 A B NA X == Says B A {|Nonce NA, X, nil|}"
wenzelm@17394
    52
wenzelm@21404
    53
abbreviation
wenzelm@21404
    54
  or4' :: "agent => agent => nat => key => event" where
wenzelm@20768
    55
  "or4' B' A NA K == Says B' A {|Nonce NA, Ciph A {|Nonce NA, Key K|}, nil|}"
wenzelm@17394
    56
wenzelm@17394
    57
subsection{*definition of the protocol*}
wenzelm@17394
    58
berghofe@23746
    59
inductive_set or :: "event list set"
berghofe@23746
    60
where
wenzelm@17394
    61
berghofe@23746
    62
  Nil: "[]:or"
wenzelm@17394
    63
berghofe@23746
    64
| Fake: "[| evs:or; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:or"
wenzelm@17394
    65
berghofe@23746
    66
| OR1: "[| evs1:or; Nonce NA ~:used evs1 |] ==> or1 A B NA # evs1:or"
wenzelm@17394
    67
berghofe@23746
    68
| OR2: "[| evs2:or; or1' A' A B NA X:set evs2; Nonce NB ~:used evs2 |]
berghofe@23746
    69
  ==> or2 A B NA NB X # evs2:or"
wenzelm@17394
    70
berghofe@23746
    71
| OR3: "[| evs3:or; or2' B' A B NA NB:set evs3; Key K ~:used evs3 |]
berghofe@23746
    72
  ==> or3 A B NA NB K # evs3:or"
wenzelm@17394
    73
berghofe@23746
    74
| OR4: "[| evs4:or; or2 A B NA NB X:set evs4; or3' S Y A B NA NB K:set evs4 |]
berghofe@23746
    75
  ==> or4 A B NA X # evs4:or"
wenzelm@17394
    76
wenzelm@17394
    77
subsection{*declarations for tactics*}
wenzelm@17394
    78
wenzelm@17394
    79
declare knows_Spy_partsEs [elim]
wenzelm@17394
    80
declare Fake_parts_insert [THEN subsetD, dest]
wenzelm@17394
    81
declare initState.simps [simp del]
wenzelm@17394
    82
wenzelm@17394
    83
subsection{*general properties of or*}
wenzelm@17394
    84
wenzelm@17394
    85
lemma or_has_no_Gets: "evs:or ==> ALL A X. Gets A X ~:set evs"
wenzelm@17394
    86
by (erule or.induct, auto)
wenzelm@17394
    87
wenzelm@17394
    88
lemma or_is_Gets_correct [iff]: "Gets_correct or"
wenzelm@17394
    89
by (auto simp: Gets_correct_def dest: or_has_no_Gets)
wenzelm@17394
    90
wenzelm@17394
    91
lemma or_is_one_step [iff]: "one_step or"
berghofe@23746
    92
by (unfold one_step_def, clarify, ind_cases "ev#evs:or" for ev evs, auto)
wenzelm@17394
    93
wenzelm@17394
    94
lemma or_has_only_Says' [rule_format]: "evs:or ==>
wenzelm@17394
    95
ev:set evs --> (EX A B X. ev=Says A B X)"
wenzelm@17394
    96
by (erule or.induct, auto)
wenzelm@17394
    97
wenzelm@17394
    98
lemma or_has_only_Says [iff]: "has_only_Says or"
wenzelm@17394
    99
by (auto simp: has_only_Says_def dest: or_has_only_Says')
wenzelm@17394
   100
wenzelm@17394
   101
subsection{*or is regular*}
wenzelm@17394
   102
wenzelm@17394
   103
lemma or1'_parts_spies [dest]: "or1' A' A B NA X:set evs
wenzelm@17394
   104
==> X:parts (spies evs)"
wenzelm@17394
   105
by blast
wenzelm@17394
   106
wenzelm@17394
   107
lemma or2_parts_spies [dest]: "or2 A B NA NB X:set evs
wenzelm@17394
   108
==> X:parts (spies evs)"
wenzelm@17394
   109
by blast
wenzelm@17394
   110
wenzelm@17394
   111
lemma or3_parts_spies [dest]: "Says S B {|NA, Y, Ciph B {|NB, K|}|}:set evs
wenzelm@17394
   112
==> K:parts (spies evs)"
wenzelm@17394
   113
by blast
wenzelm@17394
   114
wenzelm@17394
   115
lemma or_is_regular [iff]: "regular or"
wenzelm@17394
   116
apply (simp only: regular_def, clarify)
wenzelm@17394
   117
apply (erule or.induct, simp_all add: initState.simps knows.simps)
wenzelm@17394
   118
by (auto dest: parts_sub)
wenzelm@17394
   119
wenzelm@17394
   120
subsection{*guardedness of KAB*}
wenzelm@17394
   121
wenzelm@17394
   122
lemma Guard_KAB [rule_format]: "[| evs:or; A ~:bad; B ~:bad |] ==>
wenzelm@17394
   123
or3 A B NA NB K:set evs --> GuardK K {shrK A,shrK B} (spies evs)" 
wenzelm@17394
   124
apply (erule or.induct)
wenzelm@17394
   125
(* Nil *)
wenzelm@17394
   126
apply simp_all
wenzelm@17394
   127
(* Fake *)
wenzelm@17394
   128
apply (clarify, erule in_synth_GuardK, erule GuardK_analz, simp)
wenzelm@17394
   129
(* OR1 *)
wenzelm@17394
   130
apply blast
wenzelm@17394
   131
(* OR2 *)
wenzelm@17394
   132
apply safe
wenzelm@17394
   133
apply (blast dest: Says_imp_spies, blast)
wenzelm@17394
   134
(* OR3 *)
wenzelm@17394
   135
apply blast
wenzelm@17394
   136
apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
wenzelm@17394
   137
apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
wenzelm@17394
   138
(* OR4 *)
wenzelm@17394
   139
by (blast dest: Says_imp_spies in_GuardK_kparts)
wenzelm@17394
   140
wenzelm@17394
   141
subsection{*guardedness of NB*}
wenzelm@17394
   142
wenzelm@17394
   143
lemma Guard_NB [rule_format]: "[| evs:or; B ~:bad |] ==>
wenzelm@17394
   144
or2 A B NA NB X:set evs --> Guard NB {shrK B} (spies evs)" 
wenzelm@17394
   145
apply (erule or.induct)
wenzelm@17394
   146
(* Nil *)
wenzelm@17394
   147
apply simp_all
wenzelm@17394
   148
(* Fake *)
wenzelm@17394
   149
apply safe
wenzelm@17394
   150
apply (erule in_synth_Guard, erule Guard_analz, simp)
wenzelm@17394
   151
(* OR1 *)
wenzelm@17394
   152
apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp)
wenzelm@17394
   153
apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp)
wenzelm@17394
   154
(* OR2 *)
wenzelm@17394
   155
apply blast
wenzelm@17394
   156
apply (drule_tac n=NA in Nonce_neq, simp+, rule No_Nonce, simp)
wenzelm@17394
   157
apply (blast intro!: No_Nonce dest: used_parts)
wenzelm@17394
   158
apply (drule_tac n=NA in Nonce_neq, simp+, rule No_Nonce, simp)
wenzelm@17394
   159
apply (blast intro!: No_Nonce dest: used_parts)
wenzelm@17394
   160
apply (blast dest: Says_imp_spies)
wenzelm@17394
   161
apply (blast dest: Says_imp_spies)
wenzelm@17394
   162
apply (case_tac "Ba=B", clarsimp)
wenzelm@17394
   163
apply (drule_tac n=NB and A=B in Nonce_neq, simp+)
wenzelm@17394
   164
apply (drule Says_imp_spies)
wenzelm@17394
   165
apply (drule_tac n'=NAa in in_Guard_kparts_neq, simp+, rule No_Nonce, simp)
wenzelm@17394
   166
(* OR3 *)
wenzelm@17394
   167
apply (drule Says_imp_spies)
wenzelm@17394
   168
apply (frule_tac n'=NAa in in_Guard_kparts_neq, simp+, rule No_Nonce, simp)
wenzelm@17394
   169
apply (case_tac "Aa=B", clarsimp)
wenzelm@17394
   170
apply (case_tac "NAa=NB", clarsimp)
wenzelm@17394
   171
apply (drule Says_imp_spies)
wenzelm@17394
   172
apply (drule_tac Y="{|Nonce NB, Agent Aa, Agent Ba|}"
wenzelm@17394
   173
                 and K="shrK Aa" in in_Guard_kparts_Crypt, simp+)
wenzelm@17394
   174
apply (simp add: No_Nonce) 
wenzelm@17394
   175
apply (case_tac "Ba=B", clarsimp)
wenzelm@17394
   176
apply (case_tac "NBa=NB", clarify)
wenzelm@17394
   177
apply (drule Says_imp_spies)
wenzelm@17394
   178
apply (drule_tac Y="{|Nonce NAa, Nonce NB, Agent Aa, Agent Ba|}"
wenzelm@17394
   179
                 and K="shrK Ba" in in_Guard_kparts_Crypt, simp+)
wenzelm@17394
   180
apply (simp add: No_Nonce) 
wenzelm@17394
   181
(* OR4 *)
wenzelm@17394
   182
by (blast dest: Says_imp_spies)+
wenzelm@17394
   183
wenzelm@17394
   184
end