equal
deleted
inserted
replaced
8 Server keys; initial states of agents; new nonces and keys; function "sees" |
8 Server keys; initial states of agents; new nonces and keys; function "sees" |
9 *) |
9 *) |
10 |
10 |
11 |
11 |
12 open Public; |
12 open Public; |
13 |
|
14 (*Injectiveness of new nonces*) |
|
15 AddIffs [inj_newN RS inj_eq]; |
|
16 |
13 |
17 (*Holds because Friend is injective: thus cannot prove for all f*) |
14 (*Holds because Friend is injective: thus cannot prove for all f*) |
18 goal thy "(Friend x : Friend``A) = (x:A)"; |
15 goal thy "(Friend x : Friend``A) = (x:A)"; |
19 by (Auto_tac()); |
16 by (Auto_tac()); |
20 qed "Friend_image_eq"; |
17 qed "Friend_image_eq"; |
50 qed "sees_mono"; |
47 qed "sees_mono"; |
51 |
48 |
52 (*** Basic properties of pubK & priK ***) |
49 (*** Basic properties of pubK & priK ***) |
53 |
50 |
54 AddIffs [inj_pubK RS inj_eq]; |
51 AddIffs [inj_pubK RS inj_eq]; |
|
52 |
|
53 goal thy "!!A B. (priK A = priK B) = (A=B)"; |
|
54 by (Step_tac 1); |
|
55 by (dres_inst_tac [("f","invKey")] arg_cong 1); |
|
56 by (Full_simp_tac 1); |
|
57 qed "priK_inj_eq"; |
|
58 |
|
59 AddIffs [priK_inj_eq]; |
55 AddIffs [priK_neq_pubK, priK_neq_pubK RS not_sym]; |
60 AddIffs [priK_neq_pubK, priK_neq_pubK RS not_sym]; |
56 |
61 |
57 goalw thy [isSymKey_def] "~ isSymKey (pubK A)"; |
62 goalw thy [isSymKey_def] "~ isSymKey (pubK A)"; |
58 by (Simp_tac 1); |
63 by (Simp_tac 1); |
59 qed "not_isSymKey_pubK"; |
64 qed "not_isSymKey_pubK"; |