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