swh:1:snp:1160b607213f14ec0f922dad3284705c8e588b30
Tip revision: 4391b04a9637c10d48185c11e42d8c7b01f83781 authored by Pierre-Yves Strub on 12 November 2020, 11:00:16 UTC
basic results about minr
basic results about minr
Tip revision: 4391b04
MAC_then_Pad_then_CBC.eca
require import AllCore Int Real List Distr.
require import DList.
require (*..*) PRP MACs RCPA_CMA CBC RCPA_pad.
(** Assume a permutation (P,Pinv) on block indexed by eK **)
type eK, block.
op d_eK: eK distr.
axiom d_eK_uffu: is_lossless d_eK /\ is_funiform d_eK.
op d_block: block distr.
axiom d_block_uffu: is_lossless d_block /\ is_funiform d_block.
op P : eK -> block -> block.
op Pi: eK -> block -> block.
axiom bijectiveP k:
support d_eK k
=> cancel (P k) (Pi k)
/\ cancel (Pi k) (P k).
(* Import definitions to consider (P,Pinv) as a weak PRP *)
clone import PRP as PRPt with
type D <- block.
clone import WeakPRP as PRPSec.
clone import PseudoRP as PRPc with
type K <- eK,
op dK <- d_eK,
op p <- P,
op pi <- Pi
proof * by smt (d_eK_uffu bijectiveP).
clone import RP as PRPi with
op dD <- d_block
rename "RP" as "PRPi"
proof * by smt (d_block_uffu).
(** Assume a zmodule structure on block (for generality... we will instantiate it with {0,1}^k later on) *)
op zeros: block.
op (+): block -> block -> block.
axiom add0b (x : block) : zeros + x = x.
axiom addbA (y x z : block): x + (y + z) = (x + y) + z.
axiom addbC (x y : block) : x + y = y + x.
axiom addbK (x : block) : x + x = zeros.
clone Ring.ZModule as Block with
type t <- block,
op zeror <- zeros,
op (+) <- (+),
op [-] (x : block) <- x
proof * by smt (add0b addbA addbC addbK).
(** Assume a (deterministic) MAC (mac,verify) with key in mK, message in msg and tag in tag **)
type mK, msg, tag.
op d_mK: mK distr.
axiom d_mK_uffu: is_lossless d_mK /\ is_funiform d_mK.
op mac: mK -> msg -> tag.
(* Import definitions to consider (mac,(fun k x t => mac k x = t)) a WUF-CMA MAC *)
clone import MACs as MACa with
type mK <- mK,
type msg <- msg,
type tag <- tag
proof * by smt ().
import WUF_CMA.
module MAC: MAC_Scheme = {
proc keygen(): mK = {
var k;
k <$ d_mK;
return k;
}
proc tag(k:mK,m:msg): tag = {
return mac k m;
}
proc verify(k:mK,m:msg,t:tag): bool = {
return mac k m = t;
}
}.
(** Assume a well-formed padding function from msg to block list **)
(* morally, if "ptxt = octetstrings" and "block = fixed length octetstrings", "pad = extend and chunk" *)
op pad : msg * tag -> block list.
op unpad: block list -> (msg * tag) option.
axiom can_unpad mt: unpad (pad mt) = Some mt.
axiom pad_tag m t0 t1: size (pad (m,t0)) = size (pad (m,t1)).
op leak: msg -> msg.
axiom leak_pad m t: size (pad (m,t)) = size (pad ((leak m),t)).
(** And construct MAC-then-Encode-then-Encrypt as a SKE scheme **)
op q: { int | 0 < q } as gt0_q. (* Number of queries to the lr oracle *)
op n: { int | 1 < n } as gt1_n. (* Max length of queries to the lr oracle (in blocks) *)
op valid_msg: msg -> bool.
axiom max_pad_n m t: valid_msg m => size (pad (m,t)) < n.
(* Import definitions to allow early type-checking *)
clone import SKE_INDR as SKEa with
type eK <- (eK * mK),
type ptxt <- msg,
type ctxt <- block list,
type leaks <- int,
op leak (m : msg) <- size (pad (m,witness<:tag>)),
op dC (l : int) <- dlist d_block (l + 1)
proof * by smt (dlist_ll d_block_uffu).
import RCPA PTXT.
module MEE (P:PseudoRP) (M:MAC_Scheme): Enc_Scheme = {
proc keygen(): eK * mK = {
var ek, mk;
ek <@ P.keygen();
mk <@ M.keygen();
return (ek,mk);
}
proc enc(key:eK * mK,p:msg): block list = {
var ek, mk;
var t, p', s, i, pi, c;
(ek,mk) <- key;
(* compute tag *)
t <@ M.tag(mk,p);
(* pad (produce block list from plain and tag) *)
p' <- pad (p,t);
(* compute CBC$ encryption *)
s <$ d_block;
c <- [s];
i <- 0;
while (i < size p') {
pi <- nth witness p' i;
s <@ P.f(ek,s + pi);
c <- c ++ [s];
i <- i + 1;
}
return c;
}
proc dec(key:eK * mK,c:block list): msg option = {
var ek, mk;
var t, s, i, ci, pi, padded, pt, p', b;
var p <- None;
(ek,mk) <- key;
(* compute CBC decryption (first block is iv) *)
s <- head witness c;
c <- behead c;
padded <- [];
i <- 0;
while (i < size c) {
ci <- nth witness c i;
pi <@ P.fi(ek,ci);
padded <- padded ++ [s + pi];
s <- ci;
i <- i + 1;
}
(* strip padding *)
pt <- unpad padded;
(* check MAC *)
if (pt <> None) {
(p',t) <- oget pt;
b <@ M.verify(mk,p',t);
p <- b ? Some p' : None;
}
return p;
}
}.
module RCPA_QueryBounder (A : RCPA_Adversary, O : RCPA_Oracles) = {
var qC : int
module O' = {
proc enc(p:msg): block list = {
var i;
var c <- witness;
if (qC < q /\ size (pad (p,witness)) <= n) {
c <@ O.enc(p);
qC <- qC + 1;
} else {
c <- [];
i <- 0;
while (i <= size (pad (p,witness))) {
c <- c ++ [witness];
i <- i + 1;
}
}
return c;
}
}
proc distinguish(): bool = {
var b;
qC <- 0;
b <@ A(O').distinguish();
return b;
}
}.
(* From the MAC and a CPA adversary against MtE, we construct an adversary against the PRP *)
module Weak_PRPa (M : MAC_Scheme, A : RCPA_Adversary, P : PRP_Oracles) = {
var qC: int
var mk: mK
module O = {
proc enc(p:msg): block list = {
var i, s, t, padded, pi;
var c <- witness;
if (qC < q /\ size (pad (p,witness)) <= n) {
t <@ M.tag(mk,p);
padded <- pad(p,t);
s <$ d_block;
c <- [s];
i <- 0;
while (i < size padded) {
pi <- nth witness padded i;
s <@ P.f(s + pi);
c <- c ++ [s];
i <- i + 1;
}
qC <- qC + 1;
} else {
c <- [];
i <- 0;
while (i <= size (pad (p,witness))) {
c <- c ++ [witness];
i <- i + 1;
}
}
return c;
}
}
proc distinguish(): bool = {
var b;
qC <- 0;
mk <@ M.keygen();
b <@ A(O).distinguish();
return b;
}
}.
section RCPA.
declare module A : RCPA_Adversary { PRPi, PRP, RCPA_Wrap, RCPA_QueryBounder, Weak_PRPa }.
axiom A_distinguish_ll (O <: RCPA_Oracles { A }):
islossless O.enc => islossless A(O).distinguish.
local clone import CBC as CBCa with
op q <- q,
op ell <- n,
type key <- eK,
op dKey <- d_eK,
type block <- block,
op dBlock <- d_block,
op zeros <- zeros,
op (+) <- (+),
op P <- P,
op Pi <- Pi
proof *.
realize gt0_q by exact/gt0_q.
realize gt0_ell by smt (gt1_n).
realize dKey_uffu by smt(@Distr d_eK_uffu).
realize dBlock_uffu by smt(@Distr d_block_uffu).
realize add0b by exact/add0b.
realize addbA by exact/addbA.
realize addbC by exact/addbC.
realize addbK by exact/addbK.
realize bijective_P. by move=> k; apply/bijectiveP; smt(@Distr d_eK_uffu). qed.
(** We really want to clone only MtE, but since RCPA_CPA is
abstract, its inner theories don't exist until cloned...
Unintended side-effect or intended behaviour? **)
local clone RCPA_CMA as CPA_CMA with
type MtE.mK <- mK,
type MtE.eK <- eK,
type MtE.ptxt <- msg,
type MtE.ctxt <- block list,
type MtE.tag <- tag,
type MtE.leaks <- msg,
op MtE.leak (m : msg) <- leak m,
op MtE.dC (m : msg) <- CBCa.dBlocks (size (pad (m,witness<:tag>)) + 1)
proof MtE.* by smt (dlist_ll d_block_uffu).
import CPA_CMA.MtE.
local clone import RCPA_pad as PtE with
type key <- eK,
type ptxt <- block list,
type ctxt <- block list,
type msg <- msg * tag,
type leaks_m <- msg,
type leaks_p <- int,
op leak_m (mt : msg * tag) <- leak mt.`1,
op leak_p <- size<:block>,
op pad <- pad,
op unpad <- unpad,
op dC_m (m : msg) <- CBCa.dBlocks (size (pad (m,witness<:tag>)) + 1),
op dC_p (l : int) <- CBCa.dBlocks (l + 1)
proof * by smt (dlist_ll d_block_uffu can_unpad leak_pad pad_tag).
local lemma MEE_unfold &m:
Pr[INDR_CPA(MEE(PseudoRP,MAC),RCPA_QueryBounder(A)).main() @ &m: res]
= Pr[INDR_CPA(MacThenEncrypt(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),MAC),RCPA_QueryBounder(A)).main () @ &m: res].
proof.
byequiv (: ={glob A} ==> ={res}); first last.
+ done.
+ done.
proc; inline *.
wp; call (: ={glob RCPA_QueryBounder, glob RCPA_Wrap}).
+ proc; inline*; sp; if; auto; sim.
by auto.
by auto.
qed.
(** We bound the RCPA advantage of A against MEE(P,M) **)
local lemma MtE_security &m:
`|Pr[INDR_CPA(MacThenEncrypt(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),MAC),RCPA_QueryBounder(A)).main() @ &m: res]
- Pr[INDR_CPA(Ideal,RCPA_QueryBounder(A)).main() @ &m: res]|
= `|Pr[SKEa.RCPA.INDR_CPA(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A))).main() @ &m: res]
- Pr[SKEa.RCPA.INDR_CPA(SKEa.RCPA.Ideal,RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A))).main() @ &m: res]|.
proof.
(* Unfortunately, we have several copies of the modules and
alpha conversion does not work at module level, so we need
to prove that it implies semantic equality. This is easy. *)
rewrite -(RCPA_WUF_RCPA.RCPA_preservation (<: PadThenEncrypt(IV_Wrap(CBC(PseudoRP)))) MAC (<: RCPA_QueryBounder(A)) &m _ _).
by proc; rnd predT; auto=> />; smt (d_mK_uffu).
by proc.
do !congr.
by byequiv=> //=; sim.
byequiv=> //=. proc; inline *; wp; call (_: ={glob RCPA_QueryBounder}).
proc; inline *; sp; if=> //=; auto; [smt (leak_pad pad_tag)|sim].
by auto.
qed.
local lemma PtE_security &m:
`|Pr[SKEa.RCPA.INDR_CPA(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A))).main() @ &m: res] - Pr[SKEa.RCPA.INDR_CPA(SKEa.RCPA.Ideal,RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A))).main() @ &m: res]|
= `|Pr[CoreDefs.RCPA.INDR_CPA(IV_Wrap(CBC(PseudoRP)),RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A)))).main() @ &m: res] - Pr[CoreDefs.RCPA.INDR_CPA(CoreDefs.RCPA.Ideal,RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A)))).main() @ &m: res]|.
proof.
(* The same issue arises here *)
rewrite -(RCPA_preservation (<: IV_Wrap(CBC(PseudoRP))) (<: RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A))) &m).
do !congr.
by byequiv=> //=; sim.
byequiv=> //=; proc; inline *.
wp; call (_: ={glob RCPA_QueryBounder, glob RCPA_WUF_RCPA.RCPAa}).
by proc; inline *; sp; if=> //=; sim.
by auto.
qed.
local lemma CBC_security &m:
`|Pr[CoreDefs.RCPA.INDR_CPA(IV_Wrap(CBC(PseudoRP)),RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A)))).main () @ &m: res]
- Pr[CoreDefs.RCPA.INDR_CPA(CoreDefs.RCPA.Ideal,RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A)))).main () @ &m: res]|
= `|Pr[CBCa.SKEa.RCPA.INDR_CPA(IV_Wrap(CBC(PseudoRP)),QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res]
- Pr[CBCa.SKEa.RCPA.INDR_CPA(CBCa.SKEa.RCPA.Ideal,QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res]|.
proof.
(* We have the same issue PLUS we need to move the QueryBounder around.
A much better way of doing this would be to make sure that each library
defines its own QueryCounter and QueryBounder and to make sure that
abstract security results come in both bounded and unbounded (when
possible) flavours. This is TODO when we rework the crypto libraries *)
have PushQueryBounder: forall (O <: CBCa.SKEa.RCPA.RCPA_Oracles { A, RCPA_QueryBounder, OracleBounder, RCPA_WUF_RCPA.RCPAa }),
equiv [QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)),O).distinguish
~ RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A)),O).distinguish
: ={arg, glob A, glob O} ==> ={res}].
move=> O; proc; inline *.
wp; call (_: ={glob O, glob RCPA_WUF_RCPA.RCPAa}
/\ ={qC}(OracleBounder,RCPA_QueryBounder)).
proc; inline *.
case ((RCPA_QueryBounder.qC < q /\ size (pad (p,witness)) <= n){2}).
rcondt{2} 2; 1:by auto.
rcondt{1} 8; 1:by auto; smt (pad_tag).
wp; call (_: true).
by auto.
rcondf{2} 2; 1:by auto.
rcondf{1} 8; 1:by auto; smt (pad_tag).
wp; while ( ={i, p}
/\ r{1} = c{2}
/\ p0{1} = pad (p,t){1}).
by auto; smt (pad_tag).
by auto; smt (max_pad_n pad_tag).
by auto.
have ->: Pr[CBCa.SKEa.RCPA.INDR_CPA(IV_Wrap(CBC(PseudoRP)),QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res]
= Pr[CBCa.SKEa.RCPA.INDR_CPA(IV_Wrap(CBC(PseudoRP)),RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A)))).main() @ &m: res].
byequiv=> //=; proc.
call (PushQueryBounder (CBCa.SKEa.RCPA.RCPA_Wrap(IV_Wrap(CBC(PseudoRP))))).
by call (_: true); auto.
have ->: Pr[CBCa.SKEa.RCPA.INDR_CPA(CBCa.SKEa.RCPA.Ideal,QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res]
= Pr[CBCa.SKEa.RCPA.INDR_CPA(CBCa.SKEa.RCPA.Ideal,RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A)))).main() @ &m: res].
byequiv=> //=; proc.
call (PushQueryBounder (CBCa.SKEa.RCPA.RCPA_Wrap(CBCa.SKEa.RCPA.Ideal))).
by call (_: true); auto.
do !congr.
by byequiv=> //=; sim.
byequiv=> //=; proc.
inline *; wp.
call (_: ={glob RCPA_QueryBounder, glob RCPA_WUF_RCPA.RCPAa}
/\ ={k}(CoreDefs.RCPA.RCPA_Wrap,CBCa.SKEa.RCPA.RCPA_Wrap)).
by proc; inline *; sp; if=> //=; sim.
by auto.
qed.
local lemma local_conclusion &m:
`|Pr[INDR_CPA(MacThenEncrypt(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),MAC),RCPA_QueryBounder(A)).main () @ &m: res]
- Pr[INDR_CPA(Ideal,RCPA_QueryBounder(A)).main() @ &m: res]|
<= `|Pr[IND(PRP, PRPF_Adv(QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))))).main() @ &m : res]
- Pr[IND(PRPi, PRPF_Adv(QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))))).main() @ &m : res]|
+ 2%r * ((q * n) ^ 2)%r * mu d_block (pred1 witness).
proof.
have := Conclusion (<: RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))) &m _.
move=> O O_enc_ll.
proc; inline *.
wp; call (_: true); 1:exact/A_distinguish_ll.
by proc; inline *; wp; call O_enc_ll; auto.
by wp; rnd predT; auto; smt (d_mK_uffu).
rewrite (MtE_security &m) (PtE_security &m) (CBC_security &m).
(* Here again, we have to tell EasyCrypt that alpha equality implies semantic equality *)
have ->: Pr[PRFt.IND(PRPr.PRP, PRPF_Adv(QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))))).main() @ &m: res]
= Pr[IND(PRP,PRPF_Adv(QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))))).main() @ &m: res].
by byequiv=> //=; sim.
have ->: Pr[PRFt.IND(PRPi.PRPi, PRPF_Adv(QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))))).main() @ &m: res]
= Pr[IND(PRPi,PRPF_Adv(QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))))).main() @ &m: res].
by byequiv=> //=; sim.
have ->: Pr[CBCa.SKEa.RCPA.INDR_CPA(IV_Wrap(CBC(PRPr.PseudoRP)),QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res]
= Pr[CBCa.SKEa.RCPA.INDR_CPA(IV_Wrap(CBC(PseudoRP)),QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res].
by byequiv=> //=; sim.
(* And we conclude by proving the equivalence of the Random module and the Ideal module used in IND$-CPA *)
have ->: Pr[CBCa.SKEa.RCPA.INDR_CPA(Random,QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res]
= Pr[CBCa.SKEa.RCPA.INDR_CPA(CBCa.SKEa.RCPA.Ideal,QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res].
byequiv=> //=; proc; inline *; wp.
call (_: ={glob OracleBounder, glob RCPA_WUF_RCPA.RCPAa}).
proc.
call (_: ={glob OracleBounder}).
call (_: ={glob OracleBounder}).
sp; if=> //=; 2:by sim.
wp; call (_: true)=> //=.
by call Random_Ideal=> //=.
by auto.
by call (_: true); auto.
by auto.
done.
qed.
local lemma CleanupAdversary (P <: PRP { A, Weak_PRPa, OracleBounder, RCPA_WUF_RCPA.RCPAa }) &m:
Pr[IND(P,Weak_PRPa(MAC,A)).main() @ &m: res]
= Pr[IND(P, PRPF_Adv(QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))))).main() @ &m : res].
proof.
byequiv (_: ={glob P, glob A} ==> ={res})=> //=; proc; inline *; wp.
call (_: ={glob P}
/\ ={qC}(Weak_PRPa,OracleBounder)
/\ Weak_PRPa.mk{1} = RCPA_WUF_RCPA.RCPAa.mk{2})=> //=.
proc; inline *; sp.
if; 1:smt (max_pad_n pad_tag).
+ by sim; auto.
wp; while ( ={i}
/\ size (pad (p,witness)){1} = size p0{2}
/\ c{1} = r{2});
1:by auto=> /#.
by auto; smt (pad_tag).
by auto; call (_: true).
qed.
lemma RCPA_security &m:
`|Pr[INDR_CPA(MEE(PseudoRP,MAC),RCPA_QueryBounder(A)).main() @ &m: res]
- Pr[INDR_CPA(Ideal,RCPA_QueryBounder(A)).main() @ &m: res]|
<= `|Pr[IND(PRP, Weak_PRPa(MAC,A)).main() @ &m : res]
- Pr[IND(PRPi, Weak_PRPa(MAC,A)).main() @ &m: res]|
+ 2%r * ((q * n) ^ 2)%r * mu d_block (pred1 witness).
proof.
rewrite (MEE_unfold &m) (CleanupAdversary PRP &m) (CleanupAdversary PRPi &m).
exact/(local_conclusion &m).
qed.
end section RCPA.
(* From the PRP and a PTXT adversary against MtE, we construct a WUF-CMA adversary against the MAC *)
module CMAa (P : PseudoRP) (A : PTXT_Adversary) (M : CMA_Oracles) = {
var ek: eK
module O = {
proc enc(m:msg): block list = {
var i, s, t, padded, pi;
var c <- witness;
t <@ M.tag(m);
padded <- pad(m,t);
s <$ d_block;
c <- [s];
i <- 0;
while (i < size padded) {
pi <- nth witness padded i;
s <@ P.f(ek,s + pi);
c <- c ++ [s];
i <- i + 1;
}
return c;
}
proc verify(c:block list): bool = {
var pt, pi, padded, b, s, i, ci;
b <- false;
(* compute CBC decryption (first block is iv) *)
s <- head witness c;
c <- behead c;
padded <- [];
i <- 0;
while (i < size c) {
ci <- nth witness c i;
pi <@ P.fi(ek,ci);
padded <- padded ++ [s + pi];
s <- ci;
i <- i + 1;
}
(* strip padding *)
pt <- unpad padded;
(* check MAC *)
if (pt <> None) {
b <@ M.verify(oget pt);
}
return b;
}
}
proc forge(): unit = {
ek <@ P.keygen();
A(O).forge();
}
}.
section PTXT.
declare module A : PTXT_Adversary { WUF_Wrap, PTXT_Wrap, CMAa }.
axiom A_forge_ll (O <: PTXT_Oracles { A }):
islossless O.enc => islossless O.verify => islossless A(O).forge.
(** TODO: this is not useful apart from avoiding having to define
the part of the scheme that we don't care about **)
local clone import CBC as CBCb (* FIXME *) with
op q <- q,
op ell <- n,
type key <- eK,
op dKey <- d_eK,
type block <- block,
op dBlock <- d_block,
op zeros <- zeros,
op (+) <- (+),
op P <- P,
op Pi <- Pi
proof *.
realize gt0_q by exact/gt0_q.
realize gt0_ell by smt (gt1_n).
realize dKey_uffu by smt(@Distr d_eK_uffu).
realize dBlock_uffu by smt(@Distr d_block_uffu).
realize add0b by exact/add0b.
realize addbA by exact/addbA.
realize addbC by exact/addbC.
realize addbK by exact/addbK.
realize bijective_P. by move=> k; apply/bijectiveP; smt(@Distr d_eK_uffu). qed.
(** TODO: ditto **)
local clone import RCPA_pad as PtEb (* FIXME *) with
type key <- eK,
type ptxt <- block list,
type ctxt <- block list,
type msg <- msg * tag,
type leaks_m <- msg,
type leaks_p <- int,
op leak_m (mt : msg * tag) <- leak mt.`1,
op leak_p <- size<:block>,
op pad <- pad,
op unpad <- unpad,
op dC_m (m : msg) <- CBCa.dBlocks (size (pad (m,witness<:tag>)) + 1),
op dC_p (l : int) <- CBCa.dBlocks (l + 1)
proof * by smt (dlist_ll d_block_uffu can_unpad leak_pad pad_tag).
(** See comment in CPA proof **)
local clone import RCPA_CMA as MtEb (* FIXME *) with
type MtE.mK <- mK,
type MtE.eK <- eK,
type MtE.ptxt <- msg,
type MtE.ctxt <- block list,
type MtE.tag <- tag,
type MtE.leaks <- msg,
op MtE.leak (m : msg) <- leak m,
op MtE.dC (m : msg) <- CBCa.dBlocks (size (pad (m,witness<:tag>)) + 1)
proof MtE.* by smt (dlist_ll d_block_uffu).
import MtEb.MtE.
local lemma MEE_unfold &m:
Pr[INT_PTXT(MEE(PseudoRP,MAC),A).main() @ &m: res]
= Pr[INT_PTXT(MacThenEncrypt(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),MAC),A).main () @ &m: res].
proof.
byequiv (_: ={glob A} ==> ={res})=> //=; proc; inline *.
wp; call (_: ={glob PTXT_Wrap})=> //=.
by proc; inline *; sim; auto.
proc; inline *; sim.
by wp=> //=; sim.
by auto.
qed.
(** We bound the PTXT advantage of A against MEE(P,M) **)
local lemma local_conclusion &m:
Pr[INT_PTXT(MacThenEncrypt(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),MAC),A).main () @ &m: res]
<= Pr[MACa.WUF_CMA.WUF_CMA(MAC,RCPA_WUF_PTXT.CMAa(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),A)).main() @ &m: res].
proof.
have ->: Pr[INT_PTXT(MacThenEncrypt(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),MAC),A).main() @ &m: res]
= Pr[Sec.PTXT.INT_PTXT(MacThenEncrypt(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),MAC),A).main() @ &m: res].
by byequiv=> //=; proc; inline *; sim.
apply/(RCPA_WUF_PTXT.PTXT_security (<: PadThenEncrypt(IV_Wrap(CBC(PseudoRP)))) MAC A _ _ _ _ _ _ _ &m).
by proc; wp; rnd predT; auto; smt (d_eK_uffu).
proc; inline *; wp; while (0 <= i <= size p0) (size p0 - i).
by move=> z; auto=> /#.
by wp; rnd predT; auto; smt (d_block_uffu size_ge0).
proc; inline *; wp; while (0 <= i <= size c1) (size c1 - i).
by move=> z; auto=> /#.
by auto; smt (size_ge0).
by proc; rnd predT; skip; smt (d_mK_uffu).
by proc.
by proc.
by move=> O O_enc_ll O_verify_ll; apply (A_forge_ll O). (* types are different but the same *)
qed.
local lemma CleanupAdversary &m:
Pr[MACa.WUF_CMA.WUF_CMA(MAC,RCPA_WUF_PTXT.CMAa(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),A)).main() @ &m: res]
= Pr[WUF_CMA(MAC,CMAa(PseudoRP,A)).main() @ &m: res].
proof.
byequiv=> //=; proc; inline *; wp.
call (_: ={ek}(RCPA_WUF_PTXT.CMAa,CMAa)
/\ ={s,k,win}(MACa.WUF_CMA.WUF_Wrap,WUF_Wrap)).
by proc; inline *; wp;
while ( ={i, s}
/\ c2{1} = c{2}
/\ p1{1} = padded{2}
/\ key0{1} = CMAa.ek{2});
auto.
by proc; inline *; wp;
while ( ={i, s}
/\ c2{1} = c{2}
/\ p2{1} = padded{2}
/\ key0{1} = CMAa.ek{2});
auto.
by auto.
qed.
lemma PTXT_security &m:
Pr[INT_PTXT(MEE(PseudoRP,MAC),A).main () @ &m: res]
<= Pr[WUF_CMA(MAC,CMAa(PseudoRP,A)).main() @ &m: res].
proof.
rewrite (MEE_unfold &m) -(CleanupAdversary &m).
exact/(local_conclusion &m).
qed.
end section PTXT.