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