src/HOL/Auth/Guard/Guard_Shared.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 35416 d8d7d1b785af
child 41775 6214816d79d3
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
     1 (******************************************************************************
     2 date: march 2002
     3 author: Frederic Blanqui
     4 email: blanqui@lri.fr
     5 webpage: http://www.lri.fr/~blanqui/
     6 
     7 University of Cambridge, Computer Laboratory
     8 William Gates Building, JJ Thomson Avenue
     9 Cambridge CB3 0FD, United Kingdom
    10 ******************************************************************************)
    11 
    12 header{*lemmas on guarded messages for protocols with symmetric keys*}
    13 
    14 theory Guard_Shared imports Guard GuardK "../Shared" begin
    15 
    16 subsection{*Extensions to Theory @{text Shared}*}
    17 
    18 declare initState.simps [simp del]
    19 
    20 subsubsection{*a little abbreviation*}
    21 
    22 abbreviation
    23   Ciph :: "agent => msg => msg" where
    24   "Ciph A X == Crypt (shrK A) X"
    25 
    26 subsubsection{*agent associated to a key*}
    27 
    28 definition agt :: "key => agent" where
    29 "agt K == @A. K = shrK A"
    30 
    31 lemma agt_shrK [simp]: "agt (shrK A) = A"
    32 by (simp add: agt_def)
    33 
    34 subsubsection{*basic facts about @{term initState}*}
    35 
    36 lemma no_Crypt_in_parts_init [simp]: "Crypt K X ~:parts (initState A)"
    37 by (cases A, auto simp: initState.simps)
    38 
    39 lemma no_Crypt_in_analz_init [simp]: "Crypt K X ~:analz (initState A)"
    40 by auto
    41 
    42 lemma no_shrK_in_analz_init [simp]: "A ~:bad
    43 ==> Key (shrK A) ~:analz (initState Spy)"
    44 by (auto simp: initState.simps)
    45 
    46 lemma shrK_notin_initState_Friend [simp]: "A ~= Friend C
    47 ==> Key (shrK A) ~: parts (initState (Friend C))"
    48 by (auto simp: initState.simps)
    49 
    50 lemma keyset_init [iff]: "keyset (initState A)"
    51 by (cases A, auto simp: keyset_def initState.simps)
    52 
    53 subsubsection{*sets of symmetric keys*}
    54 
    55 definition shrK_set :: "key set => bool" where
    56 "shrK_set Ks == ALL K. K:Ks --> (EX A. K = shrK A)"
    57 
    58 lemma in_shrK_set: "[| shrK_set Ks; K:Ks |] ==> EX A. K = shrK A"
    59 by (simp add: shrK_set_def)
    60 
    61 lemma shrK_set1 [iff]: "shrK_set {shrK A}"
    62 by (simp add: shrK_set_def)
    63 
    64 lemma shrK_set2 [iff]: "shrK_set {shrK A, shrK B}"
    65 by (simp add: shrK_set_def)
    66 
    67 subsubsection{*sets of good keys*}
    68 
    69 definition good :: "key set => bool" where
    70 "good Ks == ALL K. K:Ks --> agt K ~:bad"
    71 
    72 lemma in_good: "[| good Ks; K:Ks |] ==> agt K ~:bad"
    73 by (simp add: good_def)
    74 
    75 lemma good1 [simp]: "A ~:bad ==> good {shrK A}"
    76 by (simp add: good_def)
    77 
    78 lemma good2 [simp]: "[| A ~:bad; B ~:bad |] ==> good {shrK A, shrK B}"
    79 by (simp add: good_def)
    80 
    81 
    82 subsection{*Proofs About Guarded Messages*}
    83 
    84 subsubsection{*small hack*}
    85 
    86 lemma shrK_is_invKey_shrK: "shrK A = invKey (shrK A)"
    87 by simp
    88 
    89 lemmas shrK_is_invKey_shrK_substI = shrK_is_invKey_shrK [THEN ssubst]
    90 
    91 lemmas invKey_invKey_substI = invKey [THEN ssubst]
    92 
    93 lemma "Nonce n:parts {X} ==> Crypt (shrK A) X:guard n {shrK A}"
    94 apply (rule shrK_is_invKey_shrK_substI, rule invKey_invKey_substI)
    95 by (rule Guard_Nonce, simp+)
    96 
    97 subsubsection{*guardedness results on nonces*}
    98 
    99 lemma guard_ciph [simp]: "shrK A:Ks ==> Ciph A X:guard n Ks"
   100 by (rule Guard_Nonce, simp)
   101 
   102 lemma guardK_ciph [simp]: "shrK A:Ks ==> Ciph A X:guardK n Ks"
   103 by (rule Guard_Key, simp)
   104 
   105 lemma Guard_init [iff]: "Guard n Ks (initState B)"
   106 by (induct B, auto simp: Guard_def initState.simps)
   107 
   108 lemma Guard_knows_max': "Guard n Ks (knows_max' C evs)
   109 ==> Guard n Ks (knows_max C evs)"
   110 by (simp add: knows_max_def)
   111 
   112 lemma Nonce_not_used_Guard_spies [dest]: "Nonce n ~:used evs
   113 ==> Guard n Ks (spies evs)"
   114 by (auto simp: Guard_def dest: not_used_not_known parts_sub)
   115 
   116 lemma Nonce_not_used_Guard [dest]: "[| evs:p; Nonce n ~:used evs;
   117 Gets_correct p; one_step p |] ==> Guard n Ks (knows (Friend C) evs)"
   118 by (auto simp: Guard_def dest: known_used parts_trans)
   119 
   120 lemma Nonce_not_used_Guard_max [dest]: "[| evs:p; Nonce n ~:used evs;
   121 Gets_correct p; one_step p |] ==> Guard n Ks (knows_max (Friend C) evs)"
   122 by (auto simp: Guard_def dest: known_max_used parts_trans)
   123 
   124 lemma Nonce_not_used_Guard_max' [dest]: "[| evs:p; Nonce n ~:used evs;
   125 Gets_correct p; one_step p |] ==> Guard n Ks (knows_max' (Friend C) evs)"
   126 apply (rule_tac H="knows_max (Friend C) evs" in Guard_mono)
   127 by (auto simp: knows_max_def)
   128 
   129 subsubsection{*guardedness results on keys*}
   130 
   131 lemma GuardK_init [simp]: "n ~:range shrK ==> GuardK n Ks (initState B)"
   132 by (induct B, auto simp: GuardK_def initState.simps)
   133 
   134 lemma GuardK_knows_max': "[| GuardK n A (knows_max' C evs); n ~:range shrK |]
   135 ==> GuardK n A (knows_max C evs)"
   136 by (simp add: knows_max_def)
   137 
   138 lemma Key_not_used_GuardK_spies [dest]: "Key n ~:used evs
   139 ==> GuardK n A (spies evs)"
   140 by (auto simp: GuardK_def dest: not_used_not_known parts_sub)
   141 
   142 lemma Key_not_used_GuardK [dest]: "[| evs:p; Key n ~:used evs;
   143 Gets_correct p; one_step p |] ==> GuardK n A (knows (Friend C) evs)"
   144 by (auto simp: GuardK_def dest: known_used parts_trans)
   145 
   146 lemma Key_not_used_GuardK_max [dest]: "[| evs:p; Key n ~:used evs;
   147 Gets_correct p; one_step p |] ==> GuardK n A (knows_max (Friend C) evs)"
   148 by (auto simp: GuardK_def dest: known_max_used parts_trans)
   149 
   150 lemma Key_not_used_GuardK_max' [dest]: "[| evs:p; Key n ~:used evs;
   151 Gets_correct p; one_step p |] ==> GuardK n A (knows_max' (Friend C) evs)"
   152 apply (rule_tac H="knows_max (Friend C) evs" in GuardK_mono)
   153 by (auto simp: knows_max_def)
   154 
   155 subsubsection{*regular protocols*}
   156 
   157 definition regular :: "event list set => bool" where
   158 "regular p == ALL evs A. evs:p --> (Key (shrK A):parts (spies evs)) = (A:bad)"
   159 
   160 lemma shrK_parts_iff_bad [simp]: "[| evs:p; regular p |] ==>
   161 (Key (shrK A):parts (spies evs)) = (A:bad)"
   162 by (auto simp: regular_def)
   163 
   164 lemma shrK_analz_iff_bad [simp]: "[| evs:p; regular p |] ==>
   165 (Key (shrK A):analz (spies evs)) = (A:bad)"
   166 by auto
   167 
   168 lemma Guard_Nonce_analz: "[| Guard n Ks (spies evs); evs:p;
   169 shrK_set Ks; good Ks; regular p |] ==> Nonce n ~:analz (spies evs)"
   170 apply (clarify, simp only: knows_decomp)
   171 apply (drule Guard_invKey_keyset, simp+, safe)
   172 apply (drule in_good, simp)
   173 apply (drule in_shrK_set, simp+, clarify)
   174 apply (frule_tac A=A in shrK_analz_iff_bad)
   175 by (simp add: knows_decomp)+
   176 
   177 lemma GuardK_Key_analz: "[| GuardK n Ks (spies evs); evs:p;
   178 shrK_set Ks; good Ks; regular p; n ~:range shrK |] ==> Key n ~:analz (spies evs)"
   179 apply (clarify, simp only: knows_decomp)
   180 apply (drule GuardK_invKey_keyset, clarify, simp+, simp add: initState.simps)
   181 apply clarify
   182 apply (drule in_good, simp)
   183 apply (drule in_shrK_set, simp+, clarify)
   184 apply (frule_tac A=A in shrK_analz_iff_bad)
   185 by (simp add: knows_decomp)+
   186 
   187 end