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