equal
deleted
inserted
replaced
51 text{*By freeness of agents, no two agents have the same key. Since |
51 text{*By freeness of agents, no two agents have the same key. Since |
52 @{term "True\<noteq>False"}, no agent has identical signing and encryption keys*} |
52 @{term "True\<noteq>False"}, no agent has identical signing and encryption keys*} |
53 specification (publicKey) |
53 specification (publicKey) |
54 injective_publicKey: |
54 injective_publicKey: |
55 "publicKey b A = publicKey c A' ==> b=c & A=A'" |
55 "publicKey b A = publicKey c A' ==> b=c & A=A'" |
56 apply (rule exI [of _ "%b A. 2 * agent_case 0 (\<lambda>n. n + 2) 1 A + (if b then 1 else 0)"]) |
56 apply (rule exI [of _ "%b A. 2 * agent_case 0 (\<lambda>n. n + 2) 1 A + (if b then 1 else 0)"]) |
57 apply (auto simp add: inj_on_def split: agent.split, presburger+) |
57 apply (auto simp add: inj_on_def split: agent.split, presburger+) |
58 (*faster would be this: |
58 (*faster would be this: |
|
59 apply (simp split: agent.split, auto) |
59 apply (drule_tac f="%x. x mod 2" in arg_cong, simp add: mod_Suc)+ |
60 apply (drule_tac f="%x. x mod 2" in arg_cong, simp add: mod_Suc)+ |
60 *) |
61 *) |
61 done |
62 done |
62 |
63 |
63 |
64 |