https://github.com/EasyCrypt/easycrypt
Tip revision: 2075873964476cccac0722f071bfaf1252c3c2ac authored by François Dupressoir on 10 May 2022, 11:31:18 UTC
Birthday refinements
Birthday refinements
Tip revision: 2075873
PRF.eca
require import AllCore Distr FSet.
pragma +implicits.
(** 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 = {
var r;
if (x \notin m) {
r <$ dR x;
m.[x] <- r;
}
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.