Relational F* for State Separating Cryptographic Proofs

Introduction

This page documents a project started in April 2019 by Markulf Kohlweiss, Konrad Kohbrok, Tahina Ramananandro and Nikhil Swamy to use relational F* (TODO: Which paper to cite for relational F*?) to conduct cryptographic proofs written in the State-Separating Proof (SSP) framework introduced in [1].

State-Separating proofs

The state-separating proof (SSP) framework was introduced in [1] and is meant to help writing modular, code-based cryptographic proofs. To reason about oracles and the state they operate on, SSPs use Packages that contains a set of oracles and their shared state. Packages provide oracles, such that other packages or the adversary (who can also be seen as a package) can call them. We can thus, for example, instantiate a traditional security definition based in indistinguishability as the adversary's inability to distinguish between two packages up to some epsilon. In that example, the indistinguishability bit would be 0 in one package and 1 in the other. We call this indistinguishability up to some epsilon "epsilon-equivalence". Similarly, we can model a reduction as a package that is composed with (i.e. calls the oracles provided by) packages representing individual security assumptions.

Much like traditional cryptographic proofs, SSPs require proving that a given reduction (composed with a number of assumptions) simulates the original security game correctly for the adversary. This simulation correctness can be established by proving that the composed reduction is perfectly equivalent to the original security game.

After establishing simulation correctness, we can then use the package algebra provided by [1] to make game hops, for example to idealize a given assumption. Each game hop gives us epsilon-equivalence between two (composed) packages.

For a complete proof, we thus need (a) perfect equivalence between security game and composed reduction (for both the real and the ideal game), as well as a number of game hops that give us an epsilon-equivalence between the reduction equivalent to the real game and the reduction equivalent to the ideal game. We thus ultimately have an epsilon-equivalence between real- and ideal game, concluding the proof.

Relational F*

Relational F* was introduced in [3] (more history/related work/context here). Instead of defining types in terms of just their value, we also provide a relation for that type, i.e. a function mapping two instances to a boolean.

[TODO: Explain differences between bool and Type0 here.]

[TODO: Should we also introduce the information flow stuff? I currently don't use it for anything. If we don't end up using it, maybe we can "skip" pers and only work with erels.]

let rel (s:Type) = s -> s -> Type0

In most cases that we're interested in here, this relation is going to be an equivalence relation.

let equiv (#s:Type) (r: rel s) =
  forall x. x `r` x /\
  forall x y. x `r` y <==> y `r` x /\
  forall x y z. x `r` y /\ y `r` z ==> x `r` z

let erel (s:Type) = r:rel s { equiv r }

[TODO: Probably rename the following if we don't introduce the information flow mechanics.]

let lo a : erel a = fun x y -> (x == y <: prop)

We can also define equivalence relations for functions and create an operator to use it more easily.

let arrow_rel (#a:Type) (#b:Type) (arel:rel a) (brel:rel b) (f g : (a -> b)) : prop =
    forall x0 x1. x0 `arel` x1 ==>
             f x0 `brel` g x1

let ( ^--> ) (#a:Type) (#b:Type) (arel:rel a) (brel:rel b) =
  f:(a -> b){ f `arrow_rel arel brel` f}

A small example: We can prove that the following functions are indeed equivalent.

let f : (lo int ^--> lo int) = fun x -> x + 45
let f' : (lo int ^--> lo int) = fun x -> 45 + x

let f_rel_f' : squash (f `arrow_rel (lo int) (lo int)` f') = ()

[TODO: Introduce state monad]

Cryptographic Notions of Equivalence in F*

[TODO: Introduce signatures, modules and composition.] [TODO: Introduce epsilons and the eq type.]

[TODO: References. Most importantly a pointer to the code.] [1]: https://eprint.iacr.org/2018/306