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.

Stating and proving program equivalences in F*

We aim to formalize and mechanize the state-separating proofs for packages within F*.

We see several potential benefits of doing this:

• Working in F*'s dependently typed logic, we have the expressive power to speak about non-trivial equivalences at higher order

• F*'s support for effects allow us to reason about equivalences among effectful programs, where effects (especially state) are pervasive in the state-separating proofs methodology

• F*'s support for a combination of SMT and tactics may allow us to attain a good degree of automation for these proofs

• Given extensive prior work in F* on libraries that provide efficient, verified, low-level implementations of cryptographic primitives, we hope to be able to apply, through several steps of abstractions, our methodology for cryptographic security proofs to those low-level implementations themselves.

Towards this end, we have started to design a library in which to state equivalences, including epsilon equivalences, among values, functions, modules, and functors.

At the core of our library is a specification style based on setoids. Setoids (see Barthe et al. [2] for an introduction) equip a type with an equivalence relation---technically, we work with partial setoids which equip types with partial equivalence relation or PER, a symmetric, transitive relation that is not necessarily reflexive.

The following module defines our library of Setoids: https://github.com/FStarLang/FStar/blob/nik_lib/examples/rel/Setoids.fst

Using that library, we can state and prove several simple equivalences, automatically. For example, the code below proves that the identity function fun x -> x is relationally parametric, i.e., given any relation arel on the input type a, given x0 and x1 related by arel, id x0 and id x1 are also related by arel.

let id #a (arel:rel a) : (arel ^--> arel) = fun x -> x

Unpeeling the syntax a bit, give two relations arel: rel a and brel: rel b, the type arel ^--> brel is the type of functions f : a -> b that additionally satisfy the following property:

forall (x0 x1:a). arel x0 x1 ==> brel (f x0) (f x1)

That is, arel ^--> brel functions are those that take arel-related arguments to brel-related results.

Briefly, we define

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