https://github.com/EasyCrypt/easycrypt
Tip revision: ff9ce6452dfed3aad05c732176ce072c8670b199 authored by Pierre-Yves Strub on 03 December 2019, 06:15:32 UTC
Merge remote-tracking branch 'origin/1.0' into deploy-taylor
Merge remote-tracking branch 'origin/1.0' into deploy-taylor
Tip revision: ff9ce64
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);
}
}.