https://github.com/EasyCrypt/easycrypt
Tip revision: 9f6a2f9c698e6c47fa841a0b040bc45d82a601c5 authored by Benjamin Gregoire on 07 July 2016, 06:32:45 UTC
add make
add make
Tip revision: 9f6a2f9
CCA1.eca
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2016 - Inria
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
require import Bool Option.
require (*--*) NewSKE.
clone include NewSKE.
module type CCA1 = {
proc enc(p: plain): cipher option
proc dec(c: cipher): plain option
}.
module type Adv_CCA1 (O : CCA1) = {
proc choose(): plain * plain
proc guess(c: cipher): bool { O.enc }
}.
module IND_CCA1 ( S : SKE, A : Adv_CCA1) = {
module O = Wrap(S)
module A = A(O)
proc main(): bool = {
var b, b', c, p0, p1, p;
O.init();
(p0,p1) = A.choose();
b = ${0,1};
p = b ? p1 : p0; (* FIXME: need to check whether plaintexts are both valid or both invalid *)
c = O.enc(p);
b' = A.guess(oget c);
return b = b';
}
}.