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

Fixup saw proofs

Browse Source
This commit is contained in:
Eric Mertens
2025-09-07 20:27:48 -07:00
parent 1acbbe633f
commit 8813e6066f
1 changed files with 5 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
verify.saw
View File

@@ -5,8 +5,10 @@ for [0,1,2,16,63,64,65,127,128,129,255,256] (\p -> do {
print ("decrypt_encrypt",a,p); print ("decrypt_encrypt",a,p);
prove_print (unint_yices ["Ascon::Ascon_p"]) {{ prove_print (unint_yices ["Ascon::Ascon_p"]) {{
\K N (A : [a]) (P : [p]) -> \K N (A : [a]) (P : [p]) ->
case AEAD128_decrypt K N A (AEAD128_encrypt K N A P) of (case AEAD128_decrypt K N A C T of
None -> False None -> False
Some p' -> p' == P Some p' -> p' == P
where
(C,T) = AEAD128_encrypt K N A P)
}}; }};
})); }));