src/HOL/Auth/Event.thy
author paulson <lp15@cam.ac.uk>
Wed, 26 Apr 2017 15:53:35 +0100
changeset 65583 8d53b3bebab4
parent 63648 f9f3006a5579
child 67443 3abf6a722518
permissions -rw-r--r--
Further new material. The simprule status of some exp and ln identities was reverted.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37936
1e4c5015a72e updated some headers;
wenzelm
parents: 32960
diff changeset
     1
(*  Title:      HOL/Auth/Event.thy
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     3
    Copyright   1996  University of Cambridge
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     4
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
     5
Datatype of events; function "spies"; freshness
3678
414e04d7c2d6 Spy can see Notes of the compromised agents
paulson
parents: 3519
diff changeset
     6
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
     7
"bad" agents have been broken by the Spy; their private keys and internal
3678
414e04d7c2d6 Spy can see Notes of the compromised agents
paulson
parents: 3519
diff changeset
     8
    stores are visible to him
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     9
*)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    10
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
    11
section\<open>Theory of Events for Security Protocols\<close>
13956
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents: 13935
diff changeset
    12
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14200
diff changeset
    13
theory Event imports Message begin
11104
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 6399
diff changeset
    14
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    15
consts  (*Initial states of agents -- parameter of the construction*)
11104
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 6399
diff changeset
    16
  initState :: "agent => msg set"
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    17
58310
91ea607a34d8 updated news
blanchet
parents: 58305
diff changeset
    18
datatype
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    19
  event = Says  agent agent msg
6399
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    20
        | Gets  agent       msg
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    21
        | Notes agent       msg
6308
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    22
       
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    23
consts 
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
    24
  bad    :: "agent set"                         \<comment> \<open>compromised agents\<close>
6308
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    25
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
    26
text\<open>Spy has access to his own key for spoof messages, but Server is secure\<close>
14126
28824746d046 Tidying and replacement of some axioms by specifications
paulson
parents: 13956
diff changeset
    27
specification (bad)
14200
d8598e24f8fa Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents: 14126
diff changeset
    28
  Spy_in_bad     [iff]: "Spy \<in> bad"
d8598e24f8fa Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents: 14126
diff changeset
    29
  Server_not_bad [iff]: "Server \<notin> bad"
14126
28824746d046 Tidying and replacement of some axioms by specifications
paulson
parents: 13956
diff changeset
    30
    by (rule exI [of _ "{Spy}"], simp)
6308
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    31
38964
b1a7bef0907a renewing specifications in HOL-Auth
bulwahn
parents: 37936
diff changeset
    32
primrec knows :: "agent => event list => msg set"
b1a7bef0907a renewing specifications in HOL-Auth
bulwahn
parents: 37936
diff changeset
    33
where
11104
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 6399
diff changeset
    34
  knows_Nil:   "knows A [] = initState A"
38964
b1a7bef0907a renewing specifications in HOL-Auth
bulwahn
parents: 37936
diff changeset
    35
| knows_Cons:
6399
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    36
    "knows A (ev # evs) =
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    37
       (if A = Spy then 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    38
        (case ev of
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    39
           Says A' B X => insert X (knows Spy evs)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    40
         | Gets A' X => knows Spy evs
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    41
         | Notes A' X  => 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    42
             if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    43
        else
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    44
        (case ev of
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    45
           Says A' B X => 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    46
             if A'=A then insert X (knows A evs) else knows A evs
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    47
         | Gets A' X    => 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    48
             if A'=A then insert X (knows A evs) else knows A evs
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    49
         | Notes A' X    => 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    50
             if A'=A then insert X (knows A evs) else knows A evs))"
6308
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    51
(*
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    52
  Case A=Spy on the Gets event
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    53
  enforces the fact that if a message is received then it must have been sent,
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    54
  therefore the oops case must use Notes
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    55
*)
3678
414e04d7c2d6 Spy can see Notes of the compromised agents
paulson
parents: 3519
diff changeset
    56
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
    57
text\<open>The constant "spies" is retained for compatibility's sake\<close>
38964
b1a7bef0907a renewing specifications in HOL-Auth
bulwahn
parents: 37936
diff changeset
    58
b1a7bef0907a renewing specifications in HOL-Auth
bulwahn
parents: 37936
diff changeset
    59
abbreviation (input)
b1a7bef0907a renewing specifications in HOL-Auth
bulwahn
parents: 37936
diff changeset
    60
  spies  :: "event list => msg set" where
b1a7bef0907a renewing specifications in HOL-Auth
bulwahn
parents: 37936
diff changeset
    61
  "spies == knows Spy"
b1a7bef0907a renewing specifications in HOL-Auth
bulwahn
parents: 37936
diff changeset
    62
b1a7bef0907a renewing specifications in HOL-Auth
bulwahn
parents: 37936
diff changeset
    63
b1a7bef0907a renewing specifications in HOL-Auth
bulwahn
parents: 37936
diff changeset
    64
(*Set of items that might be visible to somebody:
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    65
    complement of the set of fresh items*)
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    66
38964
b1a7bef0907a renewing specifications in HOL-Auth
bulwahn
parents: 37936
diff changeset
    67
primrec used :: "event list => msg set"
b1a7bef0907a renewing specifications in HOL-Auth
bulwahn
parents: 37936
diff changeset
    68
where
11104
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 6399
diff changeset
    69
  used_Nil:   "used []         = (UN B. parts (initState B))"
38964
b1a7bef0907a renewing specifications in HOL-Auth
bulwahn
parents: 37936
diff changeset
    70
| used_Cons:  "used (ev # evs) =
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    71
                     (case ev of
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    72
                        Says A B X => parts {X} \<union> used evs
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    73
                      | Gets A X   => used evs
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
    74
                      | Notes A X  => parts {X} \<union> used evs)"
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
    75
    \<comment>\<open>The case for @{term Gets} seems anomalous, but @{term Gets} always
13935
paulson
parents: 13926
diff changeset
    76
        follows @{term Says} in real protocols.  Seems difficult to change.
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
    77
        See \<open>Gets_correct\<close> in theory \<open>Guard/Extensions.thy\<close>.\<close>
6308
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    78
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
    79
lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs --> X \<in> used evs"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
    80
apply (induct_tac evs)
11463
96b5b27da55c three new theorems
paulson
parents: 11310
diff changeset
    81
apply (auto split: event.split) 
96b5b27da55c three new theorems
paulson
parents: 11310
diff changeset
    82
done
96b5b27da55c three new theorems
paulson
parents: 11310
diff changeset
    83
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
    84
lemma Says_imp_used [rule_format]: "Says A B X \<in> set evs --> X \<in> used evs"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
    85
apply (induct_tac evs)
11463
96b5b27da55c three new theorems
paulson
parents: 11310
diff changeset
    86
apply (auto split: event.split) 
96b5b27da55c three new theorems
paulson
parents: 11310
diff changeset
    87
done
96b5b27da55c three new theorems
paulson
parents: 11310
diff changeset
    88
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
    89
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
    90
subsection\<open>Function @{term knows}\<close>
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
    91
13956
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents: 13935
diff changeset
    92
(*Simplifying   
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents: 13935
diff changeset
    93
 parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs).
8fe7e12290e1 improved presentation of HOL/Auth theories
paulson
parents: 13935
diff changeset
    94
  This version won't loop with the simplifier.*)
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 41693
diff changeset
    95
lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs"] for A evs
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
    96
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
    97
lemma knows_Spy_Says [simp]:
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
    98
     "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
    99
by simp
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   100
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   101
text\<open>Letting the Spy see "bad" agents' notes avoids redundant case-splits
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   102
      on whether @{term "A=Spy"} and whether @{term "A\<in>bad"}\<close>
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   103
lemma knows_Spy_Notes [simp]:
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   104
     "knows Spy (Notes A X # evs) =  
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   105
          (if A:bad then insert X (knows Spy evs) else knows Spy evs)"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   106
by simp
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   107
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   108
lemma knows_Spy_Gets [simp]: "knows Spy (Gets A X # evs) = knows Spy evs"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   109
by simp
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   110
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   111
lemma knows_Spy_subset_knows_Spy_Says:
13935
paulson
parents: 13926
diff changeset
   112
     "knows Spy evs \<subseteq> knows Spy (Says A B X # evs)"
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   113
by (simp add: subset_insertI)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   114
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   115
lemma knows_Spy_subset_knows_Spy_Notes:
13935
paulson
parents: 13926
diff changeset
   116
     "knows Spy evs \<subseteq> knows Spy (Notes A X # evs)"
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   117
by force
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   118
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   119
lemma knows_Spy_subset_knows_Spy_Gets:
13935
paulson
parents: 13926
diff changeset
   120
     "knows Spy evs \<subseteq> knows Spy (Gets A X # evs)"
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   121
by (simp add: subset_insertI)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   122
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   123
text\<open>Spy sees what is sent on the traffic\<close>
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   124
lemma Says_imp_knows_Spy [rule_format]:
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   125
     "Says A B X \<in> set evs --> X \<in> knows Spy evs"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   126
apply (induct_tac "evs")
63648
f9f3006a5579 "split add" -> "split"
nipkow
parents: 61830
diff changeset
   127
apply (simp_all (no_asm_simp) split: event.split)
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   128
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   129
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   130
lemma Notes_imp_knows_Spy [rule_format]:
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   131
     "Notes A X \<in> set evs --> A: bad --> X \<in> knows Spy evs"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   132
apply (induct_tac "evs")
63648
f9f3006a5579 "split add" -> "split"
nipkow
parents: 61830
diff changeset
   133
apply (simp_all (no_asm_simp) split: event.split)
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   134
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   135
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   136
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   137
text\<open>Elimination rules: derive contradictions from old Says events containing
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   138
  items known to be fresh\<close>
32404
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 30549
diff changeset
   139
lemmas Says_imp_parts_knows_Spy = 
46471
2289a3869c88 prefer high-level elim_format;
wenzelm
parents: 45605
diff changeset
   140
       Says_imp_knows_Spy [THEN parts.Inj, elim_format] 
32404
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 30549
diff changeset
   141
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   142
lemmas knows_Spy_partsEs =
46471
2289a3869c88 prefer high-level elim_format;
wenzelm
parents: 45605
diff changeset
   143
     Says_imp_parts_knows_Spy parts.Body [elim_format]
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   144
18570
ffce25f9aa7f a few more named lemmas
paulson
parents: 17990
diff changeset
   145
lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]
ffce25f9aa7f a few more named lemmas
paulson
parents: 17990
diff changeset
   146
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   147
text\<open>Compatibility for the old "spies" function\<close>
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   148
lemmas spies_partsEs = knows_Spy_partsEs
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   149
lemmas Says_imp_spies = Says_imp_knows_Spy
13935
paulson
parents: 13926
diff changeset
   150
lemmas parts_insert_spies = parts_insert_knows_A [of _ Spy]
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   151
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   152
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   153
subsection\<open>Knowledge of Agents\<close>
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   154
13935
paulson
parents: 13926
diff changeset
   155
lemma knows_subset_knows_Says: "knows A evs \<subseteq> knows A (Says A' B X # evs)"
paulson
parents: 13926
diff changeset
   156
by (simp add: subset_insertI)
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   157
13935
paulson
parents: 13926
diff changeset
   158
lemma knows_subset_knows_Notes: "knows A evs \<subseteq> knows A (Notes A' X # evs)"
paulson
parents: 13926
diff changeset
   159
by (simp add: subset_insertI)
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   160
13935
paulson
parents: 13926
diff changeset
   161
lemma knows_subset_knows_Gets: "knows A evs \<subseteq> knows A (Gets A' X # evs)"
paulson
parents: 13926
diff changeset
   162
by (simp add: subset_insertI)
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   163
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   164
text\<open>Agents know what they say\<close>
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   165
lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs --> X \<in> knows A evs"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   166
apply (induct_tac "evs")
63648
f9f3006a5579 "split add" -> "split"
nipkow
parents: 61830
diff changeset
   167
apply (simp_all (no_asm_simp) split: event.split)
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   168
apply blast
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   169
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   170
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   171
text\<open>Agents know what they note\<close>
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   172
lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs --> X \<in> knows A evs"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   173
apply (induct_tac "evs")
63648
f9f3006a5579 "split add" -> "split"
nipkow
parents: 61830
diff changeset
   174
apply (simp_all (no_asm_simp) split: event.split)
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   175
apply blast
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   176
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   177
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   178
text\<open>Agents know what they receive\<close>
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   179
lemma Gets_imp_knows_agents [rule_format]:
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   180
     "A \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> knows A evs"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   181
apply (induct_tac "evs")
63648
f9f3006a5579 "split add" -> "split"
nipkow
parents: 61830
diff changeset
   182
apply (simp_all (no_asm_simp) split: event.split)
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   183
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   184
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   185
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   186
text\<open>What agents DIFFERENT FROM Spy know 
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   187
  was either said, or noted, or got, or known initially\<close>
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   188
lemma knows_imp_Says_Gets_Notes_initState [rule_format]:
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   189
     "[| X \<in> knows A evs; A \<noteq> Spy |] ==> EX B.  
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   190
  Says A B X \<in> set evs | Gets A X \<in> set evs | Notes A X \<in> set evs | X \<in> initState A"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   191
apply (erule rev_mp)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   192
apply (induct_tac "evs")
63648
f9f3006a5579 "split add" -> "split"
nipkow
parents: 61830
diff changeset
   193
apply (simp_all (no_asm_simp) split: event.split)
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   194
apply blast
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   195
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   196
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   197
text\<open>What the Spy knows -- for the time being --
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   198
  was either said or noted, or known initially\<close>
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   199
lemma knows_Spy_imp_Says_Notes_initState [rule_format]:
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   200
     "[| X \<in> knows Spy evs |] ==> EX A B.  
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   201
  Says A B X \<in> set evs | Notes A X \<in> set evs | X \<in> initState Spy"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   202
apply (erule rev_mp)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   203
apply (induct_tac "evs")
63648
f9f3006a5579 "split add" -> "split"
nipkow
parents: 61830
diff changeset
   204
apply (simp_all (no_asm_simp) split: event.split)
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   205
apply blast
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   206
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   207
13935
paulson
parents: 13926
diff changeset
   208
lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) \<subseteq> used evs"
paulson
parents: 13926
diff changeset
   209
apply (induct_tac "evs", force)  
paulson
parents: 13926
diff changeset
   210
apply (simp add: parts_insert_knows_A knows_Cons add: event.split, blast) 
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   211
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   212
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   213
lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro]
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   214
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   215
lemma initState_into_used: "X \<in> parts (initState B) ==> X \<in> used evs"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   216
apply (induct_tac "evs")
63648
f9f3006a5579 "split add" -> "split"
nipkow
parents: 61830
diff changeset
   217
apply (simp_all add: parts_insert_knows_A split: event.split, blast)
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   218
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   219
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   220
lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   221
by simp
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   222
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   223
lemma used_Notes [simp]: "used (Notes A X # evs) = parts{X} \<union> used evs"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   224
by simp
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   225
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   226
lemma used_Gets [simp]: "used (Gets A X # evs) = used evs"
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   227
by simp
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   228
13935
paulson
parents: 13926
diff changeset
   229
lemma used_nil_subset: "used [] \<subseteq> used evs"
paulson
parents: 13926
diff changeset
   230
apply simp
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   231
apply (blast intro: initState_into_used)
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   232
done
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   233
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   234
text\<open>NOTE REMOVAL--laws above are cleaner, as they don't involve "case"\<close>
13935
paulson
parents: 13926
diff changeset
   235
declare knows_Cons [simp del]
paulson
parents: 13926
diff changeset
   236
        used_Nil [simp del] used_Cons [simp del]
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   237
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   238
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   239
text\<open>For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) --> P"}
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   240
  New events added by induction to "evs" are discarded.  Provided 
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   241
  this information isn't needed, the proof will be much shorter, since
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   242
  it will omit complicated reasoning about @{term analz}.\<close>
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   243
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   244
lemmas analz_mono_contra =
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   245
       knows_Spy_subset_knows_Spy_Says [THEN analz_mono, THEN contra_subsetD]
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   246
       knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   247
       knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   248
11104
f2024fed9f0c partial conversion to Isar script style
paulson
parents: 6399
diff changeset
   249
13922
75ae4244a596 Changes required by the certified email protocol
paulson
parents: 11463
diff changeset
   250
lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
53428
3083c611ec40 use case_of_simps
noschinl
parents: 46471
diff changeset
   251
by (cases e, auto simp: knows_Cons)
13922
75ae4244a596 Changes required by the certified email protocol
paulson
parents: 11463
diff changeset
   252
13935
paulson
parents: 13926
diff changeset
   253
lemma initState_subset_knows: "initState A \<subseteq> knows A evs"
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   254
apply (induct_tac evs, simp) 
13922
75ae4244a596 Changes required by the certified email protocol
paulson
parents: 11463
diff changeset
   255
apply (blast intro: knows_subset_knows_Cons [THEN subsetD])
75ae4244a596 Changes required by the certified email protocol
paulson
parents: 11463
diff changeset
   256
done
75ae4244a596 Changes required by the certified email protocol
paulson
parents: 11463
diff changeset
   257
75ae4244a596 Changes required by the certified email protocol
paulson
parents: 11463
diff changeset
   258
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   259
text\<open>For proving \<open>new_keys_not_used\<close>\<close>
13922
75ae4244a596 Changes required by the certified email protocol
paulson
parents: 11463
diff changeset
   260
lemma keysFor_parts_insert:
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13922
diff changeset
   261
     "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |] 
41693
47532fe9e075 Introduction of metis calls and other cosmetic modifications.
paulson
parents: 38964
diff changeset
   262
      ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H"
13922
75ae4244a596 Changes required by the certified email protocol
paulson
parents: 11463
diff changeset
   263
by (force 
75ae4244a596 Changes required by the certified email protocol
paulson
parents: 11463
diff changeset
   264
    dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
75ae4244a596 Changes required by the certified email protocol
paulson
parents: 11463
diff changeset
   265
           analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
75ae4244a596 Changes required by the certified email protocol
paulson
parents: 11463
diff changeset
   266
    intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
75ae4244a596 Changes required by the certified email protocol
paulson
parents: 11463
diff changeset
   267
24122
fc7f857d33c8 tuned ML bindings (for multithreading);
wenzelm
parents: 21588
diff changeset
   268
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 41693
diff changeset
   269
lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)"] for Y evs
27225
b316dde851f5 eliminated OldGoals.inst;
wenzelm
parents: 27154
diff changeset
   270
24122
fc7f857d33c8 tuned ML bindings (for multithreading);
wenzelm
parents: 21588
diff changeset
   271
ML
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   272
\<open>
58963
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents: 58889
diff changeset
   273
fun analz_mono_contra_tac ctxt = 
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 59498
diff changeset
   274
  resolve_tac ctxt @{thms analz_impI} THEN' 
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58963
diff changeset
   275
  REPEAT1 o (dresolve_tac ctxt @{thms analz_mono_contra})
58963
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents: 58889
diff changeset
   276
  THEN' (mp_tac ctxt)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   277
\<close>
24122
fc7f857d33c8 tuned ML bindings (for multithreading);
wenzelm
parents: 21588
diff changeset
   278
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   279
method_setup analz_mono_contra = \<open>
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   280
    Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (analz_mono_contra_tac ctxt)))\<close>
13922
75ae4244a596 Changes required by the certified email protocol
paulson
parents: 11463
diff changeset
   281
    "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
75ae4244a596 Changes required by the certified email protocol
paulson
parents: 11463
diff changeset
   282
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   283
subsubsection\<open>Useful for case analysis on whether a hash is a spoof or not\<close>
13922
75ae4244a596 Changes required by the certified email protocol
paulson
parents: 11463
diff changeset
   284
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 41693
diff changeset
   285
lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))"] for Y evs
27225
b316dde851f5 eliminated OldGoals.inst;
wenzelm
parents: 27154
diff changeset
   286
13922
75ae4244a596 Changes required by the certified email protocol
paulson
parents: 11463
diff changeset
   287
ML
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   288
\<open>
58963
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents: 58889
diff changeset
   289
fun synth_analz_mono_contra_tac ctxt = 
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 59498
diff changeset
   290
  resolve_tac ctxt @{thms syan_impI} THEN'
27225
b316dde851f5 eliminated OldGoals.inst;
wenzelm
parents: 27154
diff changeset
   291
  REPEAT1 o 
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58963
diff changeset
   292
    (dresolve_tac ctxt
27225
b316dde851f5 eliminated OldGoals.inst;
wenzelm
parents: 27154
diff changeset
   293
     [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
b316dde851f5 eliminated OldGoals.inst;
wenzelm
parents: 27154
diff changeset
   294
      @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
b316dde851f5 eliminated OldGoals.inst;
wenzelm
parents: 27154
diff changeset
   295
      @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])
b316dde851f5 eliminated OldGoals.inst;
wenzelm
parents: 27154
diff changeset
   296
  THEN'
58963
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents: 58889
diff changeset
   297
  mp_tac ctxt
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   298
\<close>
13922
75ae4244a596 Changes required by the certified email protocol
paulson
parents: 11463
diff changeset
   299
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   300
method_setup synth_analz_mono_contra = \<open>
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 60754
diff changeset
   301
    Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (synth_analz_mono_contra_tac ctxt)))\<close>
13922
75ae4244a596 Changes required by the certified email protocol
paulson
parents: 11463
diff changeset
   302
    "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   303
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   304
end