Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
 14 Citations
 800 Downloads
Abstract
This paper presents a shallow embedding of a probabilistic functional programming language in higher order logic. The language features monadic sequencing, recursion, random sampling, failures and failure handling, and blackbox access to oracles. Oracles are probabilistic functions which maintain hidden state between different invocations. To that end, we propose generative probabilistic systems as the semantic domain in which the operators of the language are defined. We prove that these operators are parametric and derive a relational program logic for reasoning about programs from parametricity. Several examples demonstrate that our language is suitable for conducting cryptographic proofs.
1 Introduction
As cryptographic algorithms and protocols are becoming increasingly complicated, flaws in their security proofs are more likely to be overlooked. So, security vulnerabilities can remain undiscovered. The game playing technique [16, 29, 48] helps in structuring such proofs and can thus increase the level of confidence in their correctness. In this view, security notions are expressed as programs (called games) in the same language as the cryptographic algorithms and protocols. The proof then consists of transforming the program in several small steps until the desired properties obviously hold. To achieve high assurance, several frameworks [8, 14, 42] and a proof assistant [13] offer machine support in formalising algorithms and security notions and in checking such sequences of game transformations. This way, many cryptographic constructions have been mechanically proven secure, e.g., [6, 7, 43].
For security protocols such as TLS, Kerberos, and IPSec, only few mechanised security proofs in the computational model are available, e.g., [18, 21]. Instead, symbolic analysis tools [4, 19, 39, 47] dominate. They model protocol messages as terms in an algebra rather than bitstrings and assume that cryptography is perfect. Computational soundness (CS) results [1, 9, 25] bridge the gap between symbolic and computational models, but to our knowledge, they have never been mechanically checked. Yet, mechanising them is desirable for three reasons. First, the proofs are extremely technical with many case distinctions. A proof assistant can check that all cases are covered and no assumption is forgotten (as has happened in early CS works), and it provides automation for dealing with the easy cases. Second, computational soundness results need to be formalised only once per set of cryptographic primitives, not for every protocol to which the symbolic analyser is applied. That is, one mechanised proof yields trustworthy proofs for a whole class of protocols. Third, mechanisation supports the evolution of models and proofs. If a primitive is added or an assumption weakened as in [10], the proof assistant checks the proofs again and pinpoints where adaptations are needed.
Unfortunately, the existing frameworks are not suitable for formalising CS proofs. CertiCrypt [14] and Verypto [8] formalise stateful languages in the proof assistants Coq and Isabelle, respectively. Due to the deep embedding, program transformations always require a proof about the semantics and programs cannot easily reuse the existing libraries of the proof assistants. Therefore, formalising cryptographic arguments requires a very substantial effort. CertiCrypt’s successor EasyCrypt [13] provides much better automation using SMT solvers. Its logical foundation is higher order logic (HOL), but the reasoning infrastructure focuses on proofs in relational Hoare logic. However, substantial parts of CS proofs reason about the term algebra of the symbolic model for which EasyCrypt provides no support at all. The foundational cryptography framework (FCF) [42] alleviates CertiCrypt’s formalisation burden by taking a semishallow approach in Coq. For pure deterministic functions, the framework reuses the language of the logic; only probabilistic effects and interaction with oracles are modelled syntactically as monads. This saves considerable effort in comparison to CertiCrypt. Yet, the monadic language lacks features such as recursion and exceptions, which are desirable for CS, e.g., to implement probabilistic serialisers and parsers.
Contributions. We present a framework for cryptographic proofs formalised in higher order logic. It consists of a probabilistic functional programming language and a logic for reasoning about programs and probabilities. The language features monadic sequencing, recursion, random sampling, failures and their handling, and blackbox access to oracles. Oracles are probabilistic functions that maintain hidden state between different invocations. We model the language shallowly, i.e., we define the operators directly in the semantic domain. Programs which need no access to oracles are interpreted in the monad of discrete subprobabilities (Sect. 2.2); recursive functions are defined in terms of a least fixpoint operator (Sect. 2.3). For programs with oracle access, we propose generative probabilistic systems as semantic domain, which supports corecursive definitions (Sect. 3.2). In particular, we define operators for composing programs with oracles and other programs. We have implemented the framework in the proof assistant Isabelle/HOL [41], but it could be formalised in any other HOLbased prover, too.
The shallow embedding offers three benefits. First, we can reuse all the existing infrastructure of the proof assistant, such as name binding, higherorder unification and the module system, but also definitional packages and existing libraries. Second, we obtain a rich equational theory directly on programs, i.e., without any intervening interpretation function. Equality is important as we can replace terms by equal terms in any context (by HOL’s substitution rule), i.e., there is no need for congruences. Consequently, proof automation can use the (conditional) equations directly for rewriting. Although no syntax is formalised in the logic, programs are still written as HOL terms. This suffices to guide syntaxdirected proof tactics. Third, the language is not restricted to a fixed set of primitives. New operators can be defined in the semantic domain at any time.
Beyond equality, we provide a relational logic for reasoning about programs (Sects. 2.4 and 3.3). Relational parametricity [44, 50] has been our guide in that most rules follow from the fact that the operators are parametric. In particular, we demonstrate that several common reasoning principles in cryptographic proofs follow from parametricity. This approach ensures soundness of the logic by construction and can also guide the discovery of proof rules for new operators. Our logic is similar to those of the other tools. The novelty is that we follow a principled way in finding the rules and establishing soundness.
Three examples demonstrate that our framework is suitable for cryptographic proofs. We proved indistinguishability under chosen plaintext attacks (INDCPA) for (i) Elgamal publickey encryption [27] in the standard model (Sects. 2.1 and 2.5), (ii) Hashed Elgamal encryption in the random oracle model (Sects. 3.1 and 3.4), and (iii) an encryption scheme based on pseudorandom functions [42]. The examples have been chosen to enable comparisons with the existing frameworks (see Sect. 4). They show that our framework leads to concise proofs with the level of proof automation being comparable to EasyCrypt’s, the current state of the art. This indicates that the framework scales to computational soundness results, although our examples are much simpler. Indeed, we have just started formalising a CS result, so this is only a first step. The framework and all examples and proofs have been formalised in Isabelle/HOL and are available online [37].
Preliminaries: HOL Notation. The metalanguage HOL mostly uses everyday mathematical notation. Here, we present basic nonstandard notation and a few types with their operations; further concepts will be introduced when needed.
HOL terms are simply typed lambda terms with letpolymorphism (we use Greek letters Open image in new window for type variables). Types include in particular the type of truth values Open image in new window and the singleton type Open image in new window with its only element Open image in new window and the space of total functions Open image in new window . Type constructors are normally written postfix, e.g., Open image in new window denotes the type of finite lists of booleans, i.e., bitstrings. The notation Open image in new window means that the HOL term Open image in new window has type Open image in new window .
Pairs (type Open image in new window ) come with two projection functions Open image in new window and Open image in new window , and the map function Open image in new window . Tuples are identified with pairs nested to the right, i.e., Open image in new window is identical to Open image in new window and Open image in new window to Open image in new window . Dually, Open image in new window denotes the disjoint sum of Open image in new window and Open image in new window ; the injections are Open image in new window and Open image in new window . Case distinctions on freely generated types use guardlike syntax. The map function Open image in new window for disjoint sums, e.g., pattern matches on Open image in new window to apply the appropriate function: Open image in new window .
Sets (type Open image in new window ) are isomorphic to predicates (type Open image in new window ) via the bijections membership Open image in new window and set comprehension Open image in new window ; the empty set is Open image in new window . Binary relations are sets of pairs and written infix, i.e., Open image in new window denotes Open image in new window . The relators Open image in new window and Open image in new window lift relations componentwise to pairs and sums.
The datatype Open image in new window corresponds to the Haskell type Maybe. It adjoins a new element Open image in new window to Open image in new window , all existing values in Open image in new window are prefixed by Open image in new window . Maps (partial functions) are modelled as functions of type Open image in new window , where Open image in new window represents undefinedness and Open image in new window means that Open image in new window maps Open image in new window to Open image in new window . The empty map Open image in new window is undefined everywhere. Map update is defined as follows: Open image in new window .
2 A Shallow Probabilistic Functional Language
Security notions in the computation model are expressed as games parametrised by an adversary. In formalising such games, we want to leverage as much of the prover’s infrastructure as possible. Therefore, we only model explicitly what cannot be expressed in the prover’s term language, namely probabilities and access to oracles. In this section, we focus on probabilities and show the framework in action on the example of Elgamal encryption (Sects. 2.1 and 2.5).
We model games as functions which return a discrete (sub)probability distribution over outcomes. Discrete subprobabilities strike a balance between expressiveness and ease of use. They provide a monadic structure for sequencing and failure (Sect. 2.2). Thus, games can be formulated naturally and control may be transferred nonlocally in error cases such as invalid data produced by the adversary. They also host a fixpoint operator for defining recursive functions (Sect. 2.3). In contrast, measuretheoretic (sub)probability distributions clutter proofs with measurability requirements. For computational soundness, discrete subprobability distributions suffice. In Sect. 2.4, we prove that the operators are relationally parametric and derive a programming logic and common cryptographic reasoning principles from parametricity.
2.1 Example: Elgamal Encryption
In this section, we formalise Elgamal’s encryption scheme [27] to motivate the features of our language. In Sect. 2.5, we prove the scheme INDCPA secure under the decisional DiffieHellman (DDH) assumption. We formally introduce the language only in Sect. 2.2. For now, an intuitive understanding sufficFes: monadic sequencing is written in Haskellstyle do notation and Open image in new window samples Open image in new window as a random element from the finite set Open image in new window .
Elgamal’s encryption scheme produces ciphertexts that are indistinguishable under chosen plaintext attacks. Chosen plaintext attacks are formalised as the game Open image in new window shown in Fig. 1c. An INDCPA adversary Open image in new window consists of two probabilistic functions Open image in new window and Open image in new window . Given a public key Open image in new window , Open image in new window chooses two plaintexts Open image in new window and Open image in new window . The game then encrypts one of them as determined by the random bit Open image in new window (a coin flip) and gives the challenge ciphertext Open image in new window to Open image in new window and any arbitrary state information Open image in new window produced by Open image in new window . Then, Open image in new window produces a guess which of the two messages Open image in new window decrypts to. Indistinguishability requires that the adversary cannot do significantly better than flipping a coin. This is measured by the INDCPA advantage given by Open image in new window . A concrete security theorem bounds the advantage by a quantity which is known or assumed to be small.
If any step in the game fails, Open image in new window behaves like a fair coin flip, i.e., the advantage is Open image in new window in that case. This happens, e.g., if the plaintexts are invalid, i.e., not elements of the group, or the adversary does not produce plaintexts or a guess at all. (In an implementation, the latter could be detected using timeouts.)
2.2 The Monad of Discrete Subprobability Distributions
A discrete subprobability distribution is given by its subprobability mass function (spmf), i.e., a nonnegative realvalued function which sums up to at most 1. We define the type Open image in new window of all spmfs^{1} over elementary events of type Open image in new window and use variables Open image in new window , Open image in new window for spmfs. We make applications of spmfs explicit using the operator Open image in new window . So, Open image in new window denotes the subprobability mass that the spmf Open image in new window assigns to the elementary event Open image in new window . An event Open image in new window is a set of elementary events; its subprobability Open image in new window is given by Open image in new window . Moreover, the weight Open image in new window of Open image in new window is the total probability mass assigned by Open image in new window , i.e., Open image in new window . If Open image in new window is a probability distribution, i.e., Open image in new window , then we call Open image in new window lossless following [14] (notation Open image in new window ). The support Open image in new window is countable by construction.
Here, Open image in new window scales the subprobability masses of Open image in new window by Open image in new window , i.e., \(\mathsf{scale}~r~p!x=r\,\cdot \) (p!x) for Open image in new window . In particular, if Open image in new window is lossless, then Open image in new window . The monad operations give rise to the functorial action \(\mathsf{map}_\mathsf{spmf}{:}{:}(\alpha \Rightarrow \beta )\Rightarrow \alpha \) Open image in new window given by Open image in new window .
For example, the Bernoulli distribution Open image in new window , which returns Open image in new window with probability Open image in new window for any Open image in new window , can be sampled from fair coin flips as shown on the right [32]. It can be used to define probabilistic choice.
Moreover, the subprobability monad contains a failure element, namely Open image in new window . Failure aborts the current part of the program, as Open image in new window propagates: Open image in new window . However, we hardly use Open image in new window in programs directly. It is more natural to define an assertion statement Open image in new window . Assertions are useful in validating the inputs received from the adversary. For example, the assertion in the INDCPA security game in Fig. 1c checks that the adversary Open image in new window produced valid plaintexts.
This completes the exposition of the language primitives except for the fixpoint combinator (see Sect. 2.3). They suffice for all examples in this paper, but note that we are not restricted to this set of operations. If necessary, users can define their own discrete subprobability distribution on the spot thanks to the shallow embedding. Also remember that all the equation in this section are equalities inside the logic. Hence, we can use them for rewriting in any context, not just under a semantics interpretation as with a deep embedding.
2.3 Recursive Functions in the SPMF Monad
In this section, we consider the denotation of recursive functions in the spmf monad. As usual in programming languages, we interpret a recursive specification as the least fixpoint of the associated functional. In the case of spmf, the approximation order Open image in new window is given by Open image in new window [5]. In this order, every chain Open image in new window has a least upper bound (lub) Open image in new window which is taken pointwise: Open image in new window where Open image in new window denotes the supremum of a bounded set Open image in new window of real numbers. Thus, the approximation order is a chaincomplete partial order (ccpo) with least element Open image in new window (see Proposition 1 below).
By Tarski’s fixpoint theorem, every monotone function Open image in new window on a ccpo has a least fixpoint Open image in new window , which is obtained by the least upper bound of the transfinite iteration of Open image in new window starting at the least element. Therefore, we can define recursive functions as the least fixpoint of the associated (monotone) functional.
Using Isabelle’s package for recursive monadic function definitions [34], we hide the internal construction via fixpoints from the user and automate the monotonicity proof. For example, the function Open image in new window can be specified exactly as shown in Fig. 2. The monotonicity proof succeeds as Open image in new window is monotone in both arguments. Namely, if Open image in new window and Open image in new window for all Open image in new window , then Open image in new window . In contrast, Open image in new window is monotone only in the second argument, but not in the first. For example, Open image in new window , but Open image in new window Open image in new window . Therefore, recursion is always possible through Open image in new window and Open image in new window , but not in general through Open image in new window .
Proposition 1
The approximation order Open image in new window is a chaincomplete partial order.
Proof
We have to show that Open image in new window is a partial order and that Open image in new window is welldefined and the least upper bound for every chain Open image in new window , i.e., every set of spmfs all of whose elements are comparable in Open image in new window . The difficult part is to show that Open image in new window is welldefined. In particular, we must show that the support of Open image in new window is countable even if Open image in new window is uncountable. Then, it is not hard to see that Open image in new window sums up to at most 1.
Clearly, we have Open image in new window . Yet, the union of an uncountable sequence of increasing countable sets need not be countable in general. In the following, we show that even for uncountable chains Open image in new window of spmfs, the union of the supports remains countable. To that end, we identify a countable subsequence of Open image in new window whose lub has the same support. The key idea is that for Open image in new window comparable spmfs Open image in new window and Open image in new window , the order can be decided by looking only at the assigned probability masses, namely, Open image in new window iff Open image in new window . So suppose without loss of generality that Open image in new window does not contain a maximal element (otherwise, the lub is the maximal element and we are done). The set of assigned probability masses Open image in new window has a supemum Open image in new window , as Open image in new window bounds the set from above. The closure of Open image in new window contains the supremum Open image in new window , so Open image in new window must contain a countable increasing sequence which converges to Open image in new window . This sequence gives rise to a countable subsequence Open image in new window of Open image in new window , for which we show Open image in new window . For any Open image in new window , there is a Open image in new window such that Open image in new window , as the assigned probability masses in Open image in new window converge to Open image in new window from below and Open image in new window is not maximal. Hence, Open image in new window as Open image in new window and Open image in new window are related in Open image in new window , and therefore Open image in new window as Open image in new window is monotone.
Overall, arbitrary chains and transfinite iteration are superior to ordinary fixpoint iteration in two ways. First, our fixpoint combinator can handle more functions, i.e., we can accept more recursive specifications. Second, the proof obligations that recursive specifications incur are simpler: monotonicity is usually easier to show than continuity.
2.4 Lifting and Parametricity
Game playing proofs transform games step by step. In each step, we have to bound the probability that the adversary can distinguish the original game from the transformed one. For some transformations, the equational theory suffices to prove the games equal—then, the probability is 0. Other transformations are justified by cryptographic assumptions. To bound the probability in such cases, our framework provides a relational logic for programs.
To that end, we first define an operation to lift relations over elementary events to relations over spmfs. With this lifting operator, our primitive operations are parametric. Then, we can derive the logic from parametricity.
Lifting. The lifting operation Open image in new window transforms a binary relation R over elementary events into a relation over spmfs over these events. For lossless distributions, a number of definitions have appeared in the literature. We generalise the one from [30] as the relator associated with the natural transformation Open image in new window [45]. Formally, Open image in new window relates the spmfs Open image in new window and Open image in new window iff there is an spmf Open image in new window such that (i) Open image in new window , (ii) Open image in new window , and (iii) Open image in new window , We call w a Rjoint spmf of p and q.
This definition reformulates the one by Larsen and Skou [36] for lossless spmfs. They consider w as a nonnegative weight function on the relation such that the marginals are the original distribution., i.e., w must satisfy (i) Open image in new window whenever Open image in new window , (ii) Open image in new window for all x, and (iii) Open image in new window for all y, Using the functorial structure of spmfs, our definition expresses the same conditions more abstractly without summations. In previous work [30], this led to considerably shorter proofs.
Lemma 1
(Characterisation of \({{{\mathbf {\mathsf{{rel}}}}}_{{\varvec{\mathsf{{ spmf}}}}}}\) ).
The following are equivalent for all R, p, and q.
 (a)
 (b)
Open image in new window and Open image in new window and Open image in new window for some w
 (c)
Open image in new window for all A and Open image in new window
The relator enjoys a number of useful properties. For example, (i) it generalises equality, namely Open image in new window , (ii) it distributes over relation composition, and (iii) it is monotone: Open image in new window implies Open image in new window if Open image in new window whenever Open image in new window and Open image in new window and Open image in new window .
Parametricity. The program logic describes the interaction between the spmf operations and the relator. As it turns out, relational parametricity [44, 50] helps us to find the rules and prove them sound.^{2}
Parametricity expresses that a polymorphic function does not inspect the values of type variables, but works uniformly for all instances. Relational parametricity formalises this as follows. Types are interpreted as relations and type constructors as relation transformers. A polymorphic function is (relationally) parametric iff it is related to itself in its type’s relation where type variables are interpreted as arbitrary relations. For spmfs, the relator Open image in new window is the appropriate relation transformers. For example, parametricity for Open image in new window is expressed as Open image in new window for all Open image in new window . Here, the relator Open image in new window for the function space relates two functions f and g iff they transform relatedness in R into relatedness in S, i.e., Open image in new window implies Open image in new window for all x and y.
As function application preserves parametricity, any combination of parametric functions is parametric, too. For example, parametricity of Open image in new window and Open image in new window follows. Similarly, Open image in new window is parametric, too. Thus, this extends to whole probabilistic programs, which we will exploit in Sect. 3.4. Such parametricity proofs are highly automated in Isabelle [31, 35].
For example, this rule plays an important role in Bellare’s and Rogaway’s fundamental lemma [16]. Lacking syntax, we cannot express their syntactic condition in HOL. Borrowing ideas from EasyCrypt [13], we instead rephrase the condition in terms of the relator.
Lemma 2
Optimistic sampling and the fundamental lemma have illustrated how cryptographic arguments follow from parametricity. But parametricity offers yet another point of view. Mitchell [40] uses parametricity to express representation independence, i.e., one can change the representation of data without affecting the overall result. In Sect. 3.4, we will exploit representation independence in the bridging steps of the game transformations.
The Fixpoint Combinator We have not yet covered one important building block of our probabilistic language in our analysis: the fixpoint combinator on spmfs. It turns out that it preserves parametricity.^{3}
Theorem 1
(Parametricity of spmf fixpoints).
If Open image in new window and Open image in new window are monotone w.r.t. Open image in new window and Open image in new window , then Open image in new window .
To avoid higherkinded types, the theorem generalises parametricity to the preservation of relatedness. In the typical use case, f and g are instances of the same polymorphic function.
We prove Theorem 1 by parallel induction on the two fixpoints. Both inductive cases are trivial. The base case requires Open image in new window to be strict, i.e., it relates the least elements, which holds trivially. The step case is precisely the relatedness condition of f and g which the theorem assumes. The hard part consists of showing that parallel induction is a valid proof principle. To that end, we must show that Open image in new window is admissible. A relation Open image in new window is admissible w.r.t. two ccpos iff for any chain Open image in new window of pairs in the product ccpo (the ordering is componentwise), R relates the componentwise lubs of Y.
Proposition 2
Open image in new window is admissible.
Proof
Note that it is not clear how to prove admissibility via the characterisation in terms of joint spmfs. The issue is that the joint spmfs for the pairs in the chain need not form a chain themselves. So we cannot construct the joint spmf for the lubs as the lub of the joint spmfs.
Admissibility of relators is preserved by the function space (ordered pointwise) and products (ordered componentwise). Thus, analogues to Theorem 1 hold for fixpoints over Open image in new window , etc. They are useful to show parametricity of (mutually) recursive probabilistic functions (Sect. 3.3) rather than recursively defined spmfs.
2.5 Security of Elgamal Encryption
The proof consists of two steps. First, observe that Open image in new window Open image in new window , because after the definitions have been unfolded, both sides are the same except for associativity and commutativity of Open image in new window and the group law Open image in new window . Second, we show that Open image in new window . Note that the message m is independent of Open image in new window , which is sampled uniformly. Multiplication with a fixed group element m is a bijection on the carrier. By (4), we can omit the multiplication and the guess b’ becomes independent of b. Hence, the adversary has to guess a random bit, which is equivalent to flipping a coin.
Formally, the second proof is broken up into three step. First, we rewrite the game using the identities about Open image in new window , and Open image in new window such that we can apply (4) on the multiplication. Second, we rewrite the resulting game such that we can apply (4) once more on the equality test. Finally, we show that the irrelevant assignments cancel out. This holds even if the adversary is not lossless thanks to the surrounding Open image in new window . Thus, our statement does not need any technical side condition like losslessness of the adversary in CertiCrypt [14] and EasyCrypt [13].
Modules. Note that the definition of INDCPA security does not depend on the Elgamal encryption scheme. In the formalisation, we abstract over the encryption scheme using Isabelle’s module system [11]. Like an MLstyle functor, the INDCPA module takes an encryption scheme and specialises the definitions of game and advantage and the proven theorems to the scheme. Similarly, the DDH assumption has its own module which takes the group as argument. This allows to reuse security definitions and cryptographic algorithms in different contexts. For Elgamal, we import the DDH module for the given group and the INDCPA module for the Elgamal encryption scheme.
3 Adversaries with Oracle Access
In many security games, the adversary is granted blackbox access to oracles. An oracle is a probabilistic function which maintains mutable state across different invocations, but the adversary must not get access to this state. In this section, we propose a new semantic domain for probabilistic functions with oracle access (Sect. 3.2). Like in Sect. 2.4, we derive reasoning rules from parametricity and explore the connection to bisimulations (Sect. 3.3). We motivate and illustrate the key features by formalising a hashed version of Elgamal encryption (HEG) in the random oracle model (ROM) [15] (Sect. 3.1) and verifying its security under the computational DiffieHellman (CDH) assumption (Sect. 3.4).
3.1 Example: Hashed Elgamal Encryption
In Sect. 3.4, we prove that HEG is INDCPA secure under the computational Diffie Hellman (CDH) assumption. For now, we explain how the formalisation changes. Figure 4c shows the new game for chosen plaintext attacks where the key generation algorithm, the encryption function and the adversary have access to an oracle. In comparison to Fig. 1c, the monad has changed: the game uses the new monad of generative probabilistic values (gpv) rather than spmf; see Sect. 3.2 for details. Accordingly, the coin flips Open image in new window are embedded with the monad homomorphism Open image in new window .
In one step of the security proof, we will have to keep track of the calls that the adversary has made. This is achieved by using the oracle transformation Open image in new window in Fig. 4b. It forwards all calls x and records them in its local state X.
As before, all these definitions live in different modules that abstract over the encryption scheme, group, and oracle. In fact, the programs in Fig. 4 are completely independent of the concrete oracle. We compose the game with the oracle only when we define the advantage. Thus, it now depends on an oracle Open image in new window with initial state Open image in new window . Here, Open image in new window binds the oracle calls in Open image in new window to the oracle Open image in new window . It thus reduces a program with oracle access to one without, i.e., a spmf.
3.2 Generative Probabilistic Values
The example from the previous section determines a wish list of features for the language of probabilistic programs with oracle access: assertions and failure handling, calls to unspecified oracles, embedding of probabilistic programs without oracle access, and composition operators. In this section, we propose a semantic domain for probabilistic computations with oracle access and show how to express the above features in this domain.
We start by discussing why spmfs do not suffice. In our probabilistic language of spmfs, we can model an oracle as a function of type Open image in new window , which takes a state and the arguments of the call and returns a subprobability distribution over the output and the new state. Unfortunately, we cannot model the adversary as a probabilistic program parametrised over the oracle and its initial state. Suppose we do. Then, its type has the shape Open image in new window . To hide the oracle state from the adversary despite passing it as an argument, we could require that the adversary be parametric in Open image in new window . This expresses that the adversary behaves uniformly for all states, so it cannot inspect the state. Yet, we must also ensure that the adversary uses the state only linearly, i.e., it does not call the oracle twice with the same state. As we are not aware of a semantic characterisation of linearity, we cannot model the adversary like this.
As we are interested in a shallow embedding, the type Open image in new window only models the observations (termination with result or failure and interaction with the environment) of the system rather than the whole system with the states. This yields a richer equational theory, i.e., we can prove more properties by rewriting without resorting to bisimulation arguments. Any probabilistic system with explicit states can be transformed into a gpv by identifying bisimilar states. The coiterator Open image in new window formalises this: given a probabilistic system and an initial state, it constructs the corresponding gpv.
Composition Operators. Two gpvs can be composed such that one (the callee) processes all the calls of the other (the caller). Thereby, the callee may issue further calls. In games, composition is mainly used to intercept and redirect the oracle calls of the adversary, i.e., the callee is an oracle transformation like Open image in new window . Syntactically, composition corresponds to inlining the callee into the caller. If programs were modelled syntactically, implementing inlining would be trivial; but with a shallow approach, we cannot rely on syntax.
The function Open image in new window recursively goes through the interactions between the caller and the callee. If the caller terminates with result x, there are no calls and the search terminates. Otherwise, the caller issues a call a and becomes the rpv r. In that case, Open image in new window analyses the callee under the argument a. If the callee returns b without issuing a call itself, the search continues recursively on r b. Otherwise, the first call is found and the search terminates.
Reductions are the primary use case for composition. They transform the adversary Open image in new window for one game into an adversary for another game. In general, the oracles of the two games differ. So, the reduction emulates the original oracle Open image in new window using an oracle transformation T, which has access to the new oracle Open image in new window . In this view, the new adversary is built from the composition Open image in new window and the cryptographic assumption executes it with access to Open image in new window . By associativity of composition (see Fig. 7), this is equivalent to executing the original adversary Open image in new window with access to the emulated oracle Open image in new window . Thus, it suffices to establish that the emulation Open image in new window of Open image in new window is good enough.
3.3 Parametricity and Bisimulation
There are also limits to what we can derive from parametricity. For example, consider the case where only one of the oracles enters an error state, say because the adversary has guessed a secret. Then, the adversary can distinguish between the oracles and behave differently, i.e., it is not related by Open image in new window any more. Therefore, we would need a notion of bisimulation up to error, but relational parametricity cannot express this. Thus, we prove the Lemma 3 directly.
Lemma 3

Open image in new window , and

Open image in new window and Open image in new window are lossless in error states and error states are never left, and

v issues finitely many calls and never fails, i.e., all spmfs in v are lossless.
3.4 Security of Hashed Elgamal Encryption
Now, we illustrate how our framework supports proofs about games with oracles by reducing the INDCPA security of Hashed Elgamal encryption to the computational DiffieHellman (CDH) assumption. The CDH assumption states that it is hard to compute Open image in new window given Open image in new window and Open image in new window . For comparison with the existing proofs in Certicrypt [14] and EasyCrypt [13] (Sect. 4), we reduce the security to the set version LCDH of CDH, where the adversary may return a finite set of candidates for Open image in new window . The reduction from LCDH to CDH is straightforward.
In the random oracle model [15], hash functions are idealised as random functions. The random oracle Open image in new window shown in Fig. 9 implements such a random function. Its state Open image in new window is a map from group elements (inputs) to bitstrings (outputs), which associates previous queries with the outputs. Upon each call, the oracle looks up the input x in the map Open image in new window and returns the corresponding output if found. If not, it returns a fresh bitstring bs of length n and updates the map Open image in new window to associate x with bs.
The security of HEG is shown by a sequence of game transformations. They closely follow [13], so we do not present them in detail here. Instead, we focus on some steps to highlight the use of parametricity, equational reasoning, and the program logic. In the following, we assume a fixed INDCPA adversary Open image in new window which makes only finitely many calls and does not fail. This technical restriction is necessary to apply Lemma 3.
The first step changes the game such that it records the adversary’s queries to the hash oracle using the oracle transformation Open image in new window from Fig. 4b. So the first game Open image in new window is the same as Open image in new window from Fig. 4c except that the calls to the adversary are replaced by Open image in new window and Open image in new window . The equality Open image in new window follows from parametricity and bisimilarity of Open image in new window and the identity oracle transformation Open image in new window due to representation independence, and the fact that Open image in new window is the identity for gpv composition. The bisimulation relation Open image in new window identifies all states. The equality is proven automatically by Isabelle’s prover for representation independence [31] using the transfer rules Open image in new window and Open image in new window and equational rewriting. In fact, the latter rule is another instance of representation independence, as the two oracle transformations differ only in the update of the local state. The transfer rule Open image in new window formalises the connection. The parametricity prover derives the transfer rule for the oracles from this.
The third transformation replaces the hash for the challenge ciphertext with a random bitstring which is not recorded in the hash oracle’s map. By the fundamental lemma, the difference in the success probabilities is bounded by the error event, which is in this case the flag introduced in Open image in new window . The assumption of the fundamental lemma is proven using the rules of the program logic. In particular, we apply Lemma 3 on the call to Open image in new window , as the oracles are not bisimilar if any of the remaining queries calls the hash function on Open image in new window .
4 Comparison with Existing Frameworks
In this section, we compare our framework with the existing tools CertiCrypt [14], EasyCrypt [13], FCF [42], and Verypto [8] in four respects: readability, expressiveness, the trusted codebase, and the formalisation effort.
Readability is important for two reasons. First, security definitions should resemble those in the cryptographic literature such that cryptographers are able to understand and evaluate them. Second, intuitive syntax supports the users during the formalisation, as they can focus on formalising the arguments rather than trying to understand hardly readable programs. All frameworks achieve good readability, but in different ways. CertiCrypt and EasyCrypt embed an imperative procedural language in their logics. They closely model Bellare’s and Rogaway’s idea of a stateful language with oracles as procedures [16]. Verypto deeply embeds a higher order language with mutable references based on de Bruijn indices in HOL. Readability is regained by reflecting the syntax in HOL’s term language using parsing and prettyprinting tricks. In contrast, FCF and our framework shallowly embed a functional language with monadic sequencing in Coq and Isabelle/HOL, respectively. Like in Shoup’s treatment [48], the state of the adversary and the oracles must be passed explicitly. This improves clarity as it makes explicit which party can access which parts of the state. Conversely, it can also be a source for errors, as it is the user who must ensure that the states be used linearly.
Expressiveness has two dimensions. First, the syntax and the semantic domain determine the expressiveness of the language. CertiCrypt and EasyCrypt support discrete subprobability distributions and a procedural while language, but no fixpoint operator, although fixpoints could be defined in CertiCrypt’s semantic domain similar to our work (Sect. 2.3 and Theorem 1). Fixpoints do not increase the expressiveness over a while combinator, but lead to more natural formulations of programs. EasyCrypt additionally provides a module system to support abstraction and reuse. Verypto is the most general framework, as it builds on measure theory and therefore supports continuous distributions and higher order functions—at the price of incurring measurability proof obligations. FCF’s semantics allows only probability distributions with finite support, so no fixpoint operator can be defined. The syntax further restricts probabilistic effects to random sampling of bitstrings and conditional probabilities. For programs with oracle access, FCF provides equivalents to our operations Open image in new window , and Open image in new window . Further effectful operators (such as Open image in new window cannot be added by the user, but require changes to the language formalisation itself. Conversely, FCF’s deterministic pure sublanguage includes all functions and types from the library of the proof assistant thanks to the shallow embedding. Abstraction and reuse come from Coq’s module system. Like FCF, our framework is integrated with the libraries and facilities of the proof assistant. It extends this advantage to probabilistic programs with oracle access, as we define also these languages directly in the semantic domain. Thus, users can define new control structures on the spot, if needed. It supports discrete subprobabilities similar to CertiCrypt and EasyCrypt and in addition features a fixpoint operator.
Second, the embedding and the logic determine what kind of security properties can be formalised. All frameworks support concrete security proofs. Thanks to the deep embedding, CertiCrypt and Verypto also support statements about efficiency and thus asymptotic security statements, which is impossible in EasyCrypt and ours, because HOL functions are extensional. FCF comes with an axiomatic cost model for efficiency, which is not formally connected to an operational model. This is possible despite the shallow embedding as long as extensionality is not assumed. In these three frameworks, asymptotic bounds are derived from concrete bounds. So no work is saved by reasoning asymptotically.
The trusted code base influences the trustworthiness of a mechanised proof and should be as small as possible. Proof assistants like Coq and Isabelle consist of a small kernel and can additionally produce proof terms or proof objects that an independent checker can certify. Consequently, CertiCrypt, FCF, and our framework achieve high ranks there. Verypto falls behind because its measure theory is only axiomatized rather than constructed definitionally. EasyCrypt does not have a small kernel, so the whole implementation in OCaml and the external SMT solvers must be trusted.
Framework comparison by line counts of concrete security theorems
As Petcher and Morrisett have already observed [43], shallow embeddings (FCF, ours) have an advantage over deep ones (CertiCrypt, Verypto), as all the reasoning infrastructure and libraries of the proof assistant can be reused directly; a deep embedding would need to encode the libraries in the syntax of the language. Despite being more general, our framework leads to shorter proofs than FCF. We see two reasons for this gap. First, our language works directly in the semantic domain, even for effectful programs. This gives a richer equational theory and all conversions between syntax and semantics become superfluous. For example, their rule for loop fission holds only in the relational logic, but it is a HOL equality in our model. Second, Isabelle’s builtin proof automation, in particularly conditional rewriting, provides a reasonable level of automation, especially for the equational proofs mentioned above. So far, we have not yet implemented any problemspecific proof tactics. Such tactics could automate the proofs even more, especially the manual reasoning with commutativity of sequencing. In comparison to EasyCrypt, the state of the art in proof automation, we achieve a similar degree of automation.
5 Further Related Work
In Sect. 4, we have already compared our framework with the existing ones for mechanising game playing proofs. In this section, we review further related work.
The tool CryptoVerif by Blanchet [20] can prove secrecy and correspondence properties such as authentication of security protocols. As it can even discover intermediate games itself, the tool achieves a much higher degree of automation than any of the frameworks including ours. The language—a process calculus inspired by the \(\pi \) calculus—distinguishes between a unique output process and possibly many input processes, which communicate via channels. Our gpvs also distinguish between inputs and outputs, but composition works differently. In CryptoVerif, several input processes may be able to receive an output and the semantics picks one uniformly randomly. In our setting, the callee represents all input processes and receives all calls. In principle, one could embed Blanchet’s calculus in our semantic domain of gpvs using a different composition operator. Then, CryptoVerif’s abstractions could be proven sound in our framework.
The functional programming language F\(^*\) [17, 49] has been used to verify implementations of cryptographic algorithms and protocols [12]. Security properties are formulated as type safety of an annotated, dependentlytyped program and the type checker ensures type safety. While this approach scales to larger applications [18], the security properties cannot be stated concisely as the typing assertions are scattered over the whole implementation.
Affeldt et al. [2] formalise pmfs in Coq and apply this to coding theory.
Audebaud and PaulinMohring [5] formalised the spmf monad in Coq. They also define the approximation order Open image in new window on spmfs and show that it forms an \(\omega \)complete partial order, i.e., countable chains have least upper bounds. Using Kleene’s fixpoint theorem, they obtain a fixpoint operator for continuous functions. We generalise their result in that arbitrary spmf chains have least upper bounds. Thus, monotonicity (rather than continuity) suffices for the fixpoints.
CertiCrypt [14] uses their monad as the semantic domain for programs and adds the lifting operator Open image in new window . Zanella Béguelin proves a special case of Theorem 1, where the functions f and g are projections of a joint continuous function [51].
Cock [24] develops a shallow embedding of a probabilistic guarded command language in HOL. Programs are interpreted as monotone transformers of bounded expectations, which form a complete lattice. So, recursive functions can be defined using fixpoints. He focuses on proving functional correctness properties using nonrelational Hoare triples and verification conditions.
Our framework reuses the existing infrastructure for relational parametricity in Isabelle/HOL, but in new ways. The Lifting package [31] exploits representation independence to transfer theorems between raw types and their quotients or subtypes. Lammich’s tool AutoRef [35] uses transfer rules to refine abstract datatypes and algorithms to executable code. Blanchette et al. [23] use parametricity to express wellformedness conditions for operators under which corecursion may appear in corecursive functions. In contrast, we derive a relational logic for reasoning about shallowly embedded programs from parametricity and apply representation independence to replace oracles in games by bisimilar ones.
6 Conclusion and Future Work
In this paper, we have integrated a language for monadic probabilistic functions with blackbox access to oracles in higher order logic. Several examples demonstrate that cryptographic algorithms and security definitions can be expressed in this language. A rich equational theory and a relational logic support the formalisation of cryptographic arguments. The definitions and proofs have been mechanised using the proof assistant Isabelle/HOL.
Although our logic is similar to those in FCF and EasyCrypt, our approach is different: we derive the rules in a principled way from parametricity of the operators. This approach can help in finding the appropriate rules when new operations are introduced, and in proving them sound. Petcher and Morrisett, e.g., add a monadic map operation to FCF’s language and an appropriate reasoning rule to their logic [43]. They show soundness for the rule by induction, which takes 22 proof steps. In our approach, their rule is an instance of parametricity of the map operator, which Isabelle’s parametricity prover can establish automatically.
This work is motivated by the goal of formalising computational soundness results. Whether our framework scales to such large applications is still an open question. In our cryptographic examples, it compares favourably to the state of the art. Indeed, our initial attempts in formalising the CoSP framework [9] are encouraging that our approach will work. Therefore, the next steps will focus on formalising these results and improving proof automation.
Our framework cannot express efficiency notions such as polynomial runtime yet. Hence, asymptotic reasoning, which dominates in CS proofs, can be used only in limited ways. This is the flipside of the shallow embedding: As HOL functions are extensional, we cannot exploit HOL syntax in the reasoning. It seems possible to adapt Petcher’s and Morrisett’s axiomatic cost model [42], but the benefits are not yet clear. A less axiomatic alternative is to formalise a small programming language, connect it to HOL’s functions and derive the bounds in terms of the operational semantics. Verypto [8] and the higherorder complexity analysis for Coq by Jouannaud and Xu [33] might be good starting points.
Beyond cryptographic arguments and computational soundness, our semantic domain of generative probabilistic values could be applied in different contexts. In previous work [38], we used a (less abstract) precursor to model interactive programs in HOL. The domain could also serve as a basis for formalising and verifying CryptoVerif or as a backend for the new EasyCrypt, as EasyCrypt’s logic and module system resemble Isabelle’s.
In this direction, it would be interesting to investigate whether gpvs admit a ccpo structure in which where the basic operations are monotone. Currently, corecursion and coinduction are available. The ccpo structure would allow us to additionally define functions recursively and use induction as proof principle. The problem is that limits must preserve discreteness of the subprobability distributions. It is not easy to move to arbitrary measuretheoretic distributions, as codatatypes in HOL require a cardinality bound on the functor through which they recurse; otherwise, they cannot be defined in HOL [28].
Footnotes
 1.
In the formalisation, we construct the type Open image in new window by combining the existing monad for probability mass functions [30] with an exception monad. This way, most of our primitive operations can be defined in terms of the primitive operations of the two monads. Hence, we can derive many of their properties, in particular parametricity (Sect. 2.4), from the latter’s.
 2.
As our embedding is shallow, we cannot define a deduction system in the logic. Rather, we derive the rules directly from the semantics, i.e., show soundness. Completeness is therefore achieved dynamically: new rules can be derived if necessary, in particular when a new operation is introduced.
 3.
Wadler showed that if all types are \(\omega \)ccpos, all functions are continuous and all relations are admissible and strict, then the fixpoint operator (defined by countable iteration) is parametric [50]. We do not consider the fixpoint operator as part of the language itself, but as a definition principle for recursive userspecified functions. That is, we assume that Open image in new window is always applied to a (monotone) function. Consequently, preservation of parametricity suffices and we do not need Wadler’s restrictions of the semantic domains. Instead, monotonicity (instead of continuity, see the discussion in Sect. 2.3) is expressed as a precondition on the given functions.
 4.
Note that Open image in new window is not the greatest fixpoint of a polynomial functor, as the recursion goes through the nonpolynomial functor Open image in new window . Still, the type is welldefined, as Open image in new window is a bounded natural functor [30] which Isabelle’s codatatype package supports [22].
 5.
The type constructor Open image in new window takes three type arguments, so we should expect Open image in new window to take three relations, too. However, the third argument occurs in a negative position in the codatatype definition. Therefore, the relator does not enjoy useful properties such as monotonicity and distributivity over relation composition. Consequently, Isabelle’s infrastructure for parametricity treats these arguments as fixed (dead in the terminology of [22]). So, Open image in new window takes only relations for the first two arguments and fixes the third to the identity relation Open image in new window as can be seen in (5). In practice, we have not found this specialisation to be restrictive.
 6.
In fact, parametricity actually yields a rule stronger than (6), namely the gpv v need not be the same on both sides. If Open image in new window and the premises of (6) hold, then Open image in new window .
 7.
The oracle transformation in this reduction is degenerate, as Open image in new window emulates the oracle without access to further oracles. Thus, we use Open image in new window directly instead of Open image in new window .
Notes
Acknowledgements
Johannes Hölzl helped us with formalising spmfs on top of his probability formalisation and with the proof of countable support of spmf chains. Christoph Sprenger and Dmitriy Traytel and the anonymous reviewers suggested improvements of the presentation and the examples. This work was supported by SNSF grant 153217 “Formalising Computational Soundness for Protocol Implementations”.
References
 1.Abadi, M., Rogaway, P.: Reconciling two views of cryptography (The computational soundness of formal encryption). J. Cryptology 15(2), 103–127 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
 2.Affeldt, R., Hagiwara, M., Sénizergues, J.: Formalization of Shannon’s theorems. J. Automat. Reason. 53(1), 63–103 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
 3.Aharoni, R., Berger, E., Georgakopoulos, A., Perlstein, A., Sprüssel, P.: The maxflow mincut theorem for countable networks. J. Combin. Theory Ser. B 101, 1–17 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
 4.Armando, A., et al.: The AVANTSSAR platform for the automated validation of trust and security of serviceoriented architectures. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 267–282. Springer, Heidelberg (2012)CrossRefGoogle Scholar
 5.Audebaud, P., PaulinMohring, C.: Proofs of randomized algorithms in Coq. Sci. Comput. Program. 74(8), 568–589 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
 6.Bacelar Almeida, J., Barbosa, M., Bangerter, E., Barthe, G., Krenn, S., Zanella Béguelin, S.: Full proof cryptography: verifiable compilation of efficient zeroknowledge protocols. In: CCS 2012, pp. 488–500. ACM (2012)Google Scholar
 7.Backes, M., Barthe, G., Berg, M., Grégoire, B., Kunz, C., Skoruppa, M., Zanella Béguelin, S.: Verified security of MerkleDamgård. In: CSF 2012, pp. 354–368 (2012)Google Scholar
 8.Backes, M., Berg, M., Unruh, D.: A formal language for cryptographic pseudocode. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 353–376. Springer, Heidelberg (2008)CrossRefGoogle Scholar
 9.Backes, M., Hofheinz, D., Unruh, D.: CoSP: a general framework for computational soundness proofs. In: CCS 2009, pp. 66–78. ACM (2009)Google Scholar
 10.Backes, M., Malik, A., Unruh, D.: Computational soundness without protocol restrictions. In: CCS 2012, pp. 699–711. ACM (2012)Google Scholar
 11.Ballarin, C.: Locales: A module system for mathematical theories. J. Automat. Reason. 52(2), 123–153 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
 12.Barthe, G., Fournet, C., Grégoire, B., Strub, P.Y., Swamy, N., Zanella Béguelin, S.: Probabilistic relational verification for cryptographic implementations. In: POPL 2014, pp. 193–205. ACM (2014)Google Scholar
 13.Barthe, G., Grégoire, B., Heraud, S., Béguelin, S.Z.: Computeraided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71–90. Springer, Heidelberg (2011)CrossRefGoogle Scholar
 14.Barthe, G., Grégoire, B., Zanella Béguelin, S.: Formal certification of codebased cryptographic proofs. In: POPL 2009, pp. 90–101. ACM (2009)Google Scholar
 15.Bellare, M., Rogaway, P.: Random oracles are practical: a paradigm for designing efficient protocols. In: CCS 1993, pp. 62–73. ACM (1993)Google Scholar
 16.Bellare, M., Rogaway, P.: The security of triple encryption and a framework for codebased gameplaying proofs. In: Vaudenay, S. (ed.) EUROCRYPT 2006. LNCS, vol. 4004, pp. 409–426. Springer, Heidelberg (2006)CrossRefGoogle Scholar
 17.Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. ACM Trans. Program. Lang. Syst. 33(2), 8:1–8:45 (2011)CrossRefGoogle Scholar
 18.Bhargavan, K., Fournet, C., Kohlweiss, M., Pironti, A., Strub, P.Y.: Implementing TLS with verified cryptographic security. In: S&P 2013, pp. 445–459. IEEE (2013)Google Scholar
 19.Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: CSFW 2001, pp. 82–96. IEEE (2001)Google Scholar
 20.Blanchet, B.: A computationally sound mechanized prover for security protocols. IEEE Trans. Dependable Secure Comput. 5(4), 193–207 (2008)CrossRefGoogle Scholar
 21.Blanchet, B., Jaggard, A.D., Rao, J., Scedrov, A., Tsay, J.K.: Refining computationally sound mechanized proofs for Kerberos. In: FCC 2009 (2009)Google Scholar
 22.Blanchette, J.C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (Co)datatypes for Isabelle/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 93–110. Springer, Heidelberg (2014)Google Scholar
 23.Blanchette, J.C., Popescu, A., Traytel, D.: Foundational extensible corecursion: A proof assistant perspective. In: ICFP 2015, pp. 192–204. ACM (2015)Google Scholar
 24.Cock, D.: Verifying probabilistic correctness in Isabelle with pGCL. In: SSV 2012. EPTCS, vol. 102, pp. 1–10 (2012)Google Scholar
 25.Cortier, V., Kremer, S., Warinschi, B.: A survey of symbolic methods in computational analysis of cryptographic systems. J. Automat. Reason. 46, 225–259 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
 26.Desharnais, J.: Labelled Markov Processes. Ph.D. thesis, McGill University (1999)Google Scholar
 27.Elgamal, T.: A public key cryptosystem and a signature scheme based on discrete logarithms. IEEE Trans. Inf. Theory 31(4), 469–472 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
 28.Gunter, E.L.: Why we can’t have SMLstyle datatype declarations in HOL. In: Claesen, L.J.M., Gordon, M.J.C. (eds.) TPHOLs 1992, pp. 561–568. Elsevier, NorthHolland (1993)Google Scholar
 29.Halevi, S.: A plausible approach to computeraided cryptographic proofs. Cryptology ePrint Archive, Report 2005/181 (2005)Google Scholar
 30.Hölzl, J., Lochbihler, A., Traytel, D.: A formalized hierarchy of probabilistic system types. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 203–220. Springer, Heidelberg (2015)Google Scholar
 31.Huffman, B., Kunčar, O.: Lifting and Transfer: a modular design for quotients in Isabelle/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131–146. Springer, Heidelberg (2013)CrossRefGoogle Scholar
 32.Hurd, J.: A formal approach to probabilistic termination. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 230–245. Springer, Heidelberg (2002)CrossRefGoogle Scholar
 33.Jouannaud, J.P., Xu, W.: Automatic complexity analysis for programs extracted from Coq proof. In: CLASE 2005. ENTCS, vol. 153(1), pp. 35–53 (2006)Google Scholar
 34.Krauss, A.: Recursive definitions of monadic functions. In: PAR 2010. EPTCS, vol. 43, pp. 1–13 (2010)Google Scholar
 35.Lammich, P.: Automatic data refinement. In: Blazy, S., PaulinMohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 84–99. Springer, Heidelberg (2013)CrossRefGoogle Scholar
 36.Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comp. 94(1), 1–28 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
 37.Lochbihler, A.: Formalisation accompanying this paper. http://www.infsec.ethz.ch/research/projects/FCSPI/ESOP2016.html
 38.Lochbihler, A., Züst, M.: Programming TLS in Isabelle/HOL. Isabelle Workshop 2014 (2014)Google Scholar
 39.Meier, S., Cremers, C.J.F., Basin, D.: Efficient construction of machinechecked symbolic protocol security proofs. J. Comput. Secur. 21(1), 41–87 (2013)CrossRefGoogle Scholar
 40.Mitchell, J.C.: Representation independence and data abstraction. In: POPL 1986, pp. 263–276. ACM (1986)Google Scholar
 41.Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL – A Proof Assistant for HigherOrder Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)zbMATHGoogle Scholar
 42.Petcher, A., Morrisett, G.: The foundational cryptography framework. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 53–72. Springer, Heidelberg (2015)Google Scholar
 43.Petcher, A., Morrisett, G.: A mechanized proof of security for searchable symmetric encryption. In: CSF 2015, pp. 481–494. IEEE (2015)Google Scholar
 44.Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP 1983. Information Processing, vol. 83, pp. 513–523. NorthHolland/IFIP (1983)Google Scholar
 45.Rutten, J.J.M.M.: Relators and metric bisimulations. Electr. Notes Theor. Comput. Sci. 11, 252–258 (1998)MathSciNetCrossRefzbMATHGoogle Scholar
 46.Sack, J., Zhang, L.: A general framework for probabilistic characterizing formulae. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 396–411. Springer, Heidelberg (2012)CrossRefGoogle Scholar
 47.Schmidt, B., Meier, S., Cremers, C.J.F., Basin, D.A.: Automated analysis of DiffieHellman protocols and advanced security properties. In: CSF 2012, pp. 78–94. IEEE (2012)Google Scholar
 48.Shoup, V.: Sequences of games: A tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004/332 (2004)Google Scholar
 49.Swamy, N., Chen, J., Fournet, C., Strub, P.Y., Bhargavan, K., Yang, J.: Secure distributed programming with valuedependent types. J. Funct. Program. 23(4), 402–451 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
 50.Wadler, P.: Theorems for free! In: FPCA 1989, pp. 347–359. ACM (1989)Google Scholar
 51.Zanella Béguelin, S.: Formal Certification of GameBased Cryptographic Proofs. Ph.D. thesis, École Nationale Supérieure des Mines de Paris (2010)Google Scholar