src/HOL/Auth/WooLam.ML
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
parent 3471 cd37ec057028
child 3519 ab0a9fbed4c0
permissions -rw-r--r--
Moving common declarations and proofs from theories "Shared" and "Public" to "Event". NB the original "Event" theory was later renamed "Shared". Addition of the Notes constructor to datatype "event".
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/WooLam
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     2
    ID:         $Id$
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     5
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     6
Inductive relation "woolam" for the Woo-Lam protocol.
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     7
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     8
Simplified version from page 11 of
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     9
  Abadi and Needham.  Prudent Engineering Practice for Cryptographic Protocols.
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    10
  IEEE Trans. S.E. 22(1), 1996, pages 6-15.
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    11
*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    12
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    13
open WooLam;
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    14
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    15
proof_timing:=true;
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    16
HOL_quantifiers := false;
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    17
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    18
2321
083912bc5775 Updated a comment
paulson
parents: 2283
diff changeset
    19
(*A "possibility property": there are traces that reach the end*)
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    20
goal thy 
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    21
 "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    22
\        ==> EX NB. EX evs: woolam.               \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
    23
\              Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) : set evs";
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    24
by (REPEAT (resolve_tac [exI,bexI] 1));
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    25
by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS 
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    26
          woolam.WL4 RS woolam.WL5) 2);
3471
cd37ec057028 Now the possibility proof calls the appropriate tactic
paulson
parents: 3466
diff changeset
    27
by possibility_tac;
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    28
result();
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    29
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    30
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    31
(**** Inductive proofs about woolam ****)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    32
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    33
(*Nobody sends themselves messages*)
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3121
diff changeset
    34
goal thy "!!evs. evs : woolam ==> ALL A X. Says A A X ~: set evs";
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    35
by (etac woolam.induct 1);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    36
by (Auto_tac());
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    37
qed_spec_mp "not_Says_to_self";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    38
Addsimps [not_Says_to_self];
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    39
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    40
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    41
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    42
(** For reasoning about the encrypted portion of messages **)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    43
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3121
diff changeset
    44
goal thy "!!evs. Says A' B X : set evs \
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    45
\                ==> X : analz (sees lost Spy evs)";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    46
by (etac (Says_imp_sees_Spy RS analz.Inj) 1);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    47
qed "WL4_analz_sees_Spy";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    48
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    49
bind_thm ("WL4_parts_sees_Spy",
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    50
          WL4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    51
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    52
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    53
val parts_induct_tac = 
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    54
    etac woolam.induct 1  THEN 
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    55
    forward_tac [WL4_parts_sees_Spy] 6  THEN
3471
cd37ec057028 Now the possibility proof calls the appropriate tactic
paulson
parents: 3466
diff changeset
    56
    prove_simple_subgoals_tac 1;
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    57
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    58
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    59
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    60
    sends messages containing X! **)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    61
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    62
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    63
goal thy 
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    64
 "!!evs. evs : woolam \
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    65
\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    66
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    67
by (Fake_parts_insert_tac 1);
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    68
qed "Spy_see_shrK";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    69
Addsimps [Spy_see_shrK];
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    70
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    71
goal thy 
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    72
 "!!evs. evs : woolam \
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    73
\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    74
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    75
qed "Spy_analz_shrK";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    76
Addsimps [Spy_analz_shrK];
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    77
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    78
goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    79
\                  evs : woolam |] ==> A:lost";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    80
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    81
qed "Spy_see_shrK_D";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    82
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    83
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    84
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    85
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    86
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    87
(**** Autheticity properties for Woo-Lam ****)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    88
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    89
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    90
(*** WL4 ***)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    91
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    92
(*If the encrypted message appears then it originated with Alice*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    93
goal thy 
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    94
 "!!evs. [| A ~: lost;  evs : woolam |]                   \
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    95
\    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs)        \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3121
diff changeset
    96
\        --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs)";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    97
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    98
by (Fake_parts_insert_tac 1);
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    99
by (Blast_tac 1);
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   100
qed_spec_mp "NB_Crypt_imp_Alice_msg";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   101
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   102
(*Guarantee for Server: if it gets a message containing a certificate from 
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   103
  Alice, then she originated that certificate.  But we DO NOT know that B
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   104
  ever saw it: the Spy may have rerouted the message to the Server.*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   105
goal thy 
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   106
 "!!evs. [| A ~: lost;  evs : woolam;                      \
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   107
\           Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3121
diff changeset
   108
\            : set evs |]                                  \
e85c24717cad set_of_list -> set
nipkow
parents: 3121
diff changeset
   109
\        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   110
by (blast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg]
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   111
                      addSEs [MPair_parts]
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   112
                      addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
2321
083912bc5775 Updated a comment
paulson
parents: 2283
diff changeset
   113
qed "Server_trusts_WL4";
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   114
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   115
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   116
(*** WL5 ***)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   117
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   118
(*Server sent WL5 only if it received the right sort of message*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   119
goal thy 
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   120
 "!!evs. evs : woolam ==>                                                   \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   121
\        Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs           \
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   122
\        --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3121
diff changeset
   123
\               : set evs)";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   124
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   125
by (Fake_parts_insert_tac 1);
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   126
by (ALLGOALS Blast_tac);
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   127
bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp));
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   128
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   129
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   130
(*If the encrypted message appears then it originated with the Server!*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   131
goal thy 
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   132
 "!!evs. [| B ~: lost;  evs : woolam |]                                  \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   133
\        ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs)  \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3121
diff changeset
   134
\        --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   135
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   136
by (Fake_parts_insert_tac 1);
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   137
qed_spec_mp "NB_Crypt_imp_Server_msg";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   138
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   139
(*Partial guarantee for B: if it gets a message of correct form then the Server
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   140
  sent the same message.*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   141
goal thy 
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   142
 "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set evs;         \
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   143
\           B ~: lost;  evs : woolam |]                                  \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3121
diff changeset
   144
\        ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   145
by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   146
                      addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   147
qed "B_got_WL5";
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   148
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   149
(*Guarantee for B.  If B gets the Server's certificate then A has encrypted
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   150
  the nonce using her key.  This event can be no older than the nonce itself.
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   151
  But A may have sent the nonce to some other agent and it could have reached
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   152
  the Server via the Spy.*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   153
goal thy 
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3121
diff changeset
   154
 "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs; \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   155
\           A ~: lost;  B ~: lost;  evs : woolam  |]                  \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3121
diff changeset
   156
\        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   157
by (blast_tac (!claset addIs  [Server_trusts_WL4]
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   158
                      addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
2321
083912bc5775 Updated a comment
paulson
parents: 2283
diff changeset
   159
qed "B_trusts_WL5";
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   160
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   161
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   162
(*B only issues challenges in response to WL1.  Useful??*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   163
goal thy 
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   164
 "!!evs. [| B ~= Spy;  evs : woolam |]                   \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3121
diff changeset
   165
\    ==> Says B A (Nonce NB) : set evs        \
e85c24717cad set_of_list -> set
nipkow
parents: 3121
diff changeset
   166
\        --> (EX A'. Says A' B (Agent A) : set evs)";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   167
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   168
by (Fake_parts_insert_tac 1);
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   169
by (ALLGOALS Blast_tac);
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   170
bind_thm ("B_said_WL2", result() RSN (2, rev_mp));
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   171
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   172
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   173
(**CANNOT be proved because A doesn't know where challenges come from...
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   174
goal thy 
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   175
 "!!evs. [| A ~: lost;  B ~= Spy;  evs : woolam |]                \
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
   176
\    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) &  \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   177
\        Says B A (Nonce NB) : set evs                            \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3121
diff changeset
   178
\        --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   179
by parts_induct_tac;
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   180
by (Fake_parts_insert_tac 1);
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   181
by (Step_tac 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   182
by (blast_tac (!claset addSEs partsEs) 1);
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
   183
**)