https://github.com/EasyCrypt/easycrypt
Tip revision: 0dd57f714852f6f779d230c5bbf3e98e4594f41f authored by François Dupressoir on 06 December 2019, 09:55:55 UTC
OneMap-PRP: a PRP with a single map and lemmas to switch
OneMap-PRP: a PRP with a single map and lemmas to switch
Tip revision: 0dd57f7
PKE_CPA.eca
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
require import Bool Core Int List.
require import DBool.
type pkey, skey, ptxt, ctxt.
module type Scheme = {
proc kg() : pkey * skey
proc enc(pk:pkey, m:ptxt) : ctxt
}.
module type Adversary = {
proc choose(pk:pkey) : ptxt * ptxt
proc guess(c:ctxt) : bool
}.
module CPA (S:Scheme) (A:Adversary) = {
proc main() : bool = {
var pk, sk, m0, m1, c, b, b';
(pk, sk) = S.kg();
(m0, m1) = A.choose(pk);
b = ${0,1};
c = S.enc(pk, b ? m1 : m0);
b' = A.guess(c);
return (b' = b);
}
}.