https://github.com/EasyCrypt/easycrypt
Tip revision: 846710a2a656834065e745d19416ebdc83158f55 authored by Benjamin Gregoire on 14 July 2019, 06:50:07 UTC
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Tip revision: 846710a
OW.ec
(* --------------------------------------------------------------------
* 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
* -------------------------------------------------------------------- *)
(* One-Way Trapdoor Permutations *)
require import Core Distr.
(** Abstract declarations to be refined when instantiating *)
(* Domain and Range *)
type D, R.
(* Keys *)
type pkey, skey.
op dkeys: (pkey * skey) distr.
axiom dkeys_ll: is_lossless dkeys.
pred valid_keys (ks:pkey * skey) = support dkeys ks.
pred valid_pkey (pk:pkey) = exists sk, valid_keys (pk,sk).
pred valid_skey (sk:skey) = exists pk, valid_keys (pk,sk).
(* The distribution from which the challenge is sampled *)
(* Note: We use its support as the permutation's domain! *)
op challenge: pkey -> D distr.
axiom challenge_ll pk:
valid_pkey pk => is_lossless (challenge pk).
axiom challenge_uni pk:
valid_pkey pk => is_uniform (challenge pk).
(** Concrete definitions *)
op f: pkey -> D -> R.
pred f_dom (pk:pkey) (x:D) =
valid_pkey pk => x \in (challenge pk).
pred f_rng (pk:pkey) (y:R) =
valid_pkey pk => exists x, f_dom pk x /\ y = f pk x.
op finv: skey -> R -> D.
axiom finv_correct (pk:pkey) (sk:skey) y:
valid_keys (pk,sk) =>
f_rng pk y =>
f_dom pk (finv sk y).
axiom finvof (pk:pkey) (sk:skey) (x:D):
valid_keys (pk,sk) =>
f_dom pk x =>
finv sk (f pk x) = x.
axiom fofinv (pk:pkey) (sk:skey) (x:R):
valid_keys (pk,sk) =>
f_rng pk x =>
f pk (finv sk x) = x.
(* This is often useful to extract plaintexts *)
lemma f_pk_inj (x, y:D) (pk:pkey) (sk:skey):
valid_keys (pk,sk) =>
f_dom pk x => f_dom pk y =>
f pk x = f pk y => x = y.
proof.
by move=> Hsupp Hdom_x Hdom_y Heqf;
rewrite -(finvof pk sk) // -(finvof pk sk y) // Heqf.
qed.
(** We can now define the module types and modules that define security **)
module type Inverter = {
proc invert(pk : pkey, y : R) : D
}.
module OW(I :Inverter) ={
proc main(): bool ={
var x,x':D;
var pk:pkey;
var sk:skey;
(pk,sk) = $dkeys;
x = $challenge pk;
x' = I.invert(pk,f pk x);
return (x = x');
}
}.