glguy/ascon
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Update tests for AEAD change

Browse Source
This commit is contained in:
Eric Mertens
2025-09-09 20:55:16 -07:00
parent a3d978a4b3
commit 6287904204
2 changed files with 8 additions and 9 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
TestAsconAEAD128.cry
View File

@@ -3,10 +3,10 @@ module TestAsconAEAD128 where
import Ascon
testcase : {n, m} (fin m, fin n) => [128] -> [128] -> [8 * m] -> [8 * n] -> [8 * (m + 16)] -> Bit
testcase K N P A C =
AEAD128_encrypt_bytes (split K) (split N) (split A) (split P) == split C
testcase K N P A (C # T) =
AEAD128_encrypt_bytes (split K) (split N) (split A) (split P) == (split C, split T)
/\
case AEAD128_decrypt_bytes (split K) (split N) (split A) (split C) of
case AEAD128_decrypt_bytes (split K) (split N) (split A) (split C) (split T) of
None -> False
Some p -> p == split P

9
verify.saw
View File

@@ -4,11 +4,10 @@ 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
\K N (A : [0]) (P : [128]) ->
(T == T'
where
(C,T) = AEAD128_encrypt K N A P)
(C, T) = AEAD128_encrypt K N A P
(P', T') = AEAD128_decrypt_raw K N A C)
}};
}));