15 lines
439 B
Plaintext
15 lines
439 B
Plaintext
import "Ascon.cry";
|
|
|
|
for [0,1,2,16,63,64,65,127,128,129,255,256] (\a ->
|
|
for [0,1,2,16,63,64,65,127,128,129,255,256] (\p -> do {
|
|
print ("decrypt_encrypt",a,p);
|
|
prove_print (unint_yices ["Ascon::Ascon_p"]) {{
|
|
\K N (A : [a]) (P : [p]) ->
|
|
(case AEAD128_decrypt K N A C T of
|
|
None -> False
|
|
Some p' -> p' == P
|
|
where
|
|
(C,T) = AEAD128_encrypt K N A P)
|
|
}};
|
|
}));
|