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