finally add Even-Mansour example; closes #124

examples/contrib/EvenMansour.cry

@@ -0,0 +1,74 @@
+/*
+  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 (width(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)) => [32] -> [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 ] ]

tests/regression/EvenMansour.icry

@@ -0,0 +1,4 @@
+:l ../../examples/contrib/EvenMansour.cry
+:check is_a_permutation (F:[10][4])
+:check is_inverse_permutation ([0..9]:[_][4]) (F:[10]_) (F':[10]_)
+:check E_and_D_are_inverses : ([10],[10]) -> [10] -> Bit

tests/regression/EvenMansour.icry.stdout

@@ -0,0 +1,12 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+Using exhaustive testing.
+testing...passed 1 tests.
+Q.E.D.
+Using exhaustive testing.
+testing...passed 1 tests.
+Q.E.D.
+Using random testing.
+testing...passed 100 tests.
+Coverage: 0.00% (100 of 2^^30 values)