mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-25 17:04:31 +03:00
74 lines
2.5 KiB
Plaintext
74 lines
2.5 KiB
Plaintext
/*
|
||
Author : Sean Weaver <saweave@tycho.ncsc.mil>
|
||
This is a rough Cryptol specification of Even-Mansour:
|
||
|
||
Even, S., Mansour, Y.: A Construction of a Cipher from a Single
|
||
Pseudorandom Permutation. J. Cryptology 10 (3) (1997) 151–162
|
||
*/
|
||
|
||
/** Pick some permutation F (here we select one at random) */
|
||
F = (generate_random_permutation 1942611697)
|
||
|
||
property is_a_permutation a = (unique a) /\ (leq a (length(a)-1))
|
||
// Main> is_a_permutation (F:[10][4])
|
||
// True
|
||
|
||
/** Calculate F inverse */
|
||
F' = inverse_permutation F
|
||
|
||
property is_inverse_permutation x a a' = ((x@@a)@@a') == x
|
||
// Main> is_inverse_permutation ([0..9]:[_][4]) (F:[10]_) (F':[10]_)
|
||
// True
|
||
|
||
/**
|
||
* The encryption (or cryptogram) E_K(M) of a message M in {0,1}^n by
|
||
* the key K = <K_1, K_2>, is performed by E
|
||
*/
|
||
E : {n} (fin n, n >= 1, width n >= width(n-1)) => ([n], [n]) -> [n] -> [n]
|
||
E (K1, K2) M = (M^K1)@@F ^ K2
|
||
|
||
/**
|
||
* The decryption of a cryptogram C in {0,1}^n, is performed by D
|
||
*/
|
||
D : {n} (fin n, n >= 1, width n >= width(n-1)) => ([n], [n]) -> [n] -> [n]
|
||
D (K1, K2) C = (C^K2)@@F' ^ K1
|
||
|
||
/**
|
||
* It is easy to verify that for every M in {0,1}^n and K in {0,1}^2n,
|
||
* the following identity holds D_K(E_K(M)) = M, i.e. D_K decrypts
|
||
* messages that were encrypted using E_K.
|
||
*/
|
||
property E_and_D_are_inverses K M = (D K (E K M)) == M
|
||
|
||
|
||
/******* Utilities *******/
|
||
|
||
swap : {a, b} (fin a, a >= 1) => [a]b -> [width(a-1)] -> [width(a-1)] -> [a]b
|
||
swap xs a b = [ if(i == a) then xs@b
|
||
|(i == b) then xs@a
|
||
else xs@i
|
||
| i <- [0 .. a-1] ]
|
||
|
||
generate_random_permutation : {a} (fin a, a >= 1, width a >= width(a-1)) => [256] -> [a][width(a-1)]
|
||
generate_random_permutation seed = pss!0
|
||
where
|
||
indices = [ take `{width(a-1)} (b % `a) | b <- (random seed) : [a][width a] ]
|
||
pss = [ [0 .. a-1] ] # [ swap ps a b | ps <- pss | a <- [0 .. a-1] | b <- indices ]
|
||
|
||
unique : {a, b} (fin a, fin b, a>=1) => [a][b] -> Bit
|
||
unique xs = [ exist x (i+1) | x <- xs | i <- [0...] ] == 0
|
||
where exist : [b] -> [width a] -> Bit
|
||
exist x i = if(i>=`a) then False
|
||
else if(x==(xs@i)) then True
|
||
else exist x (i+1)
|
||
|
||
leq xs a = [ x <= a | x <- xs ] == ~0
|
||
|
||
index_of : {a, b} (fin a, a>=1, Cmp b) => [a]b -> b -> [width(a-1)]
|
||
index_of xs a = (ret!0).1
|
||
where ret = [(False, 0)] # [ if(xs@i == a) then (True, i) else r
|
||
| i <- [0 .. a-1 ]
|
||
| r <- ret ]
|
||
|
||
inverse_permutation : {a} (fin a, a >= 1) => [a][width(a-1)] -> [a][width(a-1)]
|
||
inverse_permutation perm = [ index_of perm i | i <- [0 .. a-1 ] ] |