https://github.com/EasyCrypt/easycrypt
Tip revision: 644ddc2e7f7b1bab87c4775250c430104c7d9f69 authored by Pierre-Yves Strub on 09 August 2022, 07:51:07 UTC
Fix a typing annotation bug in distribution tags' axioms
Fix a typing annotation bug in distribution tags' axioms
Tip revision: 644ddc2
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.