22 qed "priK_inj_eq"; |
22 qed "priK_inj_eq"; |
23 |
23 |
24 AddIffs [priK_inj_eq]; |
24 AddIffs [priK_inj_eq]; |
25 AddIffs [priK_neq_pubK, priK_neq_pubK RS not_sym]; |
25 AddIffs [priK_neq_pubK, priK_neq_pubK RS not_sym]; |
26 |
26 |
27 Goalw [isSymKey_def] "~ isSymKey (pubK A)"; |
27 Goalw [symKeys_def] "pubK A \\<notin> symKeys"; |
28 by (Simp_tac 1); |
28 by (Simp_tac 1); |
29 qed "not_isSymKey_pubK"; |
29 qed "not_symKeys_pubK"; |
30 |
30 |
31 Goalw [isSymKey_def] "~ isSymKey (priK A)"; |
31 Goalw [symKeys_def] "priK A \\<notin> symKeys"; |
32 by (Simp_tac 1); |
32 by (Simp_tac 1); |
33 qed "not_isSymKey_priK"; |
33 qed "not_symKeys_priK"; |
34 |
34 |
35 AddIffs [not_isSymKey_pubK, not_isSymKey_priK]; |
35 AddIffs [not_symKeys_pubK, not_symKeys_priK]; |
36 |
36 |
37 Goal "[| Crypt K X \\<in> analz H; isSymKey K; Key K \\<in> analz H |] \ |
37 Goal "(K \\<in> symKeys) \\<noteq> (K' \\<in> symKeys) ==> K \\<noteq> K'"; |
|
38 by (Blast_tac 1); |
|
39 qed "symKeys_neq_imp_neq"; |
|
40 |
|
41 Goal "[| Crypt K X \\<in> analz H; K \\<in> symKeys; Key K \\<in> analz H |] \ |
38 \ ==> X \\<in> analz H"; |
42 \ ==> X \\<in> analz H"; |
39 by (auto_tac(claset(), simpset() addsimps [isSymKey_def])); |
43 by (auto_tac(claset(), simpset() addsimps [symKeys_def])); |
40 qed "analz_isSymKey_Decrypt"; |
44 qed "analz_symKeys_Decrypt"; |
41 |
45 |
42 |
46 |
43 (** "Image" equations that hold for injective functions **) |
47 (** "Image" equations that hold for injective functions **) |
44 |
48 |
45 Goal "(invKey x : invKey`A) = (x:A)"; |
49 Goal "(invKey x : invKey`A) = (x:A)"; |