https://github.com/EasyCrypt/easycrypt
Tip revision: 863066bded664a5e2aba7f89c4fb7bc2afd0e28d authored by Pierre-Yves Strub on 23 September 2015, 08:28:02 UTC
Ring axioms of the `ring`/`field` tactics agree with the ones of `Ring.ec`
Ring axioms of the `ring`/`field` tactics agree with the ones of `Ring.ec`
Tip revision: 863066b
FunctionalSpec.ec
require import Fun Pred Option Int NewList ABitstring Distr.
require (*--*) AWord MAC_then_Pad_then_CBC.
(** A type for octets and its structure **)
type octet.
(** WARNING: This clone implicitly assumes:
- octet is finite,
- |octet| = 2^8,
- a bijection (to_int,from_int) between octet and [0..2^8 - 1],
- a bijection (to_bits,from_bits) between octet and {x \in {0,1}^* | |x| = 8},
- the uniform distribution Octet.Dword.dword on octet.
We should eventually replace it with an axiom-free version of the same. **)
clone import AWord as Octet with
type word <- octet,
op length <- 8
proof leq0_length by smt.
(** A type for blocks and its structure **)
type block.
(** WARNING: This clone implicitly assumes:
- block is finite,
- |block| = 2^128,
- a bijection (to_int,from_int) between block and [0..2^128 - 1],
- a bijection (to_bits,from_bits) between block and {x \in {0,1}^* | |x| = 128},
- the uniform distribution Block.Dword.dword on block.
We should eventually replace it with an axiom-free version of the same. **)
clone import AWord as Block with
type word <- block,
op length <- 128
proof leq0_length by smt.
lemma d_block_uffu: is_uniform_over Block.Dword.dword predT.
proof. by do !split; smt. qed.
(** A type for tags and its structure **)
type tag.
(** WARNING: This clone implicitly assumes:
- tag is finite,
- |tag| = 2^256,
- a bijection (to_int,from_int) between tag and [0..2^256 - 1],
- a bijection (to_bits,from_bits) between tag and {x \in {0,1}^* | |x| = 256}.
We should eventually replace it with an axiom-free version of the same. **)
clone import AWord as Tag with
type word <- tag,
op length <- 256
proof leq0_length by smt.
(** Conversions **)
(* octet list <-> bitstring *)
(* WARNING: This is a (underspecified) fixpoint on nat, which we currently need to axiomatize *)
op bits2os (bs : bitstring): octet list.
axiom bits2os0 (bs : bitstring):
`|bs| = 0 =>
bits2os bs = [].
axiom bits2osS (bs : bitstring):
0 < `|bs| =>
`|bs| %% 8 = 0 =>
bits2os bs = (Octet.from_bits (sub bs 0 8)) :: bits2os (sub bs 8 (`|bs| - 8)).
lemma size_bits2os (bs : bitstring):
`|bs| %% 8 = 0 =>
size (bits2os bs) = `|bs| /% 8.
proof.
move: {-1}(`|bs| /% 8) (eq_refl (`|bs| /% 8))=> n len_bs.
have le0_n: 0 <= n by smt.
elim/Induction.induction n le0_n bs len_bs=> [bs bs_is_octets bs_is_empty
|n le0_n ih bs bs_is_nonempty bs_is_octets].
by rewrite bits2os0 1:smt.
rewrite bits2osS 1:smt //=.
have h_len:= length_sub bs 8 (`|bs| - 8) _ _ _ => //=; 1,2:smt.
rewrite ih 3:addzC// h_len 1,2:smt.
qed.
op os2bits (os : octet list) =
foldr (fun o bs => (Octet.to_bits o) || bs) (zeros 0) os.
lemma length_os2bits (os : octet list):
`|os2bits os| = 8 * size os.
proof.
elim os=> //= [|o os ih].
by rewrite /os2bits /= length_zeros.
by rewrite /os2bits /= length_app length_to_bits ih smt.
qed.
lemma bits2osK (os : octet list):
bits2os (os2bits os) = os.
proof.
elim os=> //= [|o os ih]; 1:smt.
have /= := length_os2bits (o :: os).
rewrite /os2bits /= -/(os2bits _)=> h_len. (* FIXME *)
rewrite bits2osS /=.
by rewrite h_len smt.
by rewrite h_len -(add0z (8 * (1 + size os))) addzC Mod_mult 2:Mod_0 smt.
rewrite -(Octet.length_to_bits o); split.
by rewrite sub_app_fst Octet.can_from_to.
rewrite h_len {2}Octet.length_to_bits Mul_distr_l //=.
rewrite addzC StdOrder.IntOrder.Domain.subrE -addzA Ring.IntID.addrN addzC add0z.
by rewrite -length_os2bits sub_app_snd.
qed.
lemma os2bitsK (bs : bitstring):
`|bs| %% 8 = 0 =>
os2bits (bits2os bs) = bs.
proof.
move: {-1}(`|bs| /% 8) (eq_refl (`|bs| /% 8))=> n len_bs.
have le0_n: 0 <= n by smt.
elim/Induction.induction n le0_n bs len_bs=> [|n le0_n ih bs len_bs good_length].
smt.
have h_len: `|sub bs 8 (`|bs| - 8)| = `|bs| - 8.
by rewrite length_sub // 1,2:smt.
rewrite bits2osS //= 1:smt /os2bits /= -/(os2bits _) ih 1,2:h_len 1,2:smt.
by rewrite Octet.pcan_to_from 1:smt app_sub //= smt.
qed.
(* block list <-> bitstring *)
(* WARNING: This is a (underspecified) fixpoint on nat - which we currently need to axiomatize *)
op bits2bs (bs : bitstring): block list.
axiom bits2bs0 (bs : bitstring):
`|bs| = 0 =>
bits2bs bs = [].
axiom bits2bsS (bs : bitstring):
0 < `|bs| =>
`|bs| %% 128 = 0 =>
bits2bs bs = (Block.from_bits (sub bs 0 128)) :: bits2bs (sub bs 128 (`|bs| - 128)).
lemma size_bits2bs (bs : bitstring):
`|bs| %% 128 = 0 =>
size (bits2bs bs) = `|bs| /% 128.
proof.
move: {-1}(`|bs| /% 128) (eq_refl (`|bs| /% 128))=> n len_bs.
have le0_n: 0 <= n by smt.
elim/Induction.induction n le0_n bs len_bs=> [bs bs_is_octets bs_is_empty
|n le0_n ih bs bs_is_nonempty bs_is_octets].
by rewrite bits2bs0 1:smt.
rewrite bits2bsS 1:smt //=.
have h_len:= length_sub bs 128 (`|bs| - 128) _ _ _ => //=; 1,2:smt.
rewrite ih 3:addzC// h_len 1,2:smt.
qed.
op bs2bits (os : block list) =
foldr (fun o bs => (Block.to_bits o) || bs) (zeros 0) os.
lemma length_bs2bits (bs : block list):
`|bs2bits bs| = 128 * size bs.
proof.
elim bs=> //= [|b bs ih].
by rewrite /bs2bits /= length_zeros.
by rewrite /bs2bits /= length_app length_to_bits ih smt.
qed.
lemma bits2bsK (bs : block list):
bits2bs (bs2bits bs) = bs.
proof.
elim bs=> //= [|b bs ih]; 1:smt.
have /= := length_bs2bits (b :: bs).
rewrite /bs2bits /= -/(bs2bits _)=> h_len. (* FIXME *)
rewrite bits2bsS /=.
by rewrite h_len smt.
by rewrite h_len -(add0z (128 * (1 + size bs))) addzC Mod_mult 2:Mod_0 smt.
rewrite -(Block.length_to_bits b); split.
by rewrite sub_app_fst Block.can_from_to.
rewrite h_len {2}Block.length_to_bits Mul_distr_l //=.
rewrite addzC StdOrder.IntOrder.Domain.subrE -addzA Ring.IntID.addrN addzC add0z.
by rewrite -length_bs2bits sub_app_snd.
qed.
lemma bs2bitsK (bs : bitstring):
`|bs| %% 128 = 0 =>
bs2bits (bits2bs bs) = bs.
proof.
move: {-1}(`|bs| /% 128) (eq_refl (`|bs| /% 128))=> n len_bs.
have le0_n: 0 <= n by smt.
elim/Induction.induction n le0_n bs len_bs=> [|n le0_n ih bs len_bs good_length].
smt.
have h_len: `|sub bs 128 (`|bs| - 128)| = `|bs| - 128.
by rewrite length_sub // 1,2:smt.
rewrite bits2bsS //= 1:smt /bs2bits /= -/(bs2bits _) ih 1,2:h_len 1,2:smt.
by rewrite Block.pcan_to_from 1:smt app_sub //= smt.
qed.
(* block list <-> octet list *)
op bs2os bs = bits2os (bs2bits bs).
lemma size_bs2os bs: size (bs2os bs) = 16 * size bs.
proof.
rewrite /bs2os size_bits2os length_bs2bits;
have ->: 128 * size bs = 8 * (16 * size bs) + 0 by smt.
by rewrite Mod_mult smt.
rewrite Div_mult 1:smt -{2}(add0z (16 * size bs)) addzC.
by congr; smt.
qed.
op os2bs os = bits2bs (os2bits os).
lemma size_os2bs os:
size os %% 16 = 0 =>
size (os2bs os) = size os /% 16.
proof.
move=> bs_is_blocks.
rewrite /os2bs size_bits2bs length_os2bits (Div_mod (size os) 16) 1,3:smt bs_is_blocks;
have ->: 8 * (16 * (size os /% 16) + 0) = 128 * (size os /% 16) + 0 by smt.
by rewrite Mod_mult smt.
rewrite !Div_mult 1,2:smt.
by congr; smt.
qed.
lemma os2bsK bs: os2bs (bs2os bs) = bs.
proof.
rewrite /os2bs /bs2os.
rewrite os2bitsK.
rewrite length_bs2bits.
have ->: 128 * size bs %% 8 = (8 * (16 * size bs) + 0) %% 8 by smt.
by rewrite Mod_mult smt.
by rewrite bits2bsK.
qed.
lemma bs2osK os:
size os %% 16 = 0 =>
bs2os (os2bs os) = os.
proof.
move=> bs_is_blocks.
rewrite /os2bs /bs2os.
rewrite bs2bitsK.
rewrite length_os2bits (Div_mod (size os) 16) 1:smt bs_is_blocks.
have ->: 8 * (16 * (size os /% 16) + 0) = 128 * (size os /% 16) + 0 by smt.
by rewrite Mod_mult smt.
by rewrite bits2osK.
qed.
(* tag <-> octet list *)
op t2os t = bits2os (Tag.to_bits t).
lemma size_t2os t: size (t2os t) = 32.
proof. by rewrite /t2os size_bits2os length_to_bits smt. qed.
op os2t os = Tag.from_bits (os2bits os).
lemma os2tK t: os2t (t2os t) = t.
proof. by rewrite /os2t /t2os os2bitsK 1:length_to_bits 1:smt Tag.can_from_to. qed.
lemma t2osK os:
size os = 32 =>
t2os (os2t os) = os.
proof.
move=> bs_is_tag.
rewrite /os2t /t2os Tag.pcan_to_from 1:length_os2bits 1:bs_is_tag 1:smt.
by rewrite bits2osK.
qed.
(* tag <-> block list *)
op t2bs t = os2bs (t2os t).
lemma size_t2bs t: size (t2bs t) = 2.
proof. rewrite /t2bs size_os2bs size_t2os smt. qed.
op bs2t bs = os2t (bs2os bs).
lemma bs2tK t: bs2t (t2bs t) = t.
proof. by rewrite /bs2t /t2bs bs2osK 2:os2tK// size_t2os smt. qed.
lemma t2bsK bs:
size bs = 2 =>
t2bs (bs2t bs) = bs.
proof.
move=> bs_is_tag.
by rewrite /bs2t /t2bs t2osK 2:os2bsK// size_bs2os bs_is_tag smt.
qed.
type msg = octet list.
(* -------------------------------------------------------------------- *)
(** Functional spec for CBC encryption and decryption with explicit IV **)
(* Definition *)
op cbc_enc (P : block -> block -> block) (k:block) (st:block) p =
with p = [] => []
with p = pi :: p => let ci = P k (st ^ pi) in ci::(cbc_enc P k ci p).
op cbc_dec (Pi : block -> block -> block) (k:block) (st:block) c =
with c = [] => []
with c = ci :: c => let pi = Pi k ci in (pi ^ st)::(cbc_dec Pi k ci c).
(* Alternative fold-based definition... Probably a lot more useful for
program verification *)
op cbc_enc_block (P : block -> block -> block) k (stc:block * block list) pi =
let (st,c) = stc in
let ci = P k (st ^ pi) in
(ci,rcons c ci).
op cbc_enc_fold P (k iv:block) p =
(foldl (cbc_enc_block P k) (iv,[]) p).`2.
lemma cbc_enc_cbc_fold P k iv p:
cbc_enc P k iv p = cbc_enc_fold P k iv p.
proof.
rewrite /cbc_enc_fold /= -(cat0s (cbc_enc P k iv p)).
elim p iv []=> //= [iv acc|pi p ih iv acc].
by rewrite cats0.
by rewrite -cat_rcons ih.
qed.
op cbc_dec_block (Pi : block -> block -> block) k (stp:block * block list) ci =
let (st,p) = stp in
let pi = Pi k ci in
(ci,rcons p (pi ^ st)).
op cbc_dec_fold Pi (k iv:block) c =
(foldl (cbc_dec_block Pi k) (iv,[]) c).`2.
lemma cbc_dec_cbc_fold Pi k iv c:
cbc_dec Pi k iv c = cbc_dec_fold Pi k iv c.
proof.
rewrite /cbc_dec_fold /= -(cat0s (cbc_dec Pi k iv c)).
elim c iv []=> //= [iv acc|ci c ih iv acc].
by rewrite cats0.
by rewrite -cat_rcons ih.
qed.
(* Correctness *)
lemma cbc_correct P Pi k st p:
cancel (P k) (Pi k) =>
cbc_dec Pi k st (cbc_enc P k st p) = p.
proof.
move=> PiK; elim p st=> //= pi p ih st.
split; 2:by apply/ih.
by rewrite PiK; smt.
qed.
(* Useful lemmas *)
lemma cbc_enc_rcons (P : block -> block -> block) k st (p:block list) pn:
rcons (cbc_enc P k st p) (P k (nth witness (st :: cbc_enc P k st p) (size p) ^ pn))
= cbc_enc P k st (rcons p pn).
proof.
elim p st=> //=.
move=> pi p ih st.
have -> /=: 1 + size p <> 0 by smt.
have ->: 1 + size p - 1 = size p by smt.
by rewrite -ih.
qed.
lemma cbc_dec_rcons (Pi : block -> block -> block) k st (c:block list) cn:
rcons (cbc_dec Pi k st c) ((Pi k cn) ^ (if 0 < size c then nth witness c (size c - 1) else st))
= cbc_dec Pi k st (rcons c cn).
proof.
elim c st=> //=.
move=> ci c ih st //=.
have -> /=: 0 < 1 + size c by smt.
have ->: 1 + size c - 1 = size c by smt.
by rewrite -ih; smt.
qed.
lemma size_cbc_enc P k iv p: size (cbc_enc P k iv p) = size p.
proof. by elim p iv=> //= p0 p ih iv; rewrite ih. qed.
(* -------------------------------------------------------------------- *)
(** Functional spec for padding a (msg * tag) pair into a block list **)
(* Definition. TODO: Once we've moved to layered lists, things should
be easier on the modular arithmetic side... *)
(** TODO: Clean up this entire section, whether or not we've moved
to better libraries **)
op pad_length (m : msg) = 16 - size m %% 16.
op padding (l : int) =
mkseq (fun i => (Octet.from_int l)) l.
op pad (m : msg) (t : tag) =
let p = padding (pad_length m) in
os2bs (m ++ t2os t ++ p).
op unpad (bs : block list) =
let os = bs2os bs in
let l = Octet.to_int (last witness os) in
let m = take (size os - l - 32) os in
let t = os2t (take 32 (drop (size os - l - 32) os)) in
let p = drop (size os - l) os in
if (1 <= l <= 16 /\ p = padding l)
then Some (m,t)
else None.
(* Proofs for instantiation *)
lemma (* TODO: move *) mod_sub_mod x y: 0 < y => (x - x %% y) %% y = 0.
proof.
move=> lt0_y; rewrite {1}(Div_mod x y) 1:smt Ring.IntID.subrE -addzA Ring.IntID.addrN.
by rewrite Mod_mult smt.
qed.
lemma size_padding m: size (padding (pad_length m)) = 16 - size m %% 16.
proof. by rewrite /padding /= size_mkseq smt. qed.
lemma last_padding x m: last x (padding (pad_length m)) = Octet.from_int (16 - size m %% 16).
proof.
rewrite /padding /mkseq /= -(lastnonempty ((fun x => Octet.from_int (16 - size m %% 16)) witness<:int>)).
case {-1}(iota_ 0 (16 - size m %% 16)) (eq_refl (iota_ 0 (16 - size m %% 16)))=> //=.
by have:= size_iota 0 (16 - size m %% 16); smt.
by rewrite last_map.
qed.
lemma size_padded m t:
size (m ++ t2os t ++ padding (pad_length m))
= 48 + (size m - size m %% 16).
proof. by rewrite !size_cat size_padding size_t2os smt. qed.
lemma padded_is_blocks m t:
size (m ++ t2os t ++ padding (pad_length m)) %% 16 = 0.
proof.
rewrite size_padded.
have ->: 48 = 16 * 3 by smt.
by rewrite Mod_mult 1:smt mod_sub_mod//.
qed.
lemma size_pad m t:
size (pad m t) (* this is in blocks of 16 octets *)
= size m /% 16 (* message *) + 2 (* tag *) + 1 (* padding *).
proof.
rewrite /pad /= size_os2bs 1:padded_is_blocks// size_padded.
have ->: (48 + (size m - size m %% 16)) /% 16
= (16 * 3 + (size m - size m %% 16)) /% 16 by smt.
rewrite Div_mult 1:smt {1}(Div_mod (size m) 16) 1:smt Ring.IntID.subrE -addzA Ring.IntID.addrN.
rewrite Div_mult 1:smt addzC -!addzA /= -{2}(add0z 3).
by congr; congr; smt.
qed.
lemma unpad_pad m t:
unpad (pad m t) = Some (m,t).
proof.
rewrite /unpad.
have -> /=: bs2os (pad m t)
= m ++ t2os t ++ padding (pad_length m).
by rewrite /pad /= bs2osK 1:padded_is_blocks.
rewrite !lastcat last_padding Octet.from_to.
rewrite (powS 7 2)// (powS 6 2)// (powS 5 2)// (powS 4 2)//
(powS 3 2)// (powS 2 2)// (powS 1 2)// (powS 0 2)//
(pow0 2) /=.
have h: 0 < 16 - size m %% 16 <= 16 < 256 by smt.
have ->: (16 - size m %% 16) %% 256 = 16 - size m %% 16 by smt.
rewrite drop_size_cat.
by rewrite !size_cat size_padding smt.
rewrite {1}/pad_length /=.
rewrite -catA take_size_cat //=.
rewrite !size_cat size_padding 1:smt.
rewrite drop_size_cat.
rewrite !size_cat size_padding 1:smt.
rewrite (_: 1 <= 16 - size m %% 16 <= 16) 1:smt /=.
by rewrite take_size_cat 1:size_t2os// os2tK.
qed.
lemma leak_pad m t:
size (pad m t)
= size (pad (mkseq (fun (i : int) => Octet.zeros) (size m - size m %% 16)) t).
proof.
rewrite /pad /=.
do 2!rewrite size_os2bs 1:padded_is_blocks//.
rewrite !size_cat !size_padding !size_mkseq.
have ->: max 0 (size m - size m %% 16) = (size m - size m %% 16) by smt.
congr; ringeq.
exact/mod_sub_mod.
qed.
(* -------------------------------------------------------------------- *)
(** Functional spec for MAC-then-Pad-then-Encrypt **)
(* We parameterize it with a (stateless deterministic) PRP (called AES) *)
theory AES.
op AES : block -> block -> block.
op AESi: block -> block -> block.
axiom AES_correct (k : block):
cancel (AES k) (AESi k)
/\ cancel (AESi k) (AES k).
end AES.
import AES.
(* and a (stateless, deterministic) MAC (called HMAC_SHA256) *)
theory HMAC_SHA256.
type mK.
op d_mK: mK distr.
axiom d_mK_uffu: is_uniform_over d_mK Pred.predT.
op hmac_sha256: mK -> msg -> tag.
end HMAC_SHA256.
import HMAC_SHA256.
(* Definition. *)
op mee_enc (P : block -> block -> block) (M : mK -> msg -> tag)
(ek : block) (mk : mK) (iv : block) (m : msg) =
let t = M mk m in
let p = pad m t in
cbc_enc P ek iv p.
op mee_dec (Pi : block -> block -> block) (M : mK -> msg -> tag)
(ek : block) (mk : mK) (iv : block) (c : block list) =
let p = cbc_dec Pi ek iv c in
let mt = unpad p in
if (mt <> None)
then let (m,t) = oget mt in
if M mk m = t
then Some m
else None
else None.
lemma mee_correct P Pi M ek mk iv m:
cancel (P ek) (Pi ek) =>
mee_dec Pi M ek mk iv (mee_enc P M ek mk iv m) = Some m.
proof.
rewrite /mee_dec /mee_enc /= => /cbc_correct ->.
by rewrite unpad_pad.
qed.
(* -------------------------------------------------------------------- *)
(** Final Instantiation: mee_enc and mee_dec are IND$-CPA and INT-PTXT **)
op q: {int | 0 < q } as lt0_q.
op n: {int | 0 <= n } as le0_n.
clone import MAC_then_Pad_then_CBC as MEEt with
(* PRP parameters and operations on the relevant types *)
type eK <- block,
type block <- block,
op d_eK <- Block.Dword.dword,
op d_block <- Block.Dword.dword,
op P <- AES,
op Pinv <- AESi,
op zeros <- Block.zeros,
op (+) <- Block.(^),
(* MAC parameters *)
type mK <- mK,
type msg <- msg,
type tag <- tag,
op d_mK <- d_mK,
op mac <- hmac_sha256,
(* pad parameters *)
op pad (mt : msg * tag) <- pad mt.`1 mt.`2,
op unpad <- unpad,
op leak (m : msg) <- mkseq (fun i => Octet.zeros) (size m - size m %% 16),
op valid_msg (m : msg) <- size m /% 16 < n,
(* security parameters *)
op q <- q,
op n <- n + 3
proof * by smt.
(* -------------------------------------------------------------------- *)
(** We show that the pWhile programs on which we do the security proof
fully and faithfully implement the operators used as functional
specs for the C code... **)
import Dapply.
phoare mee_encrypt_correct _mk _ek _p _c:
[MEEt.MEE(MEEt.PRPa.PRPr,MEEt.MAC).enc: key = (_ek,_mk) /\ p = _p
==> res = _c]
=(mu (dapply (fun iv => iv :: mee_enc AES hmac_sha256 _ek _mk iv _p) Top.Block.Dword.dword) (pred1 _c)).
proof.
rewrite -/(mu_x _ _) Dapply.mu_x_def /preim /pred1 /=.
proc; inline MAC.tag PRPa.PRPr.f.
swap 6 -5 => //=; alias 2 iv = s.
while ( 0 <= i <= size (pad _p (hmac_sha256 _mk _p))
/\ ek = _ek
/\ p' = pad _p (hmac_sha256 _mk _p)
/\ s = nth witness c i
/\ size c = i + 1
/\ c = iv :: cbc_enc AES _ek iv (take i (pad _p (hmac_sha256 _mk _p))))
(size (pad _p (hmac_sha256 _mk _p)) - i).
by auto; smt.
wp=> //=.
conseq (_: _ ==> s :: mee_enc AES hmac_sha256 _ek _mk s _p = _c)=> //=.
move=> &m [->>] ->> iv //=; split=> [[[le0_size _] h]|<<-].
have -> //=:= h (iv :: mee_enc AES hmac_sha256 _ek _mk iv _p)
(nth witness (iv :: mee_enc AES hmac_sha256 _ek _mk iv _p)
(size (pad _p (hmac_sha256 _mk _p))))
(size (pad _p (hmac_sha256 _mk _p))).
split=> //=.
split; 1:by rewrite /mee_enc /= size_cbc_enc addzC.
by rewrite take_size.
split=> [|c s0 n]; 1:by split; [rewrite size_ge0|rewrite take0].
split=> [[[le0_n le_n_size] [s0_is_nth [size_c]]] c_is_enc|].
by rewrite StdOrder.IntOrder.ler_subl_addr add0z=> /StdOrder.IntOrder.ler_gtF.
rewrite -lezNgt=> le_size_n [[le0_n le_n_size]] [_] [_] ->.
have [_ ->] //:= eqz_leq n (size (pad _p (hmac_sha256 _mk _p))).
by rewrite take_size.
by rnd.
qed.
phoare mee_decrypt_correct _mk _ek _c:
[MEEt.MEE(MEEt.PRPa.PRPr,MEEt.MAC).dec: key = (_ek,_mk) /\ c = _c
==> res = mee_dec AESi hmac_sha256 _ek _mk (head witness _c) (behead _c)]
=1%r.
proof.
conseq (_: true ==> true) (_: _ ==> _)=> //=.
proc; inline MAC.verify PRPa.PRPr.finv; wp.
while ( 0 <= i <= size c
/\ ek = _ek
/\ s = (if 0 < i then nth witness c (i - 1) else head witness _c)
/\ size padded = i
/\ padded = cbc_dec AESi _ek (head witness _c) (take i c)).
auto; progress; 1..4:smt.
by rewrite (take_nth witness)// -cbc_dec_rcons cats1 -H1 smt.
by auto; smt.
by proc; inline *; wp; while true (size c - i); auto; smt.
qed.