equal
deleted
inserted
replaced
32 Keys are just natural numbers. Function @{text invKey} maps a public key to |
32 Keys are just natural numbers. Function @{text invKey} maps a public key to |
33 the matching private key, and vice versa: |
33 the matching private key, and vice versa: |
34 *} |
34 *} |
35 |
35 |
36 types key = nat |
36 types key = nat |
37 consts invKey :: "key=>key" |
37 consts invKey :: "key \<Rightarrow> key" |
38 (*<*) |
38 (*<*) |
39 consts all_symmetric :: bool --{*true if all keys are symmetric*} |
39 consts all_symmetric :: bool --{*true if all keys are symmetric*} |
40 |
40 |
41 specification (invKey) |
41 specification (invKey) |
42 invKey [simp]: "invKey (invKey K) = K" |
42 invKey [simp]: "invKey (invKey K) = K" |