127 lines
3.2 KiB
Plaintext
127 lines
3.2 KiB
Plaintext
m <- llvm_load_module "aead.bc";
|
|
|
|
include "common.saw";
|
|
|
|
thm_P8 <- mk_P8;
|
|
thm_P12 <- mk_P12;
|
|
|
|
let N_len = 16;
|
|
let N_type = llvm_array N_len i8;
|
|
|
|
let K_len = 16;
|
|
let K_type = llvm_array K_len i8;
|
|
|
|
let T_len = 16;
|
|
let T_type = llvm_array T_len i8;
|
|
|
|
let verify_encrypt A_len P_len = do {
|
|
llvm_verify
|
|
m "crypto_aead_encrypt"
|
|
[thm_P12, thm_P8]
|
|
false
|
|
do {
|
|
// Inputs
|
|
|
|
let A_type = llvm_array A_len i8;
|
|
let P_type = llvm_array P_len i8;
|
|
|
|
let CT_len = eval_size {| P_len + T_len |};
|
|
let CT_type = llvm_array CT_len i8;
|
|
|
|
(P, P_ptr) <- fresh_alloc_readonly "P" P_type;
|
|
(A, A_ptr) <- fresh_alloc_readonly "A" A_type;
|
|
(N, N_ptr) <- fresh_alloc_readonly "N" N_type;
|
|
(K, K_ptr) <- fresh_alloc_readonly "K" K_type;
|
|
|
|
// Outputs
|
|
|
|
CT_ptr <- llvm_alloc CT_type;
|
|
CTLEN_ptr <- llvm_alloc i64;
|
|
|
|
llvm_execute_func
|
|
[ CT_ptr, CTLEN_ptr
|
|
, P_ptr, llvm_term {{ `P_len:[64] }}
|
|
, A_ptr, llvm_term {{ `A_len:[64] }}
|
|
, llvm_null
|
|
, N_ptr
|
|
, K_ptr
|
|
];
|
|
|
|
llvm_points_to CTLEN_ptr (llvm_term {{ `CT_len : [64] }});
|
|
llvm_points_to CT_ptr (llvm_term {{ C # T where (C,T) = AEAD128_encrypt_bytes K N A P }});
|
|
llvm_return (llvm_term {{ 0 : [32] }});
|
|
}
|
|
(unint_yices ["Ascon::Ascon_p"]);
|
|
};
|
|
|
|
let verify_decrypt A_len P_len = do {
|
|
llvm_verify
|
|
m "crypto_aead_decrypt"
|
|
[thm_P12, thm_P8]
|
|
false
|
|
do {
|
|
let CT_len = eval_size {| P_len + T_len |};
|
|
|
|
let C_type = llvm_array P_len i8;
|
|
let CT_type = llvm_array CT_len i8;
|
|
let A_type = llvm_array A_len i8;
|
|
let P_type = llvm_array P_len i8;
|
|
|
|
// Inputs
|
|
C <- llvm_fresh_var "C" C_type;
|
|
T <- llvm_fresh_var "T" T_type;
|
|
|
|
CT_ptr <- llvm_alloc_readonly CT_type;
|
|
llvm_points_to CT_ptr (llvm_term {{ C # T }});
|
|
|
|
(A, A_ptr) <- fresh_alloc_readonly "A" A_type;
|
|
(N, N_ptr) <- fresh_alloc_readonly "N" N_type;
|
|
(K, K_ptr) <- fresh_alloc_readonly "K" K_type;
|
|
|
|
// Outputs
|
|
P_ptr <- llvm_alloc P_type;
|
|
PLEN_ptr <- llvm_alloc i64;
|
|
|
|
llvm_execute_func
|
|
[ P_ptr, PLEN_ptr
|
|
, llvm_null
|
|
, CT_ptr, llvm_term {{ `CT_len:[64] }}
|
|
, A_ptr, llvm_term {{ `A_len:[64] }}
|
|
, N_ptr
|
|
, K_ptr
|
|
];
|
|
|
|
// Compute the expected plaintext and tag
|
|
let PT = {{ AEAD128_decrypt_raw (wordsToBits K) (wordsToBits N) (wordsToBits A) (wordsToBits C) }};
|
|
|
|
// Update the plaintext length
|
|
llvm_points_to PLEN_ptr (llvm_term {{ `P_len : [64] }});
|
|
|
|
if eval_bool {{ `P_len > (0 : Integer) }}
|
|
then llvm_points_to P_ptr (llvm_term {{ bitsToWords PT.0 : [P_len][8] }})
|
|
else return (); // Reading a 0-length array out of uninitialized memory doesn't work (and isn't needed)
|
|
|
|
// Returns 0 on success, -1 on error
|
|
llvm_return (llvm_term {{ if bitsToWords PT.1 == T then 0 else ~0 : [32] }});
|
|
}
|
|
(unint_yices ["Ascon::Ascon_p"]);
|
|
};
|
|
|
|
// Additional Data incorporation is independent of
|
|
// plain/cipher text processing. Check multiple sizes
|
|
// of AD first and then check multiple sizes of P/C
|
|
|
|
for [0,1,10,16,100] (\A_len ->
|
|
for [1] (\P_len -> do {
|
|
verify_encrypt A_len P_len;
|
|
verify_decrypt A_len P_len;
|
|
})
|
|
);
|
|
|
|
for [0,1] (\A_len ->
|
|
for [0,1,2,10,15,16,17,100] (\P_len -> do {
|
|
verify_encrypt A_len P_len;
|
|
verify_decrypt A_len P_len;
|
|
})
|
|
);
|