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

Add saw proof for AEAD inversion

Browse Source
This commit is contained in:
Eric Mertens
2025-09-07 10:41:52 -07:00
parent 671aac130f
commit 8c9c356220
2 changed files with 17 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
Makefile
View File

@@ -1,6 +1,7 @@
.PHONY: test test-hash256 test-xof128 test-cxof128 test-aead128 .PHONY: test test-hash256 test-xof128 test-cxof128 test-aead128 saw-proofs
CRYPTOL ?= cryptol CRYPTOL ?= cryptol
SAW ?= saw
test: test-hash256 test-xof128 test-cxof128 test-aead128 test: test-hash256 test-xof128 test-cxof128 test-aead128
@@ -15,3 +16,6 @@ test-cxof128:
test-aead128: test-aead128:
$(CRYPTOL) -c :exhaust TestAsconAEAD128.cry $(CRYPTOL) -c :exhaust TestAsconAEAD128.cry
saw-proofs:
$(SAW) verify.saw

12
verify.saw Normal file
View File

@@ -0,0 +1,12 @@
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 (AEAD128_encrypt K N A P) of
None -> False
Some p' -> p' == P
}};
}));