src/HOL/Auth/Guard/Guard_Public.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 48260 65ed3b2b3157
child 61830 4f5ab843cf5b
permissions -rw-r--r--
prefer symbols;
     1 (*  Title:      HOL/Auth/Guard/Guard_Public.thy
     2     Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
     3     Copyright   2002  University of Cambridge
     4 
     5 Lemmas on guarded messages for public protocols.
     6 *)
     7 
     8 theory Guard_Public imports Guard "../Public" Extensions begin
     9 
    10 subsection{*Extensions to Theory @{text Public}*}
    11 
    12 declare initState.simps [simp del]
    13 
    14 subsubsection{*signature*}
    15 
    16 definition sign :: "agent => msg => msg" where
    17 "sign A X == {|Agent A, X, Crypt (priK A) (Hash X)|}"
    18 
    19 lemma sign_inj [iff]: "(sign A X = sign A' X') = (A=A' & X=X')"
    20 by (auto simp: sign_def)
    21 
    22 subsubsection{*agent associated to a key*}
    23 
    24 definition agt :: "key => agent" where
    25 "agt K == @A. K = priK A | K = pubK A"
    26 
    27 lemma agt_priK [simp]: "agt (priK A) = A"
    28 by (simp add: agt_def)
    29 
    30 lemma agt_pubK [simp]: "agt (pubK A) = A"
    31 by (simp add: agt_def)
    32 
    33 subsubsection{*basic facts about @{term initState}*}
    34 
    35 lemma no_Crypt_in_parts_init [simp]: "Crypt K X ~:parts (initState A)"
    36 by (cases A, auto simp: initState.simps)
    37 
    38 lemma no_Crypt_in_analz_init [simp]: "Crypt K X ~:analz (initState A)"
    39 by auto
    40 
    41 lemma no_priK_in_analz_init [simp]: "A ~:bad
    42 ==> Key (priK A) ~:analz (initState Spy)"
    43 by (auto simp: initState.simps)
    44 
    45 lemma priK_notin_initState_Friend [simp]: "A ~= Friend C
    46 ==> Key (priK A) ~: parts (initState (Friend C))"
    47 by (auto simp: initState.simps)
    48 
    49 lemma keyset_init [iff]: "keyset (initState A)"
    50 by (cases A, auto simp: keyset_def initState.simps)
    51 
    52 subsubsection{*sets of private keys*}
    53 
    54 definition priK_set :: "key set => bool" where
    55 "priK_set Ks == ALL K. K:Ks --> (EX A. K = priK A)"
    56 
    57 lemma in_priK_set: "[| priK_set Ks; K:Ks |] ==> EX A. K = priK A"
    58 by (simp add: priK_set_def)
    59 
    60 lemma priK_set1 [iff]: "priK_set {priK A}"
    61 by (simp add: priK_set_def)
    62 
    63 lemma priK_set2 [iff]: "priK_set {priK A, priK B}"
    64 by (simp add: priK_set_def)
    65 
    66 subsubsection{*sets of good keys*}
    67 
    68 definition good :: "key set => bool" where
    69 "good Ks == ALL K. K:Ks --> agt K ~:bad"
    70 
    71 lemma in_good: "[| good Ks; K:Ks |] ==> agt K ~:bad"
    72 by (simp add: good_def)
    73 
    74 lemma good1 [simp]: "A ~:bad ==> good {priK A}"
    75 by (simp add: good_def)
    76 
    77 lemma good2 [simp]: "[| A ~:bad; B ~:bad |] ==> good {priK A, priK B}"
    78 by (simp add: good_def)
    79 
    80 subsubsection{*greatest nonce used in a trace, 0 if there is no nonce*}
    81 
    82 primrec greatest :: "event list => nat"
    83 where
    84   "greatest [] = 0"
    85 | "greatest (ev # evs) = max (greatest_msg (msg ev)) (greatest evs)"
    86 
    87 lemma greatest_is_greatest: "Nonce n:used evs ==> n <= greatest evs"
    88 apply (induct evs, auto simp: initState.simps)
    89 apply (drule used_sub_parts_used, safe)
    90 apply (drule greatest_msg_is_greatest, arith)
    91 by simp
    92 
    93 subsubsection{*function giving a new nonce*}
    94 
    95 definition new :: "event list => nat" where
    96 "new evs == Suc (greatest evs)"
    97 
    98 lemma new_isnt_used [iff]: "Nonce (new evs) ~:used evs"
    99 by (clarify, drule greatest_is_greatest, auto simp: new_def)
   100 
   101 subsection{*Proofs About Guarded Messages*}
   102 
   103 subsubsection{*small hack necessary because priK is defined as the inverse of pubK*}
   104 
   105 lemma pubK_is_invKey_priK: "pubK A = invKey (priK A)"
   106 by simp
   107 
   108 lemmas pubK_is_invKey_priK_substI = pubK_is_invKey_priK [THEN ssubst]
   109 
   110 lemmas invKey_invKey_substI = invKey [THEN ssubst]
   111 
   112 lemma "Nonce n:parts {X} ==> Crypt (pubK A) X:guard n {priK A}"
   113 apply (rule pubK_is_invKey_priK_substI, rule invKey_invKey_substI)
   114 by (rule Guard_Nonce, simp+)
   115 
   116 subsubsection{*guardedness results*}
   117 
   118 lemma sign_guard [intro]: "X:guard n Ks ==> sign A X:guard n Ks"
   119 by (auto simp: sign_def)
   120 
   121 lemma Guard_init [iff]: "Guard n Ks (initState B)"
   122 by (induct B, auto simp: Guard_def initState.simps)
   123 
   124 lemma Guard_knows_max': "Guard n Ks (knows_max' C evs)
   125 ==> Guard n Ks (knows_max C evs)"
   126 by (simp add: knows_max_def)
   127 
   128 lemma Nonce_not_used_Guard_spies [dest]: "Nonce n ~:used evs
   129 ==> Guard n Ks (spies evs)"
   130 by (auto simp: Guard_def dest: not_used_not_known parts_sub)
   131 
   132 lemma Nonce_not_used_Guard [dest]: "[| evs:p; Nonce n ~:used evs;
   133 Gets_correct p; one_step p |] ==> Guard n Ks (knows (Friend C) evs)"
   134 by (auto simp: Guard_def dest: known_used parts_trans)
   135 
   136 lemma Nonce_not_used_Guard_max [dest]: "[| evs:p; Nonce n ~:used evs;
   137 Gets_correct p; one_step p |] ==> Guard n Ks (knows_max (Friend C) evs)"
   138 by (auto simp: Guard_def dest: known_max_used parts_trans)
   139 
   140 lemma Nonce_not_used_Guard_max' [dest]: "[| evs:p; Nonce n ~:used evs;
   141 Gets_correct p; one_step p |] ==> Guard n Ks (knows_max' (Friend C) evs)"
   142 apply (rule_tac H="knows_max (Friend C) evs" in Guard_mono)
   143 by (auto simp: knows_max_def)
   144 
   145 subsubsection{*regular protocols*}
   146 
   147 definition regular :: "event list set => bool" where
   148 "regular p == ALL evs A. evs:p --> (Key (priK A):parts (spies evs)) = (A:bad)"
   149 
   150 lemma priK_parts_iff_bad [simp]: "[| evs:p; regular p |] ==>
   151 (Key (priK A):parts (spies evs)) = (A:bad)"
   152 by (auto simp: regular_def)
   153 
   154 lemma priK_analz_iff_bad [simp]: "[| evs:p; regular p |] ==>
   155 (Key (priK A):analz (spies evs)) = (A:bad)"
   156 by auto
   157 
   158 lemma Guard_Nonce_analz: "[| Guard n Ks (spies evs); evs:p;
   159 priK_set Ks; good Ks; regular p |] ==> Nonce n ~:analz (spies evs)"
   160 apply (clarify, simp only: knows_decomp)
   161 apply (drule Guard_invKey_keyset, simp+, safe)
   162 apply (drule in_good, simp)
   163 apply (drule in_priK_set, simp+, clarify)
   164 apply (frule_tac A=A in priK_analz_iff_bad)
   165 by (simp add: knows_decomp)+
   166 
   167 end