https://github.com/EasyCrypt/easycrypt
Tip revision: 8bceccd0cf22999f88e5e30e1269c6153b519729 authored by Cécile BARITEL-RUET on 13 December 2017, 16:30:02 UTC
.
.
Tip revision: 8bceccd
PKE_CPA.eca
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2017 - Inria
*
* 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);
}
}.