https://github.com/EasyCrypt/easycrypt
Tip revision: 86266aebe9e85f235009269211a06e2e0a1784a0 authored by Pierre-Yves Strub on 12 February 2020, 17:00:54 UTC
rigid auto rewrite
rigid auto rewrite
Tip revision: 86266ae
PRF.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 AllCore Distr FSet.
pragma +implicits. pragma -oldip.
(** A PRF is a family of functions F from domain D to finite range R
indexed by a keyspace K equipped with a (lossless) distribution dK. *)
type D, R.
module type PRF = {
proc init(): unit
proc f(_ : D): R
}.
module type PRF_Oracles = {
proc f(_: D): R
}.
module type Distinguisher (F : PRF_Oracles) = {
proc distinguish(): bool
}.
module IND (F : PRF) (D : Distinguisher) = {
proc main(): bool = {
var b;
F.init();
b <@ D(F).distinguish();
return b;
}
}.
(* -------------------------------------------------------------------- *)
abstract theory RF.
require import SmtMap.
op dR: { D -> R distr | forall x, is_lossless (dR x) } as dR_ll.
module RF = {
var m : (D,R) fmap
proc init(): unit = {
m <- empty;
}
proc f(x:D): R = {
if (x \notin m) {
m.[x] <$ dR x;
}
return (oget m.[x]);
}
}.
end RF.
(* -------------------------------------------------------------------- *)
abstract theory PseudoRF.
type K.
op dK: { K distr | is_lossless dK } as dK_ll.
op F : K -> D -> R.
module type PseudoRF = {
proc keygen(): K
proc f(_ : K * D): R
}.
module PseudoRF = {
proc keygen() = {
var k;
k <$ dK;
return k;
}
proc f(k, x) = { return F k x; }
}.
module PRF = {
var k : K
proc init() = { k <$ dK; }
proc f(x: D) = { return F k x; }
}.
end PseudoRF.