equal
deleted
inserted
replaced
17 (*Injectiveness: Agents' long-term keys are distinct.*) |
17 (*Injectiveness: Agents' long-term keys are distinct.*) |
18 AddIffs [inj_shrK RS inj_eq]; |
18 AddIffs [inj_shrK RS inj_eq]; |
19 |
19 |
20 (* invKey(shrK A) = shrK A *) |
20 (* invKey(shrK A) = shrK A *) |
21 Addsimps [rewrite_rule [isSymKey_def] isSym_keys]; |
21 Addsimps [rewrite_rule [isSymKey_def] isSym_keys]; |
|
22 |
|
23 |
|
24 Goal "[| Crypt K X \\<in> analz H; Key K \\<in> analz H |] ==> X \\<in> analz H"; |
|
25 by Auto_tac; |
|
26 qed "analz_Decrypt'"; |
|
27 AddDs [analz_Decrypt']; |
|
28 Delrules [analz.Decrypt]; |
22 |
29 |
23 (** Rewrites should not refer to initState(Friend i) |
30 (** Rewrites should not refer to initState(Friend i) |
24 -- not in normal form! **) |
31 -- not in normal form! **) |
25 |
32 |
26 Goalw [keysFor_def] "keysFor (parts (initState C)) = {}"; |
33 Goalw [keysFor_def] "keysFor (parts (initState C)) = {}"; |