equal
deleted
inserted
replaced
45 Two axioms are asserted about the public-key cryptosystem. |
45 Two axioms are asserted about the public-key cryptosystem. |
46 No two agents have the same public key, and no private key equals |
46 No two agents have the same public key, and no private key equals |
47 any public key. |
47 any public key. |
48 *} |
48 *} |
49 |
49 |
50 axioms |
50 axiomatization where |
51 inj_pubK: "inj pubK" |
51 inj_pubK: "inj pubK" and |
52 priK_neq_pubK: "priK A \<noteq> pubK B" |
52 priK_neq_pubK: "priK A \<noteq> pubK B" |
53 (*<*) |
53 (*<*) |
54 lemmas [iff] = inj_pubK [THEN inj_eq] |
54 lemmas [iff] = inj_pubK [THEN inj_eq] |
55 |
55 |
56 lemma priK_inj_eq[iff]: "(priK A = priK B) = (A=B)" |
56 lemma priK_inj_eq[iff]: "(priK A = priK B) = (A=B)" |