src/HOL/Auth/Recur.thy
author paulson <lp15@cam.ac.uk>
Wed, 26 Apr 2017 15:53:35 +0100
changeset 65583 8d53b3bebab4
parent 62343 24106dc44def
child 67613 ce654b0e6d69
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/Recur.thy
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
     3
    Copyright   1996  University of Cambridge
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
     4
*)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
     5
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
     6
section\<open>The Otway-Bull Recursive Authentication Protocol\<close>
14207
f20fbb141673 Conversion of all main protocols from "Shared" to "Public".
paulson
parents: 14200
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14207
diff changeset
     8
theory Recur imports Public begin
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
     9
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
    10
text\<open>End marker for message bundles\<close>
20768
1d478c2d621f replaced syntax/translations by abbreviation;
wenzelm
parents: 16417
diff changeset
    11
abbreviation
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20768
diff changeset
    12
  END :: "msg" where
20768
1d478c2d621f replaced syntax/translations by abbreviation;
wenzelm
parents: 16417
diff changeset
    13
  "END == Number 0"
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
    14
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    15
(*Two session keys are distributed to each agent except for the initiator,
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    16
        who receives one.
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    17
  Perhaps the two session keys could be bundled into a single message.
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    18
*)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    19
inductive_set (*Server's response to the nested message*)
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    20
  respond :: "event list => (msg*msg*key)set"
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    21
  for evs :: "event list"
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    22
  where
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
    23
   One:  "Key KAB \<notin> used evs
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
    24
          ==> (Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, Nonce NA, END\<rbrace>,
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
    25
               \<lbrace>Crypt (shrK A) \<lbrace>Key KAB, Agent B, Nonce NA\<rbrace>, END\<rbrace>,
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
    26
               KAB)   \<in> respond evs"
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    27
2532
cde25bf71cc1 Improved layout and updated comments
paulson
parents: 2516
diff changeset
    28
    (*The most recent session key is passed up to the caller*)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    29
 | Cons: "[| (PA, RA, KAB) \<in> respond evs;
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
    30
             Key KBC \<notin> used evs;  Key KBC \<notin> parts {RA};
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
    31
             PA = Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, Nonce NA, P\<rbrace> |]
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
    32
          ==> (Hash[Key(shrK B)] \<lbrace>Agent B, Agent C, Nonce NB, PA\<rbrace>,
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
    33
               \<lbrace>Crypt (shrK B) \<lbrace>Key KBC, Agent C, Nonce NB\<rbrace>,
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
    34
                 Crypt (shrK B) \<lbrace>Key KAB, Agent A, Nonce NB\<rbrace>,
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
    35
                 RA\<rbrace>,
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    36
               KBC)
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
    37
              \<in> respond evs"
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    38
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    39
2481
ee461c8bc9c3 Now uses HPair
paulson
parents: 2451
diff changeset
    40
(*Induction over "respond" can be difficult due to the complexity of the
2532
cde25bf71cc1 Improved layout and updated comments
paulson
parents: 2516
diff changeset
    41
  subgoals.  Set "responses" captures the general form of certificates.
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    42
*)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    43
inductive_set
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    44
  responses :: "event list => msg set"
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    45
  for evs :: "event list"
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    46
  where
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    47
    (*Server terminates lists*)
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
    48
   Nil:  "END \<in> responses evs"
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    49
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    50
 | Cons: "[| RA \<in> responses evs;  Key KAB \<notin> used evs |]
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
    51
          ==> \<lbrace>Crypt (shrK B) \<lbrace>Key KAB, Agent A, Nonce NB\<rbrace>,
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
    52
                RA\<rbrace>  \<in> responses evs"
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    53
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    54
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    55
inductive_set recur :: "event list set"
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    56
  where
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    57
         (*Initial trace is empty*)
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
    58
   Nil:  "[] \<in> recur"
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    59
2532
cde25bf71cc1 Improved layout and updated comments
paulson
parents: 2516
diff changeset
    60
         (*The spy MAY say anything he CAN say.  Common to
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    61
           all similar protocols.*)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    62
 | Fake: "[| evsf \<in> recur;  X \<in> synth (analz (knows Spy evsf)) |]
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
    63
          ==> Says Spy B X  # evsf \<in> recur"
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    64
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    65
         (*Alice initiates a protocol run.
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
    66
           END is a placeholder to terminate the nesting.*)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    67
 | RA1:  "[| evs1 \<in> recur;  Nonce NA \<notin> used evs1 |]
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
    68
          ==> Says A B (Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, Nonce NA, END\<rbrace>)
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
    69
              # evs1 \<in> recur"
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    70
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    71
         (*Bob's response to Alice's message.  C might be the Server.
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
    72
           We omit PA = \<lbrace>XA, Agent A, Agent B, Nonce NA, P\<rbrace> because
4552
bb8ff763c93d Simplified proofs by omitting PA = {|XA, ...|} from RA2
paulson
parents: 3683
diff changeset
    73
           it complicates proofs, so B may respond to any message at all!*)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    74
 | RA2:  "[| evs2 \<in> recur;  Nonce NB \<notin> used evs2;
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
    75
             Says A' B PA \<in> set evs2 |]
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
    76
          ==> Says B C (Hash[Key(shrK B)] \<lbrace>Agent B, Agent C, Nonce NB, PA\<rbrace>)
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
    77
              # evs2 \<in> recur"
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    78
2550
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2532
diff changeset
    79
         (*The Server receives Bob's message and prepares a response.*)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    80
 | RA3:  "[| evs3 \<in> recur;  Says B' Server PB \<in> set evs3;
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
    81
             (PB,RB,K) \<in> respond evs3 |]
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
    82
          ==> Says Server B RB # evs3 \<in> recur"
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    83
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    84
         (*Bob receives the returned message and compares the Nonces with
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    85
           those in the message he previously sent the Server.*)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    86
 | RA4:  "[| evs4 \<in> recur;
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
    87
             Says B  C \<lbrace>XH, Agent B, Agent C, Nonce NB,
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
    88
                         XA, Agent A, Agent B, Nonce NA, P\<rbrace> \<in> set evs4;
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
    89
             Says C' B \<lbrace>Crypt (shrK B) \<lbrace>Key KBC, Agent C, Nonce NB\<rbrace>,
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
    90
                         Crypt (shrK B) \<lbrace>Key KAB, Agent A, Nonce NB\<rbrace>,
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
    91
                         RA\<rbrace> \<in> set evs4 |]
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
    92
          ==> Says B A RA # evs4 \<in> recur"
5359
bd539b72d484 Tidying
paulson
parents: 4552
diff changeset
    93
bd539b72d484 Tidying
paulson
parents: 4552
diff changeset
    94
   (*No "oops" message can easily be expressed.  Each session key is
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
    95
     associated--in two separate messages--with two nonces.  This is
5359
bd539b72d484 Tidying
paulson
parents: 4552
diff changeset
    96
     one try, but it isn't that useful.  Re domino attack, note that
24122
fc7f857d33c8 tuned ML bindings (for multithreading);
wenzelm
parents: 23894
diff changeset
    97
     Recur.thy proves that each session key is secure provided the two
5359
bd539b72d484 Tidying
paulson
parents: 4552
diff changeset
    98
     peers are, even if there are compromised agents elsewhere in
bd539b72d484 Tidying
paulson
parents: 4552
diff changeset
    99
     the chain.  Oops cases proved using parts_cut, Key_in_keysFor_parts,
bd539b72d484 Tidying
paulson
parents: 4552
diff changeset
   100
     etc.
bd539b72d484 Tidying
paulson
parents: 4552
diff changeset
   101
14207
f20fbb141673 Conversion of all main protocols from "Shared" to "Public".
paulson
parents: 14200
diff changeset
   102
   Oops:  "[| evso \<in> recur;  Says Server B RB \<in> set evso;
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   103
              RB \<in> responses evs';  Key K \<in> parts {RB} |]
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   104
           ==> Notes Spy \<lbrace>Key K, RB\<rbrace> # evso \<in> recur"
5359
bd539b72d484 Tidying
paulson
parents: 4552
diff changeset
   105
  *)
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   106
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   107
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   108
declare Says_imp_knows_Spy [THEN analz.Inj, dest]
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   109
declare parts.Body  [dest]
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   110
declare analz_into_parts [dest]
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   111
declare Fake_parts_insert_in_Un  [dest]
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   112
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   113
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   114
(** Possibility properties: traces that reach the end
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   115
        ONE theorem would be more elegant and faster!
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   116
        By induction on a list of agents (no repetitions)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   117
**)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   118
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   119
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   120
text\<open>Simplest case: Alice goes directly to the server\<close>
14200
d8598e24f8fa Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents: 13956
diff changeset
   121
lemma "Key K \<notin> used [] 
d8598e24f8fa Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents: 13956
diff changeset
   122
       ==> \<exists>NA. \<exists>evs \<in> recur.
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   123
              Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent Server, Nonce NA\<rbrace>,
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   124
                    END\<rbrace>  \<in> set evs"
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   125
apply (intro exI bexI)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   126
apply (rule_tac [2] recur.Nil [THEN recur.RA1, 
14200
d8598e24f8fa Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents: 13956
diff changeset
   127
                             THEN recur.RA3 [OF _ _ respond.One]])
d8598e24f8fa Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents: 13956
diff changeset
   128
apply (possibility, simp add: used_Cons) 
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   129
done
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   130
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   131
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   132
text\<open>Case two: Alice, Bob and the server\<close>
14207
f20fbb141673 Conversion of all main protocols from "Shared" to "Public".
paulson
parents: 14200
diff changeset
   133
lemma "[| Key K \<notin> used []; Key K' \<notin> used []; K \<noteq> K';
f20fbb141673 Conversion of all main protocols from "Shared" to "Public".
paulson
parents: 14200
diff changeset
   134
          Nonce NA \<notin> used []; Nonce NB \<notin> used []; NA < NB |]
f20fbb141673 Conversion of all main protocols from "Shared" to "Public".
paulson
parents: 14200
diff changeset
   135
       ==> \<exists>NA. \<exists>evs \<in> recur.
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   136
        Says B A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent B, Nonce NA\<rbrace>,
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   137
                   END\<rbrace>  \<in> set evs"
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   138
apply (intro exI bexI)
11270
a315a3862bb4 better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents: 11264
diff changeset
   139
apply (rule_tac [2] 
14207
f20fbb141673 Conversion of all main protocols from "Shared" to "Public".
paulson
parents: 14200
diff changeset
   140
          recur.Nil
f20fbb141673 Conversion of all main protocols from "Shared" to "Public".
paulson
parents: 14200
diff changeset
   141
           [THEN recur.RA1 [of _ NA], 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   142
            THEN recur.RA2 [of _ NB],
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   143
            THEN recur.RA3 [OF _ _ respond.One 
14207
f20fbb141673 Conversion of all main protocols from "Shared" to "Public".
paulson
parents: 14200
diff changeset
   144
                                     [THEN respond.Cons [of _ _ K _ K']]],
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   145
            THEN recur.RA4], possibility)
14200
d8598e24f8fa Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents: 13956
diff changeset
   146
apply (auto simp add: used_Cons)
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   147
done
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   148
14200
d8598e24f8fa Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents: 13956
diff changeset
   149
(*Case three: Alice, Bob, Charlie and the server Rather slow (5 seconds)*)
d8598e24f8fa Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents: 13956
diff changeset
   150
lemma "[| Key K \<notin> used []; Key K' \<notin> used [];  
14207
f20fbb141673 Conversion of all main protocols from "Shared" to "Public".
paulson
parents: 14200
diff changeset
   151
          Key K'' \<notin> used []; K \<noteq> K'; K' \<noteq> K''; K \<noteq> K'';
f20fbb141673 Conversion of all main protocols from "Shared" to "Public".
paulson
parents: 14200
diff changeset
   152
          Nonce NA \<notin> used []; Nonce NB \<notin> used []; Nonce NC \<notin> used []; 
f20fbb141673 Conversion of all main protocols from "Shared" to "Public".
paulson
parents: 14200
diff changeset
   153
          NA < NB; NB < NC |]
14200
d8598e24f8fa Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents: 13956
diff changeset
   154
       ==> \<exists>K. \<exists>NA. \<exists>evs \<in> recur.
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   155
             Says B A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent B, Nonce NA\<rbrace>,
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   156
                        END\<rbrace>  \<in> set evs"
11270
a315a3862bb4 better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents: 11264
diff changeset
   157
apply (intro exI bexI)
a315a3862bb4 better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents: 11264
diff changeset
   158
apply (rule_tac [2] 
a315a3862bb4 better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents: 11264
diff changeset
   159
          recur.Nil [THEN recur.RA1, 
a315a3862bb4 better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents: 11264
diff changeset
   160
                     THEN recur.RA2, THEN recur.RA2,
a315a3862bb4 better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents: 11264
diff changeset
   161
                     THEN recur.RA3 
a315a3862bb4 better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents: 11264
diff changeset
   162
                          [OF _ _ respond.One 
a315a3862bb4 better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents: 11264
diff changeset
   163
                                  [THEN respond.Cons, THEN respond.Cons]],
a315a3862bb4 better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents: 11264
diff changeset
   164
                     THEN recur.RA4, THEN recur.RA4])
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 23746
diff changeset
   165
apply basic_possibility
58963
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents: 58889
diff changeset
   166
apply (tactic "DEPTH_SOLVE (swap_res_tac @{context} [refl, conjI, disjCI] 1)")
11270
a315a3862bb4 better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents: 11264
diff changeset
   167
done
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   168
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   169
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   170
lemma respond_imp_not_used: "(PA,RB,KAB) \<in> respond evs ==> Key KAB \<notin> used evs"
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   171
by (erule respond.induct, simp_all)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   172
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   173
lemma Key_in_parts_respond [rule_format]:
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   174
   "[| Key K \<in> parts {RB};  (PB,RB,K') \<in> respond evs |] ==> Key K \<notin> used evs"
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   175
apply (erule rev_mp, erule respond.induct)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   176
apply (auto dest: Key_not_used respond_imp_not_used)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   177
done
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   178
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   179
text\<open>Simple inductive reasoning about responses\<close>
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   180
lemma respond_imp_responses:
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   181
     "(PA,RB,KAB) \<in> respond evs ==> RB \<in> responses evs"
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   182
apply (erule respond.induct)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   183
apply (blast intro!: respond_imp_not_used responses.intros)+
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   184
done
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   185
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   186
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   187
(** For reasoning about the encrypted portion of messages **)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   188
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   189
lemmas RA2_analz_spies = Says_imp_spies [THEN analz.Inj]
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   190
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   191
lemma RA4_analz_spies:
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   192
     "Says C' B \<lbrace>Crypt K X, X', RA\<rbrace> \<in> set evs ==> RA \<in> analz (spies evs)"
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   193
by blast
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   194
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   195
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   196
(*RA2_analz... and RA4_analz... let us treat those cases using the same
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   197
  argument as for the Fake case.  This is possible for most, but not all,
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   198
  proofs: Fake does not invent new nonces (as in RA2), and of course Fake
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   199
  messages originate from the Spy. *)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   200
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   201
lemmas RA2_parts_spies =  RA2_analz_spies [THEN analz_into_parts]
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   202
lemmas RA4_parts_spies =  RA4_analz_spies [THEN analz_into_parts]
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   203
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   204
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   205
(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   206
    sends messages containing X! **)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   207
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   208
(** Spy never sees another agent's shared key! (unless it's bad at start) **)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   209
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   210
lemma Spy_see_shrK [simp]:
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   211
     "evs \<in> recur ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
13507
febb8e5d2a9d tidying of Isar scripts
paulson
parents: 11655
diff changeset
   212
apply (erule recur.induct, auto)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   213
txt\<open>RA3.  It's ugly to call auto twice, but it seems necessary.\<close>
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   214
apply (auto dest: Key_in_parts_respond simp add: parts_insert_spies)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   215
done
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   216
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   217
lemma Spy_analz_shrK [simp]:
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   218
     "evs \<in> recur ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   219
by auto
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   220
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   221
lemma Spy_see_shrK_D [dest!]:
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   222
     "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> recur|] ==> A \<in> bad"
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   223
by (blast dest: Spy_see_shrK)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   224
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   225
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   226
(*** Proofs involving analz ***)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   227
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   228
(** Session keys are not used to encrypt other session keys **)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   229
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   230
(*Version for "responses" relation.  Handles case RA3 in the theorem below.
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   231
  Note that it holds for *any* set H (not just "spies evs")
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   232
  satisfying the inductive hypothesis.*)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   233
lemma resp_analz_image_freshK_lemma:
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   234
     "[| RB \<in> responses evs;
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   235
         \<forall>K KK. KK \<subseteq> - (range shrK) -->
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   236
                   (Key K \<in> analz (Key`KK Un H)) =
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   237
                   (K \<in> KK | Key K \<in> analz H) |]
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   238
     ==> \<forall>K KK. KK \<subseteq> - (range shrK) -->
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   239
                   (Key K \<in> analz (insert RB (Key`KK Un H))) =
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   240
                   (K \<in> KK | Key K \<in> analz (insert RB H))"
14207
f20fbb141673 Conversion of all main protocols from "Shared" to "Public".
paulson
parents: 14200
diff changeset
   241
apply (erule responses.induct)
f20fbb141673 Conversion of all main protocols from "Shared" to "Public".
paulson
parents: 14200
diff changeset
   242
apply (simp_all del: image_insert
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32404
diff changeset
   243
                add: analz_image_freshK_simps, auto)
14207
f20fbb141673 Conversion of all main protocols from "Shared" to "Public".
paulson
parents: 14200
diff changeset
   244
done 
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   245
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   246
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   247
text\<open>Version for the protocol.  Proof is easy, thanks to the lemma.\<close>
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   248
lemma raw_analz_image_freshK:
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   249
 "evs \<in> recur ==>
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   250
   \<forall>K KK. KK \<subseteq> - (range shrK) -->
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   251
          (Key K \<in> analz (Key`KK Un (spies evs))) =
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   252
          (K \<in> KK | Key K \<in> analz (spies evs))"
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   253
apply (erule recur.induct)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   254
apply (drule_tac [4] RA2_analz_spies,
11281
f2a284b2d588 minor tweaks
paulson
parents: 11270
diff changeset
   255
       drule_tac [5] respond_imp_responses,
13507
febb8e5d2a9d tidying of Isar scripts
paulson
parents: 11655
diff changeset
   256
       drule_tac [6] RA4_analz_spies, analz_freshK, spy_analz)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   257
txt\<open>RA3\<close>
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   258
apply (simp_all add: resp_analz_image_freshK_lemma)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   259
done
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   260
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   261
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   262
(*Instance of the lemma with H replaced by (spies evs):
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   263
   [| RB \<in> responses evs;  evs \<in> recur; |]
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   264
   ==> KK \<subseteq> - (range shrK) -->
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   265
       Key K \<in> analz (insert RB (Key`KK Un spies evs)) =
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   266
       (K \<in> KK | Key K \<in> analz (insert RB (spies evs)))
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   267
*)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   268
lemmas resp_analz_image_freshK =  
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   269
       resp_analz_image_freshK_lemma [OF _ raw_analz_image_freshK]
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   270
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   271
lemma analz_insert_freshK:
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   272
     "[| evs \<in> recur;  KAB \<notin> range shrK |]
11655
923e4d0d36d5 tuned parentheses in relational expressions;
wenzelm
parents: 11281
diff changeset
   273
      ==> (Key K \<in> analz (insert (Key KAB) (spies evs))) =
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   274
          (K = KAB | Key K \<in> analz (spies evs))"
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   275
by (simp del: image_insert
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   276
         add: analz_image_freshK_simps raw_analz_image_freshK)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   277
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   278
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   279
text\<open>Everything that's hashed is already in past traffic.\<close>
11270
a315a3862bb4 better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents: 11264
diff changeset
   280
lemma Hash_imp_body:
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   281
     "[| Hash \<lbrace>Key(shrK A), X\<rbrace> \<in> parts (spies evs);
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   282
         evs \<in> recur;  A \<notin> bad |] ==> X \<in> parts (spies evs)"
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   283
apply (erule rev_mp)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   284
apply (erule recur.induct,
11281
f2a284b2d588 minor tweaks
paulson
parents: 11270
diff changeset
   285
       drule_tac [6] RA4_parts_spies,
f2a284b2d588 minor tweaks
paulson
parents: 11270
diff changeset
   286
       drule_tac [5] respond_imp_responses,
f2a284b2d588 minor tweaks
paulson
parents: 11270
diff changeset
   287
       drule_tac [4] RA2_parts_spies)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   288
txt\<open>RA3 requires a further induction\<close>
13507
febb8e5d2a9d tidying of Isar scripts
paulson
parents: 11655
diff changeset
   289
apply (erule_tac [5] responses.induct, simp_all)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   290
txt\<open>Fake\<close>
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   291
apply (blast intro: parts_insertI)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   292
done
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   293
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   294
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   295
(** The Nonce NA uniquely identifies A's message.
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   296
    This theorem applies to steps RA1 and RA2!
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   297
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   298
  Unicity is not used in other proofs but is desirable in its own right.
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   299
**)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   300
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   301
lemma unique_NA:
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   302
  "[| Hash \<lbrace>Key(shrK A), Agent A, B, NA, P\<rbrace> \<in> parts (spies evs);
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   303
      Hash \<lbrace>Key(shrK A), Agent A, B',NA, P'\<rbrace> \<in> parts (spies evs);
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   304
      evs \<in> recur;  A \<notin> bad |]
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   305
    ==> B=B' & P=P'"
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   306
apply (erule rev_mp, erule rev_mp)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   307
apply (erule recur.induct,
11281
f2a284b2d588 minor tweaks
paulson
parents: 11270
diff changeset
   308
       drule_tac [5] respond_imp_responses)
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   309
apply (force, simp_all)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   310
txt\<open>Fake\<close>
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   311
apply blast
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   312
apply (erule_tac [3] responses.induct)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   313
txt\<open>RA1,2: creation of new Nonce\<close>
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   314
apply simp_all
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   315
apply (blast dest!: Hash_imp_body)+
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   316
done
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   317
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   318
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   319
(*** Lemmas concerning the Server's response
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   320
      (relations "respond" and "responses")
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   321
***)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   322
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   323
lemma shrK_in_analz_respond [simp]:
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   324
     "[| RB \<in> responses evs;  evs \<in> recur |]
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   325
  ==> (Key (shrK B) \<in> analz (insert RB (spies evs))) = (B:bad)"
14207
f20fbb141673 Conversion of all main protocols from "Shared" to "Public".
paulson
parents: 14200
diff changeset
   326
apply (erule responses.induct)
f20fbb141673 Conversion of all main protocols from "Shared" to "Public".
paulson
parents: 14200
diff changeset
   327
apply (simp_all del: image_insert
f20fbb141673 Conversion of all main protocols from "Shared" to "Public".
paulson
parents: 14200
diff changeset
   328
                add: analz_image_freshK_simps resp_analz_image_freshK, auto) 
f20fbb141673 Conversion of all main protocols from "Shared" to "Public".
paulson
parents: 14200
diff changeset
   329
done
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   330
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   331
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   332
lemma resp_analz_insert_lemma:
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   333
     "[| Key K \<in> analz (insert RB H);
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   334
         \<forall>K KK. KK \<subseteq> - (range shrK) -->
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   335
                   (Key K \<in> analz (Key`KK Un H)) =
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   336
                   (K \<in> KK | Key K \<in> analz H);
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   337
         RB \<in> responses evs |]
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   338
     ==> (Key K \<in> parts{RB} | Key K \<in> analz H)"
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   339
apply (erule rev_mp, erule responses.induct)
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 61956
diff changeset
   340
apply (simp_all del: image_insert parts_image
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   341
             add: analz_image_freshK_simps resp_analz_image_freshK_lemma)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   342
txt\<open>Simplification using two distinct treatments of "image"\<close>
13507
febb8e5d2a9d tidying of Isar scripts
paulson
parents: 11655
diff changeset
   343
apply (simp add: parts_insert2, blast)
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   344
done
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   345
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   346
lemmas resp_analz_insert =
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   347
       resp_analz_insert_lemma [OF _ raw_analz_image_freshK]
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   348
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   349
text\<open>The last key returned by respond indeed appears in a certificate\<close>
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   350
lemma respond_certificate:
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   351
     "(Hash[Key(shrK A)] \<lbrace>Agent A, B, NA, P\<rbrace>, RA, K) \<in> respond evs
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   352
      ==> Crypt (shrK A) \<lbrace>Key K, B, NA\<rbrace> \<in> parts {RA}"
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
   353
apply (ind_cases "(Hash[Key (shrK A)] \<lbrace>Agent A, B, NA, P\<rbrace>, RA, K) \<in> respond evs")
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   354
apply simp_all
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   355
done
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   356
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   357
(*This unicity proof differs from all the others in the HOL/Auth directory.
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   358
  The conclusion isn't quite unicity but duplicity, in that there are two
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   359
  possibilities.  Also, the presence of two different matching messages in
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   360
  the inductive step complicates the case analysis.  Unusually for such proofs,
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   361
  the quantifiers appear to be necessary.*)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   362
lemma unique_lemma [rule_format]:
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   363
     "(PB,RB,KXY) \<in> respond evs ==>
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   364
      \<forall>A B N. Crypt (shrK A) \<lbrace>Key K, Agent B, N\<rbrace> \<in> parts {RB} -->
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   365
      (\<forall>A' B' N'. Crypt (shrK A') \<lbrace>Key K, Agent B', N'\<rbrace> \<in> parts {RB} -->
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   366
      (A'=A & B'=B) | (A'=B & B'=A))"
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   367
apply (erule respond.induct)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   368
apply (simp_all add: all_conj_distrib)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   369
apply (blast dest: respond_certificate)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   370
done
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   371
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   372
lemma unique_session_keys:
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   373
     "[| Crypt (shrK A) \<lbrace>Key K, Agent B, N\<rbrace> \<in> parts {RB};
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   374
         Crypt (shrK A') \<lbrace>Key K, Agent B', N'\<rbrace> \<in> parts {RB};
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   375
         (PB,RB,KXY) \<in> respond evs |]
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   376
      ==> (A'=A & B'=B) | (A'=B & B'=A)"
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   377
by (rule unique_lemma, auto)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   378
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   379
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   380
(** Crucial secrecy property: Spy does not see the keys sent in msg RA3
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   381
    Does not in itself guarantee security: an attack could violate
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   382
    the premises, e.g. by having A=Spy **)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   383
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   384
lemma respond_Spy_not_see_session_key [rule_format]:
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   385
     "[| (PB,RB,KAB) \<in> respond evs;  evs \<in> recur |]
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   386
      ==> \<forall>A A' N. A \<notin> bad & A' \<notin> bad -->
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   387
          Crypt (shrK A) \<lbrace>Key K, Agent A', N\<rbrace> \<in> parts{RB} -->
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   388
          Key K \<notin> analz (insert RB (spies evs))"
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   389
apply (erule respond.induct)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   390
apply (frule_tac [2] respond_imp_responses)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   391
apply (frule_tac [2] respond_imp_not_used)
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 61956
diff changeset
   392
apply (simp_all del: image_insert parts_image
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   393
                add: analz_image_freshK_simps split_ifs shrK_in_analz_respond
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   394
                     resp_analz_image_freshK parts_insert2)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   395
txt\<open>Base case of respond\<close>
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   396
apply blast
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   397
txt\<open>Inductive step of respond\<close>
13507
febb8e5d2a9d tidying of Isar scripts
paulson
parents: 11655
diff changeset
   398
apply (intro allI conjI impI, simp_all)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   399
txt\<open>by unicity, either @{term "B=Aa"} or @{term "B=A'"}, a contradiction
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   400
     if @{term "B \<in> bad"}\<close>   
13935
paulson
parents: 13922
diff changeset
   401
apply (blast dest: unique_session_keys respond_certificate)
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   402
apply (blast dest!: respond_certificate)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   403
apply (blast dest!: resp_analz_insert)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   404
done
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   405
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   406
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   407
lemma Spy_not_see_session_key:
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   408
     "[| Crypt (shrK A) \<lbrace>Key K, Agent A', N\<rbrace> \<in> parts (spies evs);
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   409
         A \<notin> bad;  A' \<notin> bad;  evs \<in> recur |]
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   410
      ==> Key K \<notin> analz (spies evs)"
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   411
apply (erule rev_mp)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   412
apply (erule recur.induct)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   413
apply (drule_tac [4] RA2_analz_spies,
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   414
       frule_tac [5] respond_imp_responses,
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   415
       drule_tac [6] RA4_analz_spies,
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   416
       simp_all add: split_ifs analz_insert_eq analz_insert_freshK)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   417
txt\<open>Fake\<close>
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   418
apply spy_analz
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   419
txt\<open>RA2\<close>
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   420
apply blast 
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   421
txt\<open>RA3\<close>
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   422
apply (simp add: parts_insert_spies)
32404
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 24122
diff changeset
   423
apply (metis Key_in_parts_respond parts.Body parts.Fst resp_analz_insert 
da3ca3c6ec81 sledgehammer used to streamline protocol proofs
paulson
parents: 24122
diff changeset
   424
             respond_Spy_not_see_session_key usedI)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   425
txt\<open>RA4\<close>
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   426
apply blast 
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   427
done
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   428
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   429
(**** Authenticity properties for Agents ****)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   430
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   431
text\<open>The response never contains Hashes\<close>
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   432
lemma Hash_in_parts_respond:
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   433
     "[| Hash \<lbrace>Key (shrK B), M\<rbrace> \<in> parts (insert RB H);
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   434
         (PB,RB,K) \<in> respond evs |]
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   435
      ==> Hash \<lbrace>Key (shrK B), M\<rbrace> \<in> parts H"
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   436
apply (erule rev_mp)
13507
febb8e5d2a9d tidying of Isar scripts
paulson
parents: 11655
diff changeset
   437
apply (erule respond_imp_responses [THEN responses.induct], auto)
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   438
done
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   439
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   440
text\<open>Only RA1 or RA2 can have caused such a part of a message to appear.
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   441
  This result is of no use to B, who cannot verify the Hash.  Moreover,
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   442
  it can say nothing about how recent A's message is.  It might later be
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   443
  used to prove B's presence to A at the run's conclusion.\<close>
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   444
lemma Hash_auth_sender [rule_format]:
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   445
     "[| Hash \<lbrace>Key(shrK A), Agent A, Agent B, NA, P\<rbrace> \<in> parts(spies evs);
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   446
         A \<notin> bad;  evs \<in> recur |]
61956
38b73f7940af more symbols;
wenzelm
parents: 61830
diff changeset
   447
      ==> Says A B (Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, NA, P\<rbrace>) \<in> set evs"
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   448
apply (unfold HPair_def)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   449
apply (erule rev_mp)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   450
apply (erule recur.induct,
11281
f2a284b2d588 minor tweaks
paulson
parents: 11270
diff changeset
   451
       drule_tac [6] RA4_parts_spies,
f2a284b2d588 minor tweaks
paulson
parents: 11270
diff changeset
   452
       drule_tac [4] RA2_parts_spies,
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   453
       simp_all)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   454
txt\<open>Fake, RA3\<close>
11281
f2a284b2d588 minor tweaks
paulson
parents: 11270
diff changeset
   455
apply (blast dest: Hash_in_parts_respond)+
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   456
done
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   457
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   458
(** These two results subsume (for all agents) the guarantees proved
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   459
    separately for A and B in the Otway-Rees protocol.
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   460
**)
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   461
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   462
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   463
text\<open>Certificates can only originate with the Server.\<close>
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   464
lemma Cert_imp_Server_msg:
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   465
     "[| Crypt (shrK A) Y \<in> parts (spies evs);
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   466
         A \<notin> bad;  evs \<in> recur |]
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   467
      ==> \<exists>C RC. Says Server C RC \<in> set evs  &
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   468
                   Crypt (shrK A) Y \<in> parts {RC}"
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   469
apply (erule rev_mp, erule recur.induct, simp_all)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   470
txt\<open>Fake\<close>
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   471
apply blast
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   472
txt\<open>RA1\<close>
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   473
apply blast
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   474
txt\<open>RA2: it cannot be a new Nonce, contradiction.\<close>
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   475
apply blast
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   476
txt\<open>RA3.  Pity that the proof is so brittle: this step requires the rewriting,
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   477
       which however would break all other steps.\<close>
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   478
apply (simp add: parts_insert_spies, blast)
61830
4f5ab843cf5b isabelle update_cartouches -c -t;
wenzelm
parents: 58963
diff changeset
   479
txt\<open>RA4\<close>
11264
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   480
apply blast
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   481
done
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   482
a47a9288f3f6 (rough) conversion of Auth/Recur to Isar format
paulson
parents: 11185
diff changeset
   483
end