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