Skip to content

Relational F* for State Separating Cryptographic Proofs

Jump to bottom Edit New page
Konrad Kohbrok edited this page Jan 4, 2020 · 6 revisions

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, game-playing 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.

To better explain SSPs, we will use the Public Key Authenticated Encryption (PKAE) as a running example. Consider PKAE the public key variant of the indistinguishability notion $AE, where the adversary has access to an encryption oracle ENC and a decryption oracle DEC. In the real case, ENC and DEC perform encryption and decryption using the scheme's algorithms and the secret key. In the ideal case, ENC outputs random ciphertexts and saves the plaintexts in a log indexed by the corresponding ciphertext, while DEC simply looks up input ciphertexts in a log and outputs either the corresponding plaintext or an error symbol "bot" if the log is empty w.r.t. the input ciphertext.

In the SSP framework, we express the PKAE security notion by bundeling up the ENC and DEC in a two packages PKAE^0 and PKAE^1. The first containing the oracles with real behaviour and the second containing the oracles with ideal behaviour. We then say the two packages are epsilon-equivalent (PKAE^0 ~ PKAE^1), i.e. the packages are indistinguishable up to some epsilon.

A strength of SSPs is the ability to compose packages both sequentially and parallelly. We say that two packages P, P' are composed sequentially (P -> P') if oracles provided by P make queries to oracles provided by P'. More specifically, to compose two packages P, P' sequentially, the oracles provided by P' have to provide oracles that fit the names of those called by oracles provided by P. Note, that two composed packages form again a package (Q := P -> P').

We can also compose two packages P, P' parallelly (P|P'). The thusly composed package Q (with Q := (P|P')) thus provides the oracles of both P and P'.

A simple example for composition is the process of describing a reduction in the SSP framework. Sticking with our earlier PKAE example, let p be a scheme that uses Diffie-Hellman scheme dh to derive a secret key and AE scheme ae to encrypt a message under that key. Then we could construct a reduction as a package R that exposes the same oracles as PKAE^b (ENC and DEC) and that interacts with the packages AE^b (parameterized with ae) and ODH^b' (parameterized with dh) to implement the functionality of those oracles.

R -> (ODH^b'|AE^b)

Much like traditional cryptographic proofs, SSPs require proving that a given reduction 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 for both the real (b=0) and the ideal (b=1) case.

PKAE^0 = R -> (ODH^0|AE^0)
PKAE^1 = R -> (ODH^0|AE^1)

After establishing simulation correctness, we can then use the package algebra provided by [1] to make game hops to idealize (or de-idealize) ODH^b' and AE^b. Each game hop gives us epsilon-equivalence, for example

PKAE^0 = R -> (ODH^0|AE^0)
       ~ R -> (ODH^1|AE^0),

where the epsilon is the epsilon defined in the ODH assumption. For the complete proof, we would have to perform a number of game hops that transitively give us

PKAE^0 = R -> (ODH^0|AE^0)
       ~ R -> (ODH^0|AE^1)
       = PKAE^1

(Note, that the presentation of the "proof" in the example above is simplified in several ways. We will follow up with a formal proof at a later point in time.)

To summarize, SSPs allow us to reason about modular constructions, however the proof mechanic requires proofs of perfect equivalence. On paper, we rely on proof of state invariants across oracle executions or manual code-comparison between oracles. However, with F*, we can do better!

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 relational types. For instances, one specification style we adopt is based on setoids (see Barthe et al. for an introduction), which 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, given 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.

One can also prove simple information-flow style properties by relational typing.

For instance, we can define the lo relation to be equality while the hi relation to be trivial---meaning that when relating two runs of a program, those inputs and outputs that are related by lo contain no secrets and can flow to/from the adversary, while values related by hi may contain secrets.

let lo a : rel a = fun x y -> x == y
let hi a : rel a = fun x y -> True

Using our relational function types, we can give information flow types to some simple programs:

let f1 : (lo int ^--> lo int) = fun x -> x + 45
let f2 : (hi int ^--> hi int) = fun x -> x + 45

Note, the same program can have more than one type (i.e., it may satisfy more than one relation), as in the case of f1 and f2. However, the same term given a type that claims it takes secret inputs and returns public outputs is rejected.

[@(expect_failure [19])]
let f3 : (hi int ^--> lo int) = fun x -> x + 45

Other programs that correctly hide their secret inputs from the adversary are easily accepted.

let f3 : (hi int ^--> lo int) = fun x -> x - x

Aside from these basic equivalences, one can also define relational variants of modules and functors.

Modules in F* (as in ML) are outside the language of terms and do not enjoy the same kinds of abstraction facilities. F* itself lacks any built-in support for functors in its module language.

However, to state equivalences among modules and functors, we encode modules and functors within F*'s term language. Specifically, we

  • Encode modules as dependent maps from labels (the names of the symbols provided by a module) to values at a given relational type: the relation associated with a module is the pointwise conjunction of the relation of each of its operations
  • Encode functors as relational-preserving maps from modules to modules
  • Enable functors at higher-order, i.e., functors that transform functors to functors are also permitted

Within this regime, we are able to encode the packages of the state-separating proofs methodology as functors, and to prove the algebraic laws of package composition as equivalences among functor compositions. E.g., See https://github.com/FStarLang/FStar/blob/nik_lib/examples/rel/Setoids.fst#L443

We also make use of relational variants of monadic encodings of effects, e.g., the code here shows the definition of a relational variant of a state+exception monad. https://github.com/FStarLang/FStar/blob/nik_lib/examples/rel/Setoids.Example.fst#L16 Specifically, the type eff srel arel shown below is the type of computations that transform srel-related initial states to arel-related optional results and srel-related final states.

let eff (#s:Type) (#a:Type) (srel:erel s) (arel:erel a) =
  srel ^--> ((option_rel arel) ** srel)

Cryptographic notions of equivalence in F*

We can now use the techniques and structures introduced above to implement the SSP framework and the algebra it provides for package composition. We begin by implementing our oracles. Instead of the pseudocode commonly used in code-based, game-playing proofs, we use F* functions to describe our oracles and the state they operate on. Note, that we use the effect introduced in the end of the previous section to model error symbols such as the "bot" returned upon unsuccessful decryption.

Before we can instantiate packages in the way described above, we first introduce signatures. Signatures allow us to specify the functions a package provides and for a oracle of a package to query oracles provided by other packages that implement this signature. A signature contains a set of oracle names (labels), a map from labels to function types (ops) and finally a map from labels to relations on those types (rels). Note, that we call a signature empty if the set of labels is empty.

type sig = {
  labels:eqtype;
  ops:labels -> Type;
  rels:(l:labels -> per (ops l))
}

A package is then a module, which maps an input signature to an output signature. If the oracles of a given package do not query any outside oracles, the input signature is empty. Using signatures, we can now say that two packages are related if they have the same output signature and for all labels we have that the functions of both packages that the label maps to are related under the relation in the signature. If all pairs of oracles of the two packages are thus related under the equivalence relation (equal inputs map to equal outputs), we have proven that the packages are perfectly equivalent.

Finally, we introduce a notion epsilon-equivalences and a package algebra that allows us to make trivial term-transformations that don't incur differences in the epsilon. For example, if P^0~P^1, then for any package R that composes with P^b, we have that R -> P^0 ~ R -> P^1.

To instantiate an epsilon equivalence, we have to introduce an assumption, which we can do by indeed using the assume qualifier provided natively by F*.

Example: Crypto Box

To demonstrate the technique described above, we have implemented (but not yet completely verified) a security proof of the Cryptobox protocol, a simple KEM-DEM construction which was introduced as part of the NaCl library by Bernstein et al. It essentially provides three algorithms:

  • gen() to generate a public/private key pair
  • enc(pk,sk,n,p) to encrypt a plaintext p under a symmetric key k, where k :=pk^sk using nonce n.
  • dec(sk,pk,n,c) to decrypt a ciphertext c a symmetric key k, where k :=pk^sk using nonce n.

(TODO: While cryptobox is the composition of a concrete DH-scheme and a concrete AE-scheme, our proof is valid for any composition of the two (given that both assumptions hold.))

We use the security notion PKAE as introduced earlier and reduce the PKAE security of cryptobox to that of Oracle-Diffie-Hellman (ODH) and Authenticated Encryption ($AE). We thus first introduce the PKAE^0 and PKAE^1 packages in the file Setoids.Crypto.PKAE.fst. Both packages operate on packages state, which consists of an encryption/decryption log and a log that maps public keys to private keys and both packages provide the same GEN oracle implemented in the function pkae_gen. The packages also implement the oracles ENC and DEC, implemented as pkae0_enc and pkae1_enc, as well as pkae0_dec and pkae1_dec respectively. We then use these functions and the labels GEN, ENC and DEC to instantiate the two signature that both packages share pkae_sig. We then instantiate the two packages as pkae0_functor and pkae1_functor. The goal is to show that we can instantiate an eq type with the two packages and some epsilon eps.

Before we build the reduction, we first introduce our two assumptions $AE and ODH. Both are relatively straight forward and can be found in files Setoids.Crypto.AE.fst and Setoids.Crypto.ODH.fst. Both packages rely on yet another set of packages called KEY^0 and KEY^1. Both packages provide oracles SET and CSET to set keys, as well as oracles GET and HON to read keys (indexed by handles) and their honesty. For KEY^0, SET sets the keys passed as input, where for KEY^1, SET sets random keys of the same length.

ODH allows the adversary to generate DH shares using the GENDH oracle (implemented as gen_dh) and use the ODH oracle (implemented as odh) to compute symmetric keys from two shares, where one share has to be present in the internal key log. The ODH oracle calls the SET oracle of the KEY package to store its keys. The assumption is that ODH composed with KEY^0 (implemented as odh_game0) is indistinguishable from ODH composed with KEY^1 (implemented as odh_game1). We express this assumption using the assume qualifier provided by F* as follows:

assume val odh_assumption : n:u32 -> os:odh_scheme n -> eq (odh_rel n) (odh_eps n) (odh_game0 n os) (odh_game1 n os)

where n is the key length (or share length).

We then instantiate the $AE assumption by composing an AE package with a KEY^1 package, such that ENC (enc0/enc1) and DEC (dec0/dec1) call the GET and HON oracles to obtain keys and decide if the should idealize a ciphertext for a given key handle. The composed packages are implemented as ae_game0 and ae_game1.

Finally, we conduct our proof in the file Setoids.Crypto.Proof.fst, where we first implement our reduction package (TODO: Currently it's confusingly named pkae). The reduction implements the same oracles as the PKAE package, but instead of calling the gen/enc/dec algorithms provided by cryptobox, it "implements" cryptobox using the oracles GENDH/ODH provided by the ODH package and the ENC/DEC oracles provided by the AE package. We then prove that the reduction composed with (ODH|AE^0)oKEY^0 is equivalent to PKAE^0 and similarly that (ODH|AE^1)oKEY^0 is equivalent to PKAE^1 (i.e. "simulation correctness") by proving that the oracles are equivalent.

(TODO: We currently do this at the very end of the proof. It would probably be better to do it up front.)

let pkae_eq_proof (n:u32) (aes:ae_scheme n) (os:odh_scheme n)
  =
    Perfect #_ #_ #(pkae_rel n os aes) (pkae0_composition n aes os) (MONPKAE.pkae0_functor n (pkaes n os aes)) (
      pkae_gen_eq n os aes /\
      pkae_enc_eq n os aes /\
      pkae_dec_eq n os aes
    )

We then use the algebra implemented by the eq type, as well as our assumptions that we can do a series of game-hops, which ultimately give us an instantiation of

eq (pkae_rel n os aes)
      (eps_sum2 n os aes)
      (pkae0_composition n aes os)
      (pkae1_composition n aes os)

The detailed series of proof steps are documented as inline-comments in the code. (TODO: The two proof steps (game-hops and simulation correctness) are currently not linked in the proof. This is still to be done as the final step of the proof.)

Current state of the project

We have an example proof for the protocol Cryptobox, which is part of the NaCl library. The proof is fairly complete, however, F* struggles when composing packages. Creating a package that has an empty input signature works fine. However, when trying to create a functor, i.e. a package that is composed of two sequentially composed packages (even trivial ones) F* endlessly tries to verify that the relations specified in the signature hold, but ultimately gives up with a simple error message, stating that it could not verify some (undefined) relational property.

Add a custom footer
Add a custom sidebar
Clone this wiki locally