19 lines
434 B
Text
19 lines
434 B
Text
|
type key. (* encryption keys, key_len bits *)
|
||
|
|
type text. (* plaintexts, text_len bits *)
|
||
|
|
type cipher. (* ciphertexts *)
|
||
|
|
|
||
|
|
module type ENC = {
|
||
|
|
proc key_gen(): key
|
||
|
|
proc enc(k: key, x: text): cipher
|
||
|
|
proc dec(k: key, c: cipher): text
|
||
|
|
}
|
||
|
|
|
||
|
|
module Cor (Enc: ENC) = {
|
||
|
|
proc main(x: text): bool = {
|
||
|
|
var k: key; var c: cipher; var y: text;
|
||
|
|
k <@ Enc.key_gen();
|
||
|
|
c <@ Enc.enc(k, x);
|
||
|
|
y <@ Enc.dec(k, c);
|
||
|
|
return x = y;
|
||
|
|
}
|
||
|
|
}
|