swh:1:snp:44a5c6c33fe8f30e42c028fce02d1c96d6b89575
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
OW_PCVA.ec
require import Bool Core Int List Distr.
require import DBool.
type pkey, skey, ptxt, ctxt.
op dptxt : ptxt distr.
axiom dptxt_ll : is_lossless dptxt.
axiom dptxt_uni : is_uniform dptxt.
axiom dptxt_full : is_full dptxt.
module type Scheme = {
(* Key generation *)
proc kg () : pkey * skey
(* Encryption *)
proc enc (pk : pkey, m : ptxt) : ctxt
(* Decryption *)
proc dec (sk : skey, c : ctxt) : ptxt option
}.
module type OraclesT = {
(* Plaintext checking oracle for *valid* cipher-texts *)
proc ptxt_check (m : ptxt, c : ctxt) : bool
(* Cipher-text validity oracle, except for the challenge cipher-text. *)
proc ctxt_val (c : ctxt) : bool
}.
module type Inverter (S : Scheme) (O : OraclesT) = {
proc invert(pk : pkey, c : ctxt) : ptxt
}.
module Oracles (S : Scheme) = {
var sk : skey
var c0 : ctxt
proc init (sk : skey, c0 : ctxt) : unit = {
sk <- sk;
c0 <- c0;
}
proc ptxt_check (m : ptxt, c : ctxt) : bool = {
var m0;
m0 <@ S.dec (sk, c);
return is_none m0 \/ oget m0 = m;
}
proc ctxt_val (c : ctxt) : bool = {
var m = None;
if (c <> c0) {
m <@ S.dec (sk,c);
}
return !is_none m;
}
}.
module OW (S : Scheme) (I : Inverter) = {
proc main(): bool ={
var pk, sk, m, c, m';
var is_inv : bool;
(pk,sk) <@ S.kg();
m <$ dptxt;
c <@ S.enc (pk, m);
Oracles(S).init(sk, c);
(* The adversary tries to invert C *)
m' <@ I(S, Oracles(S)).invert(pk, c);
(* We check if m' is the invert of c using the oracle.
If the schema is correct here, i.e. if dec sk c = m, this corresponds
to checking whether m = m'. *)
is_inv <@ Oracles(S).ptxt_check (m',c);
return is_inv;
}
}.