18 datatype keymode = Signature | Encryption |
18 datatype keymode = Signature | Encryption |
19 |
19 |
20 consts |
20 consts |
21 publicKey :: "[keymode,agent] => key" |
21 publicKey :: "[keymode,agent] => key" |
22 |
22 |
23 syntax |
23 abbreviation |
24 pubEK :: "agent => key" |
24 pubEK :: "agent => key" |
|
25 "pubEK == publicKey Encryption" |
|
26 |
25 pubSK :: "agent => key" |
27 pubSK :: "agent => key" |
26 |
28 "pubSK == publicKey Signature" |
27 privateKey :: "[bool,agent] => key" |
29 |
|
30 privateKey :: "[keymode, agent] => key" |
|
31 "privateKey b A == invKey (publicKey b A)" |
|
32 |
|
33 (*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*) |
28 priEK :: "agent => key" |
34 priEK :: "agent => key" |
|
35 "priEK A == privateKey Encryption A" |
29 priSK :: "agent => key" |
36 priSK :: "agent => key" |
30 |
37 "priSK A == privateKey Signature A" |
31 translations |
38 |
32 "pubEK" == "publicKey Encryption" |
39 |
33 "pubSK" == "publicKey Signature" |
40 text{*These abbreviations give backward compatibility. They represent the |
34 |
|
35 (*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*) |
|
36 "privateKey b A" == "invKey (publicKey b A)" |
|
37 "priEK A" == "privateKey Encryption A" |
|
38 "priSK A" == "privateKey Signature A" |
|
39 |
|
40 |
|
41 text{*These translations give backward compatibility. They represent the |
|
42 simple situation where the signature and encryption keys are the same.*} |
41 simple situation where the signature and encryption keys are the same.*} |
43 syntax |
42 |
|
43 abbreviation |
44 pubK :: "agent => key" |
44 pubK :: "agent => key" |
|
45 "pubK A == pubEK A" |
|
46 |
45 priK :: "agent => key" |
47 priK :: "agent => key" |
46 |
48 "priK A == invKey (pubEK A)" |
47 translations |
|
48 "pubK A" == "pubEK A" |
|
49 "priK A" == "invKey (pubEK A)" |
|
50 |
49 |
51 |
50 |
52 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 |
53 @{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*} |
54 specification (publicKey) |
53 specification (publicKey) |