Skip to content

[cryptolib] generalize PRF definitions, PRP<->PRF #1028

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
fdupress wants to merge 1 commit into
base: main
Choose a base branch
from
+1,709 −1,837
Draft

[cryptolib] generalize PRF definitions, PRP<->PRF #1028

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
628 changes: 269 additions & 359 deletions examples/MEE-CBC/CBC.eca
View file
Open in desktop

Large diffs are not rendered by default.

97 changes: 53 additions & 44 deletions examples/MEE-CBC/FunctionalSpec.ec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -458,65 +458,75 @@ realize max_pad_n by move=> m t szm /=; rewrite size_pad -addrA ltr_add2r.
(** 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... **)
module PRP_AES = {
proc keygen() = {
var k;
k <$ dblock;
return k;
}

proc p(k, x) = { return AES k x; }
proc pi(k, x) = { return AESi k x; }
}.

phoare mee_encrypt_correct _mk _ek _p _c:
[MEEt.MEE(MEEt.PRPc.PseudoRP,MEEt.MAC).enc: key = (_ek,_mk) /\ p = _p
[MEEt.MEE(PRP_AES,MEEt.MAC).enc: key = (_ek,_mk) /\ p = _p
==> res = _c]
=(mu (dapply (fun iv => iv :: mee_enc AES hmac_sha256 _ek _mk iv _p) dblock) (pred1 _c)).
proof.
have->: mu1 (dapply (fun iv=> iv :: mee_enc AES hmac_sha256 _ek _mk iv _p) dblock) _c
= mu1 (dmap dblock (fun iv=> iv :: mee_enc AES hmac_sha256 _ek _mk iv _p)) _c by move.
rewrite dmap1E /pred1 /=.
proc; inline MAC.tag PRPc.PseudoRP.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 = 1 + i
/\ c = iv :: cbc_enc AES _ek iv (take i (pad _p (hmac_sha256 _mk _p))))
(size (pad _p (hmac_sha256 _mk _p)) - i).
auto=> /> &hr le0_i _ /addzI szcbc_eq_i lti_szpadded.
split; last by smt ().
split; first by smt().
split; last first.
split; first by rewrite size_cat /= szcbc_eq_i.
rewrite (take_nth witness) //= -cbc_enc_rcons -cats1 /=.
by rewrite size_take // lti_szpadded.
have -> /=: i{hr} + 1 <> 0 by smt ().
by rewrite cats1 nth_rcons size_cbc_enc size_take // lti_szpadded /=.
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)
(size (pad _p (hmac_sha256 _mk _p)))
(nth witness (iv :: mee_enc AES hmac_sha256 _ek _mk iv _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 n s0]; 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))).
have->: mu1 (dapply (fun iv=> iv :: mee_enc AES hmac_sha256 _ek _mk iv _p) dblock) _c
= mu1 (dmap dblock (fun iv=> iv :: mee_enc AES hmac_sha256 _ek _mk iv _p)) _c by move.
rewrite dmap1E /pred1 /=.
proc; inline MAC.tag PRP_AES.p.
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 = 1 + i
/\ c = iv :: cbc_enc AES _ek iv (take i (pad _p (hmac_sha256 _mk _p))))
(size (pad _p (hmac_sha256 _mk _p)) - i).
- auto=> /> &0 le0_i _ /addzI szcbc_eq_i lti_szpadded.
split; last by smt ().
split; first by smt().
split; last first.
+ split; first by rewrite size_cat /= szcbc_eq_i.
rewrite (take_nth witness) //= -cbc_enc_rcons -cats1 /=.
by rewrite size_take // lti_szpadded.
have -> /=: i{0} + 1 <> 0 by smt ().
by rewrite cats1 nth_rcons size_cbc_enc size_take // lti_szpadded /=.
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)
(size (pad _p (hmac_sha256 _mk _p)))
(nth witness (iv :: mee_enc AES hmac_sha256 _ek _mk iv _p)
(size (pad _p (hmac_sha256 _mk _p)))).
split=> //=.
split; 1:by rewrite /mee_enc /= size_cbc_enc addzC.
by rewrite take_size.
by rnd.
split=> [|c n s0]; 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.PRPc.PseudoRP,MEEt.MAC).dec: key = (_ek,_mk) /\ c = _c
[MEEt.MEE(PRP_AES,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 PRPc.PseudoRP.fi; wp.
+ proc; inline MAC.verify PRP_AES.pi; 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=> /> &hr le0_szpadded _ h lt_padded_c.
+ auto=> /> &0 le0_szpadded _ h lt_padded_c.
split; first by smt ().
split; first by smt (size_ge0).
split; first by rewrite size_cat.
Expand All @@ -525,11 +535,10 @@ conseq (_: true ==> true) (_: _ ==> _)=> //=.
auto=> />; split.
+ by rewrite size_ge0 take0.
move=> p /lezNgt le_szc_p _ ge_szc_p.
rewrite (ler_asym (size p) (size (behead _c)) _);
rewrite ?ge_szc_p ?le_szc_p // take_size => p_def.
rewrite (ler_asym (size p) (size (behead _c)) _) ?ge_szc_p ?le_szc_p // take_size => p_def.
split.
+ case: {-1}(unpad p) (eq_refl (unpad p))=> //= - [] m t.
by rewrite /mee_dec /= -p_def=> -> /=.
by rewrite /mee_dec -p_def /= => ->.
proc; inline *; wp; while true (size c - i); auto =>/#.
by proc; inline *; wp; while true (size c - i); auto =>/#.
qed.
Loading
Loading