src/HOL/Auth/NS_Public.ML
author paulson
Tue, 16 Dec 1997 15:17:26 +0100
changeset 4422 21238c9d363e
parent 4197 1547bc6daa5a
child 4449 df30e75f670f
permissions -rw-r--r--
Simplified proofs using rewrites for f``A where f is injective
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/NS_Public
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     2
    ID:         $Id$
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     5
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     6
Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     7
Version incorporating Lowe's fix (inclusion of B's identify in round 2).
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     8
*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     9
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    10
open NS_Public;
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    11
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    12
proof_timing:=true;
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    13
HOL_quantifiers := false;
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    14
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
    15
AddIffs [Spy_in_bad];
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    16
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    17
(*A "possibility property": there are traces that reach the end*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    18
goal thy 
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    19
 "!!A B. A ~= B ==> EX NB. EX evs: ns_public.               \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3121
diff changeset
    20
\                     Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    21
by (REPEAT (resolve_tac [exI,bexI] 1));
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    22
by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2497
diff changeset
    23
by possibility_tac;
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    24
result();
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    25
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    26
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    27
(**** Inductive proofs about ns_public ****)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    28
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    29
(*Nobody sends themselves messages*)
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3121
diff changeset
    30
goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs";
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    31
by (etac ns_public.induct 1);
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    32
by (Auto_tac());
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    33
qed_spec_mp "not_Says_to_self";
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    34
Addsimps [not_Says_to_self];
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    35
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    36
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    37
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    38
(*Induction for regularity theorems.  If induction formula has the form
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
    39
   X ~: analz (spies evs) --> ... then it shortens the proof by discarding
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
    40
   needless information about analz (insert X (spies evs))  *)
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    41
fun parts_induct_tac i = 
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    42
    etac ns_public.induct i
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    43
    THEN 
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    44
    REPEAT (FIRSTGOAL analz_mono_contra_tac)
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    45
    THEN 
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    46
    prove_simple_subgoals_tac i;
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    47
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    48
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
    49
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    50
    sends messages containing X! **)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    51
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
    52
(*Spy never sees another agent's private key! (unless it's bad at start)*)
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    53
goal thy 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
    54
 "!!A. evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)";
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    55
by (parts_induct_tac 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
    56
by (Fake_parts_insert_tac 1);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    57
qed "Spy_see_priK";
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    58
Addsimps [Spy_see_priK];
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    59
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4197
diff changeset
    60
AddDs [impOfSubs analz_subset_parts];
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4197
diff changeset
    61
AddDs [Says_imp_spies RS parts.Inj];
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4197
diff changeset
    62
AddDs [impOfSubs Fake_parts_insert];
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4197
diff changeset
    63
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    64
goal thy 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
    65
 "!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4197
diff changeset
    66
by (Auto_tac());
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    67
qed "Spy_analz_priK";
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    68
Addsimps [Spy_analz_priK];
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    69
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
    70
goal thy  "!!A. [| Key (priK A) : parts (spies evs);       \
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
    71
\                  evs : ns_public |] ==> A:bad";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    72
by (blast_tac (claset() addDs [Spy_see_priK]) 1);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    73
qed "Spy_see_priK_D";
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    74
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    75
bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    76
AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    77
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    78
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    79
(**** Authenticity properties obtained from NS2 ****)
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    80
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    81
(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    82
  is secret.  (Honest users generate fresh nonces.)*)
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    83
goal thy 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
    84
 "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
    85
\           Nonce NA ~: analz (spies evs);       \
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    86
\           evs : ns_public |]                      \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
    87
\ ==> Crypt (pubK C) {|NA', Nonce NA, Agent D|} ~: parts (spies evs)";
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    88
by (etac rev_mp 1);
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    89
by (etac rev_mp 1);
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    90
by (parts_induct_tac 1);
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    91
(*NS3*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    92
by (blast_tac (claset() addSEs partsEs) 3);
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    93
(*NS2*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    94
by (blast_tac (claset() addSEs partsEs) 2);
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    95
by (Fake_parts_insert_tac 1);
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    96
qed "no_nonce_NS1_NS2";
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    97
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    98
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
    99
(*Unicity for NS1: nonce NA identifies agents A and B*)
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   100
goal thy 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   101
 "!!evs. [| Nonce NA ~: analz (spies evs);  evs : ns_public |]      \
3709
c13c2137e9ee Tidied proofs, using Clarify_tac
paulson
parents: 3683
diff changeset
   102
\ ==> EX A' B'. ALL A B.                                            \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   103
\      Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   104
\      A=A' & B=B'";
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   105
by (etac rev_mp 1);
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   106
by (parts_induct_tac 1);
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   107
by (ALLGOALS
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   108
    (asm_simp_tac (simpset() addsimps [all_conj_distrib, parts_insert_spies])));
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   109
(*NS1*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   110
by (expand_case_tac "NA = ?y" 2 THEN blast_tac (claset() addSEs partsEs) 2);
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   111
(*Fake*)
3709
c13c2137e9ee Tidied proofs, using Clarify_tac
paulson
parents: 3683
diff changeset
   112
by (Clarify_tac 1);
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   113
by (ex_strip_tac 1);
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   114
by (Fake_parts_insert_tac 1);
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   115
val lemma = result();
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   116
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   117
goal thy 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   118
 "!!evs. [| Crypt(pubK B)  {|Nonce NA, Agent A|}  : parts(spies evs); \
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   119
\           Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   120
\           Nonce NA ~: analz (spies evs);                            \
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   121
\           evs : ns_public |]                                        \
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   122
\        ==> A=A' & B=B'";
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   123
by (prove_unique_tac lemma 1);
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   124
qed "unique_NA";
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   125
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   126
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   127
(*Tactic for proving secrecy theorems*)
2418
6b6a92d05fb2 New tactics: prove_unique_tac and analz_induct_tac
paulson
parents: 2374
diff changeset
   128
fun analz_induct_tac i = 
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   129
    etac ns_public.induct i   THEN
2418
6b6a92d05fb2 New tactics: prove_unique_tac and analz_induct_tac
paulson
parents: 2374
diff changeset
   130
    ALLGOALS (asm_simp_tac 
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   131
              (simpset() addsplits [expand_if]));
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   132
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   133
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   134
(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   135
goal thy 
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   136
 "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs;         \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   137
\           A ~: bad;  B ~: bad;  evs : ns_public |]                        \
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   138
\        ==>  Nonce NA ~: analz (spies evs)";
2536
1e04eb7f7eb1 Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents: 2516
diff changeset
   139
by (etac rev_mp 1);
2418
6b6a92d05fb2 New tactics: prove_unique_tac and analz_induct_tac
paulson
parents: 2374
diff changeset
   140
by (analz_induct_tac 1);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   141
(*NS3*)
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4197
diff changeset
   142
by (blast_tac (claset() addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
2536
1e04eb7f7eb1 Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents: 2516
diff changeset
   143
(*NS2*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   144
by (blast_tac (claset() addSEs [MPair_parts]
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4197
diff changeset
   145
		        addDs  [parts.Body, unique_NA]) 3);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   146
(*NS1*)
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4197
diff changeset
   147
by (blast_tac (claset() addSEs spies_partsEs) 2);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   148
(*Fake*)
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2480
diff changeset
   149
by (spy_analz_tac 1);
2536
1e04eb7f7eb1 Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents: 2516
diff changeset
   150
qed "Spy_not_see_NA";
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   151
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   152
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   153
(*Authentication for A: if she receives message 2 and has used NA
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   154
  to start a run, then B has sent message 2.*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   155
goal thy 
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   156
 "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;  \
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   157
\           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|})   \
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   158
\             : set evs;                                                \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   159
\           A ~: bad;  B ~: bad;  evs : ns_public |]                  \
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   160
\        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|})   \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3121
diff changeset
   161
\              : set evs";
2536
1e04eb7f7eb1 Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents: 2516
diff changeset
   162
by (etac rev_mp 1);
1e04eb7f7eb1 Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents: 2516
diff changeset
   163
(*prepare induction over Crypt (pubK A) {|NA,NB,B|} : parts H*)
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   164
by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   165
by (etac ns_public.induct 1);
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   166
by (ALLGOALS Asm_simp_tac);
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   167
(*NS1*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   168
by (blast_tac (claset() addSEs spies_partsEs) 2);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   169
(*Fake*)
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4197
diff changeset
   170
by (blast_tac (claset() addDs [Spy_not_see_NA]) 1);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   171
qed "A_trusts_NS2";
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   172
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   173
(*If the encrypted message appears then it originated with Alice in NS1*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   174
goal thy 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   175
 "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   176
\           Nonce NA ~: analz (spies evs);                 \
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   177
\           evs : ns_public |]                             \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3121
diff changeset
   178
\   ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
2536
1e04eb7f7eb1 Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents: 2516
diff changeset
   179
by (etac rev_mp 1);
1e04eb7f7eb1 Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents: 2516
diff changeset
   180
by (etac rev_mp 1);
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   181
by (parts_induct_tac 1);
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   182
by (Fake_parts_insert_tac 1);
2536
1e04eb7f7eb1 Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents: 2516
diff changeset
   183
qed "B_trusts_NS1";
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   184
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   185
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   186
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   187
(**** Authenticity properties obtained from NS2 ****)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   188
2480
f9be937df511 Tidied up the unicity proofs
paulson
parents: 2451
diff changeset
   189
(*Unicity for NS2: nonce NB identifies nonce NA and agents A, B 
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   190
  [unicity of B makes Lowe's fix work]
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   191
  [proof closely follows that for unique_NA] *)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   192
goal thy 
3709
c13c2137e9ee Tidied proofs, using Clarify_tac
paulson
parents: 3683
diff changeset
   193
 "!!evs. [| Nonce NB ~: analz (spies evs);  evs : ns_public |]            \
c13c2137e9ee Tidied proofs, using Clarify_tac
paulson
parents: 3683
diff changeset
   194
\ ==> EX A' NA' B'. ALL A NA B.                                           \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   195
\      Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} : parts (spies evs) \
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   196
\         -->  A=A' & NA=NA' & B=B'";
2536
1e04eb7f7eb1 Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents: 2516
diff changeset
   197
by (etac rev_mp 1);
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   198
by (parts_induct_tac 1);
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   199
by (ALLGOALS
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4197
diff changeset
   200
    (asm_simp_tac (simpset() addsimps [all_conj_distrib, 
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4197
diff changeset
   201
				       parts_insert_spies])));
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   202
(*NS2*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   203
by (expand_case_tac "NB = ?y" 2 THEN blast_tac (claset() addSEs partsEs) 2);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   204
(*Fake*)
3709
c13c2137e9ee Tidied proofs, using Clarify_tac
paulson
parents: 3683
diff changeset
   205
by (Clarify_tac 1);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   206
by (ex_strip_tac 1);
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   207
by (Fake_parts_insert_tac 1);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   208
val lemma = result();
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   209
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   210
goal thy 
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   211
 "!!evs. [| Crypt(pubK A)  {|Nonce NA, Nonce NB, Agent B|}   \
3709
c13c2137e9ee Tidied proofs, using Clarify_tac
paulson
parents: 3683
diff changeset
   212
\             : parts(spies evs);                            \
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   213
\           Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \
3709
c13c2137e9ee Tidied proofs, using Clarify_tac
paulson
parents: 3683
diff changeset
   214
\             : parts(spies evs);                            \
c13c2137e9ee Tidied proofs, using Clarify_tac
paulson
parents: 3683
diff changeset
   215
\           Nonce NB ~: analz (spies evs);                   \
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   216
\           evs : ns_public |]                               \
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   217
\        ==> A=A' & NA=NA' & B=B'";
2418
6b6a92d05fb2 New tactics: prove_unique_tac and analz_induct_tac
paulson
parents: 2374
diff changeset
   218
by (prove_unique_tac lemma 1);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   219
qed "unique_NB";
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   220
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   221
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   222
(*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   223
goal thy 
2536
1e04eb7f7eb1 Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents: 2516
diff changeset
   224
 "!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   225
\             : set evs;                                              \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   226
\           A ~: bad;  B ~: bad;  evs : ns_public |]                \
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   227
\ ==> Nonce NB ~: analz (spies evs)";
2536
1e04eb7f7eb1 Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents: 2516
diff changeset
   228
by (etac rev_mp 1);
2418
6b6a92d05fb2 New tactics: prove_unique_tac and analz_induct_tac
paulson
parents: 2374
diff changeset
   229
by (analz_induct_tac 1);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   230
(*NS3*)
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4197
diff changeset
   231
by (blast_tac (claset() addDs [unique_NB]) 4);
3709
c13c2137e9ee Tidied proofs, using Clarify_tac
paulson
parents: 3683
diff changeset
   232
(*NS2: by freshness and unicity of NB*)
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4197
diff changeset
   233
by (blast_tac (claset() addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4197
diff changeset
   234
                        addEs partsEs) 3);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   235
(*NS1*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   236
by (blast_tac (claset() addSEs spies_partsEs) 2);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   237
(*Fake*)
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2480
diff changeset
   238
by (spy_analz_tac 1);
2536
1e04eb7f7eb1 Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents: 2516
diff changeset
   239
qed "Spy_not_see_NB";
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   240
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4197
diff changeset
   241
AddDs [Spy_not_see_NB];
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4197
diff changeset
   242
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   243
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   244
(*Authentication for B: if he receives message 3 and has used NB
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   245
  in message 2, then A has sent message 3.*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   246
goal thy 
2536
1e04eb7f7eb1 Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents: 2516
diff changeset
   247
 "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   248
\             : set evs;                                               \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   249
\           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;            \
4197
1547bc6daa5a Made some proofs more robust
paulson
parents: 4091
diff changeset
   250
\           A ~: bad;  B ~: bad;  evs : ns_public |]                   \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3121
diff changeset
   251
\        ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
2536
1e04eb7f7eb1 Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents: 2516
diff changeset
   252
by (etac rev_mp 1);
1e04eb7f7eb1 Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents: 2516
diff changeset
   253
(*prepare induction over Crypt (pubK B) NB : parts H*)
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   254
by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3516
diff changeset
   255
by (parts_induct_tac 1);
3709
c13c2137e9ee Tidied proofs, using Clarify_tac
paulson
parents: 3683
diff changeset
   256
by (ALLGOALS Clarify_tac);
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4197
diff changeset
   257
(*NS3: because NB determines A*)
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4197
diff changeset
   258
by (blast_tac (claset() addDs [unique_NB]) 3);
3709
c13c2137e9ee Tidied proofs, using Clarify_tac
paulson
parents: 3683
diff changeset
   259
(*NS1: by freshness*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   260
by (blast_tac (claset() addSEs spies_partsEs) 2);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   261
(*Fake*)
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4197
diff changeset
   262
by (Blast_tac 1);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   263
qed "B_trusts_NS3";
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   264
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   265
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   266
(**** Overall guarantee for B*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   267
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   268
(*Matches only NS2, not NS1 (or NS3)*)
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   269
val Says_imp_spies' = 
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   270
    read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_spies;
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   271
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2637
diff changeset
   272
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   273
(*If B receives NS3 and the nonce NB agrees with the nonce he joined with
2536
1e04eb7f7eb1 Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents: 2516
diff changeset
   274
  NA, then A initiated the run using NA.  SAME proof as B_trusts_NS3!*)
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   275
goal thy 
2536
1e04eb7f7eb1 Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents: 2516
diff changeset
   276
 "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   277
\             : set evs;                                               \
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
   278
\           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;            \
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   279
\           A ~: bad;  B ~: bad;  evs : ns_public |]                 \
3465
e85c24717cad set_of_list -> set
nipkow
parents: 3121
diff changeset
   280
\    ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
2536
1e04eb7f7eb1 Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents: 2516
diff changeset
   281
by (etac rev_mp 1);
1e04eb7f7eb1 Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents: 2516
diff changeset
   282
(*prepare induction over Crypt (pubK B) {|NB|} : parts H*)
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3675
diff changeset
   283
by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   284
by (etac ns_public.induct 1);
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   285
by (ALLGOALS Asm_simp_tac);
3709
c13c2137e9ee Tidied proofs, using Clarify_tac
paulson
parents: 3683
diff changeset
   286
by (ALLGOALS Clarify_tac);
4197
1547bc6daa5a Made some proofs more robust
paulson
parents: 4091
diff changeset
   287
(*NS3: because NB determines A and NA*)
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4197
diff changeset
   288
by (blast_tac (claset() addDs [unique_NB]) 3);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   289
(*NS1*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   290
by (blast_tac (claset() addSEs spies_partsEs) 2);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   291
(*Fake*)
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4197
diff changeset
   292
by (Blast_tac 1);
2536
1e04eb7f7eb1 Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
paulson
parents: 2516
diff changeset
   293
qed "B_trusts_protocol";
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   294