swh:1:snp:1160b607213f14ec0f922dad3284705c8e588b30
Tip revision: ce01988409000c56ae7602f0b00f28e9417494d7 authored by Adrien Koutsos on 19 June 2020, 11:54:46 UTC
allow cost precondition in rcondf, rcondt and if tactics
allow cost precondition in rcondf, rcondt and if tactics
Tip revision: ce01988
SKE_INDR.eca
require import AllCore Int Real Distr.
(** Given types for keys, plaintexts and ciphertexts **)
type eK, ptxt, ctxt.
(** and a leakage function (modelling the information about the
plaintext that can be inferred from the ciphertext) **)
type leaks.
op leak: ptxt -> leaks.
(* and a distribution on ciphertexts parameterized by leaks, used to
specify security *)
op dC: leaks -> ctxt distr.
axiom dC_ll p: is_lossless (dC p).
(* An encryption scheme is a triple of algorithm *)
module type Enc_Scheme = {
proc keygen() : eK
proc enc(k:eK, p:ptxt): ctxt
proc dec(k:eK, c:ctxt): ptxt option
}.
theory RCPA. (* IND$-CPA *)
module type RCPA_Oracles = {
proc enc(p:ptxt): ctxt
}.
module type RCPA_Adversary(O : RCPA_Oracles) = {
proc distinguish() : bool
}.
module RCPA_Wrap (S : Enc_Scheme): RCPA_Oracles = {
var k: eK
proc enc(p:ptxt): ctxt = {
var c;
c <@ S.enc(k,p);
return c;
}
}.
module INDR_CPA (S:Enc_Scheme, A:RCPA_Adversary) = {
proc main(): bool = {
var b;
RCPA_Wrap.k <@ S.keygen();
b <@ A(RCPA_Wrap(S)).distinguish();
return b;
}
}.
module Ideal = {
proc keygen(): eK = { return witness; }
proc enc(k:eK,p:ptxt): ctxt = {
var r;
r <$ dC (leak p);
return r;
}
proc dec(k:eK,p:ctxt): ptxt option = {
return None;
}
}.
(** An encryption scheme S is IND$-CPA secure if, for all
* "reasonable" adversary A, the following quantity is "small":
*
* Adv^{IND$-CPA}_{S}(A,&m)
* = `|Pr[INDR_CPA(S,A).main() @ &m: res]
* - Pr[INDR_CPA(Ideal,A).main() @ &m: res]|
**)
end RCPA.
theory PTXT.
require import FSet.
(* Definitions for INT-PTXT security *)
module type PTXT_Oracles = {
proc enc(p:ptxt) : ctxt
proc verify(c:ctxt): bool
}.
module type PTXT_Adversary (O : PTXT_Oracles) = {
proc forge(): unit
}.
module PTXT_Wrap (S : Enc_Scheme): PTXT_Oracles = {
var k : eK
var s : ptxt fset
var win: bool
proc init(): unit = {
k <@ S.keygen();
s <- fset0;
win <- false;
}
proc enc(p:ptxt): ctxt = {
var c;
c <@ S.enc(k,p);
s <- s `|` (fset1 p);
return c;
}
proc verify(c:ctxt): bool = {
var p;
p <@ S.dec(k,c);
win <- win \/ (p <> None /\ !mem s (oget p));
return (p <> None);
}
}.
module INT_PTXT (S : Enc_Scheme, A : PTXT_Adversary) = {
proc main(): bool = {
PTXT_Wrap(S).init();
A(PTXT_Wrap(S)).forge();
return PTXT_Wrap.win;
}
}.
(* An encryption scheme E : Enc_Scheme is said to be INT-PTXT
secure whenever, for all "efficient" PTXT adversary A, the
following quantity is "small":
Adv^{INT-PTXT}_{E}(A) = Pr[INT_PTXT(E,A).main: res] *)
end PTXT.
theory CTXT.
require import FSet.
(* Definitions for INT-CTXT security *)
module type CTXT_Oracles = {
proc enc(p:ptxt) : ctxt
proc verify(c:ctxt): bool
}.
module type CTXT_Adversary (O : CTXT_Oracles) = {
proc forge(): unit
}.
module CTXT_Wrap (S : Enc_Scheme): CTXT_Oracles = {
var k : eK
var s : ctxt fset
var win: bool
proc init(): unit = {
k <@ S.keygen();
s <- fset0;
win <- false;
}
proc enc(p:ptxt): ctxt = {
var c;
c <@ S.enc(k,p);
s <- s `|` (fset1 c);
return c;
}
proc verify(c:ctxt): bool = {
var p;
p <@ S.dec(k,c);
win <- win \/ (p <> None /\ !mem s c);
return (p <> None);
}
}.
module INT_CTXT (S : Enc_Scheme, A : CTXT_Adversary) = {
proc main(): bool = {
CTXT_Wrap(S).init();
A(CTXT_Wrap(S)).forge();
return CTXT_Wrap.win;
}
}.
(* An encryption scheme E : Enc_Scheme is said to be INT-CTXT
secure whenever, for all "efficient" CTXT adversary A , the
following quantity is "small":
Adv^{INT-CTXT}_{E}(A) = Pr[INT_CTXT(E,A).main: res] *)
end CTXT.