% !TeX root = easycrypt.tex

%\section{A Basic Example: Public-Key Encryption}
This section introduces key features of \EasyCrypt through the simple
but representative example of a public-key encryption scheme from
\citet{Bellare:1993}. On the modelling side, the example shows how to
model cryptographic schemes, security notions and security
assumptions, and in particular how to to define abstract operators and
axioms; how to clone theories; how to define module types, modules and
how to model adversaries as abstract procedures. On the proving side,
the example shows how to use the different logics supported by
\EasyCrypt, and in particular how to perform common reasoning patterns
such as reasoning up to failure; optimistic sampling and simple
reasoning about probabilites of events in games.


\subsubsection{Statement}
\EasyCrypt supports reductionist proofs in the style of provable
security~\citet{Goldwasser:1984}. This approach involves:
\begin{enumerate}
\item formalize a class of cryptographic constructions, and state
  precisely their intended security guarantees. For the latter, one
  must set the capacities of the adversary, and give a probabilistic
  experiment that defines the security goal. Security can then be
  quantified as the probability of an event in the experiment;

\item specify the primitives from which cryptographic constructions
  are built, and state explicitly the security properties that are
  assumed for them. Like security goals, they are generally formalized
  by means of experiments between a challenger and an adversary (an
  assumption could play the role of a security goal in a lower level
  proof);

\item define concrete cryptographic constructions that use primitives
  as black-boxes, and prove rigorously that every adversary against
  the construction can be turned into an adversary against one of the
  primitives, and prove that the probability that the former wins the
  experiment is small, provided the probability of the latter is.
\end{enumerate}
In our case study, we consider chosen-plaintext security of public-key
encryption schemes, and focus on schemes built from one-way trapdoor
permutations and random oracles. We prove, for the concrete scheme
considered in~\citet{Bellare:1993}, the following statement:
% TODO FIX STATEMENT USING ECIMPORT, POSSIBLY ADD MORE EXPLANATIONS
\begin{easycrypt}[]{}
lemma Conclusion :
forall (A <: Adv) &m, exists (I<:Inverter), 
Pr[CPA(BR,A).main() @ &m : res] - 1%r / 2%r 
<= Pr[OW(I).main() @ &m : res].
\end{easycrypt}
where the experiment \texttt{CPA} formalizes chosen-plaintext security
and \texttt{Adv} is the associated type of adversaries, whereas the
experiment \texttt{OW} formalizes one-wayness and \texttt{Inverter} is
the associated type of adversaries, \texttt{BR} is the public-key
encryption scheme from \citet{Bellare:1993}. 

The remaining of the section provides a detailed explanation of the
statement, and an outline of its proof.



\subsubsection{Setting}
We begin by introducing some basic concepts of cryptography and how we
model them in \EasyCrypt.

\paragraph{Bitstrings}
As part of its standard library, \EasyCrypt provides a theory of fixed-length
bitstrings coined \ec{Word}. For the purpose of this example, we will
need bitstrings of three different lengths, \ec{k} for messages,
\ec{l} for randomness and \ec{n} for ciphers; such that \ec{k + l =
  n}. The following piece of code declares three integer constants,
states the desired relationship between them as an axiom, clones the
theories (see Section~\ref{sec:cloning} for details on cloning) with
appropriate lengths and defines synonyms for the types.

\ecimport{ }{../examples/br93_tutorial.ec}{bitstrings}

The \ec{import} keyword allows us to ommit the qualified names when
they can be inferred from the lexical scope and typing context. 

We will be interested in sampling from uniform distributions of types
\ec{randomness} and \ec{plaintext}. These distributions are defined in
the standard library, but we define shortcuts to them as follows

\ecimport{ }{../examples/br93_tutorial.ec}{distributions}

where \ec{'a distr} is the type of discrete sub-distributions over
\ec{'a} (see Section~\ref{sec:distributions} for details on sub-distributions).

\paragraph{Random oracles}
A hash function in the random oracle model is a consistent random
function: new queries trigger samplings that are stored in a map; old
queries trigger a map lookup. 

Adversaries are normally given restricted access to the oracle, in the
sense that the amount of calls allowed is bounded. Moreover, we keep
track of the queries triggered by the adversary. 

The following piece of code defines two signatures for random oracles:
the one that will be used in the encryption of messages and the one
that will be provided to adversaries. Moreover, we define an
implementation between types \ec{randomness} and \ec{plaintext} as
defined above.

\ecimport{ }{../examples/br93_tutorial.ec}{random_oracles}


The module \ec{RO} is assigned two module types: \ec{Oracle} and
\ec{ARO} and implements both the normal oracle and the adversary
interface. It consists of a global variable \ec{m} that models the map
of the random oracle; a global variable \ec{s} that models the queries
performed by the adversary, a function \ec{init} that initializes the
map to \ec{empty} and the set to \ec{empty}, a function \ec{o} that
models the actual oracle and a function that models the adversary
version. The former takes an argument \ec{x} of type \ec{randomness},
samples a value \ec{y} of type \ec{plaintext}, updates the value of
the map when necesary and finally returns the lookup of \ec{x}
in the map \ec{m}. The latter checks that the adversary has not
exceeded the amount of calls as prescribed by \ec{qO}; and if this is
the case, records the query in \ec{s}, calls \ec{o} and returns its
result; otherwise, it returns a bitstring consisting of zeros.


\paragraph{One-way trapdoor permutations}
Trapdoor permutations are families of keyed functions that are \lq\lq
easy\rq\rq\ to compute but are \lq\lq hard\rq\rq\ to invert without
knowing the secret key. Formally, a family of trapdoor permutations is
modeled by a triple $(\KG,f,f^{-1})$, where $\KG$ is a probabilistic
key generation algorithm, and $f$ is a keyed permutation, and $f^{-1}$
is its inverse, i.e.\ for any pair of keys $(pk,sk)$ output by $\KG$,
$f(pk,\cdot)$ and $f^{-1}(sk,\cdot)$ are permutations and inverse of
each other.

In this case, we are interested in trapdoor permutations on type
\ec{randomness}. In \EasyCrypt we model them as follows

\ecimport{ }{../examples/br93_tutorial.ec}{one_way}

First, we declare two types \ec{pkey} and \ec{skey} that represent
public and secret keys respectively. We then declare a distribution
\ec{keypairs} that will be used by the $\KG$ algorithm to produce fresh
keys. We then declare an abstract predicate that will model when two
keys are matching and specify that all the pairs of keys that can be
sampled from \ec{keypairs} are matching. Afterwards, we declare \ec{f}
and \ec{finv} with the appropriate type and we state the axioms saying
that one is inverse of each other for valid pair of keys.
%% TODO (Francois -> JuanMa): you are missing the "matching keys" axiom
 
The module \ec{OW} is defined by declaring an interface corresponding
to the inverter, which comprises a function that given a challenge
value and a public key returns a guess for the pre-image of the
challenge. The one-wayness experiment is then defined by sampling a
value \ec{x} uniformly over the carrier of the trapdoor permutation
and a pair of keys \ec{pk} and \ec{sk} and providing the inverter with
the public key \ec{pk} and the image \ec{f pk x} of \ec{x}. The
inverter returns a value \ec{x'} and the experiment succeds if \ec{x =
  x'}.

\paragraph{Public-key encryption}
A public-key encryption scheme consists of a triple of algorithms
$(\KG,\Enc,\Dec)$:

\begin{description}
\item[Key Generation] 
  The key generation algorithm $\KG$ produces a pair of keys $(pk,sk)$;
  $pk$ is a \emph{public-key} used for encryption, $sk$ is
  a \emph{secret-key} used for decryption;

\item[Encryption] 
  Given a public-key $pk$ and a message $m$, $\Enc_{pk}(m)$ outputs a
  ciphertext $c$;

\item[Decryption] 
  Given a secret-key $sk$ and a ciphertext $c$, $\Dec_{sk}(c)$ outputs
  either message $m$ or a distinguished value $\bot$ denoting failure.
\end{description}
%
We require that for pairs of keys $(pk,sk)$ generated by $\KG$,
$\Dec_{sk}(\Enc_{pk}(m))= m$ holds for any message $m$. 

In \EasyCrypt, we model public-key encryption schemes in the following way

\ecimport{ }{../examples/br93_tutorial.ec}{scheme}

We declare the interface of an encryption scheme, that consists of a
key generation algorithm \ec{kg}, an encryption function \ec{enc} and
a decryption function \ec{dec}. Note that we are actually modelling
the particular class of encryption schemes that use at most one random
oracle.

\paragraph{The BR93 scheme}
The scheme we consider defines encryption as 
$\Enc_{pk}(m) = f_{pk}(r) \concat m \xor H(r)$, where $r$ is a
randomly sampled value and $H(r)$ denotes the result of a hash oracle
call with value $r$.

 In easycrypt we model the encryption scheme as an instance of our
 \ec{Scheme} signature as follows

\ecimport[morecomment={[is]{proof.}{qed.}}]{ }{../examples/br93_tutorial.ec}{br93}

First, we define a concatenation operation with the appropriate
type. In doing so, we make use of the array library, in particular,
the concat operation \ec{||}. Note that we have to insert the
appropriate cast functions that allows us to move from boolean arrays
to bitstrings of fixed size. We then define some useful lemmas (we
ommit the proofs for conciseness).

Afterwards, we define the module \ec{BR}, that makes use of a random
oracle \ec{R} and has type \ec{Scheme(R)}. This module defines the
required operations in the \ec{Scheme} signature. \ec{kg} samples a
pair of keys and returns them. \ec{enc} takes a public key \ec{pk} and
a plaintext \ec{m} and encrypts by samplying a random value \ec{r},
querying the oracle with this value and applying \ec{f} to \ec{pk} and
\ec{r} and appending it to the xor of result of the hash call and the
message. Decryption is defined by projecting the first part of \ec{c}
and applying \ec{finv} with \ec{sk} to it to recover the
randomness. Afterwards, we query the oracle with the randomness and
xor the result with the second part of \ec{c}.

\paragraph{The \textsf{IND-CPA} experiment}
The CPA experiment can be described in \EasyCrypt as follows:

\ecimport{ }{../examples/br93_tutorial.ec}{cpa}

We start by declaring a module type for the adversary. This interface
establishes that an adversary has to provide two functions. The
function \ec{a1} corresponds to the first round of the CPA game in
which the adverasay is given a public key \ec{pk} and produces two
plaintext of its choice. The function \ec{a2} corresponds to the
second phase, in which the adversary is presented with a challenge
ciphertext \ec{c} and he has to determine (by producing a boolean)
which plaintext was encrypted.

The module \ec{CPA} is parametrized by an adversary \ec{A_} and a
scheme \ec{S}. Note however, that in order to use these modules we
have to instantiate them with a random oracle. However, we will not
use the same oracle for both: for the encryption we use the bare
random oracle \ec{RO}, but for the adversary we first define \ec{AO},
a wrapped version of the oracle that provides the increased
functionality mentioned previously, and then we instantiate \ec{A_}
with it.

The function \ec{main} defines the CPA experiment. We initialize the
adversary oracle, and we call the key generation algorithm and obtain
\ec{pk} and \ec{sk}. Then we provide \ec{a1} with the public key and get
two plaintext \ec{m0} and \ec{m1}. We proceed by sampling a random bit
and we encrypt either \ec{m0} or \ec{m1} according to its value and we
call \ec{a2} with this ciphertext as argument and obtain a boolean
\ec{b'}. The experiment returns true if the adversary manages to
establish the value of \ec{b}, {\em i.e.} it returns \ec{b=b'}.

\paragraph{Security property}
We are interested in proving that for any adversary \ec{A} against CPA,
that manages to win with probability $P$, there exists a inverter
I that manages to win the one-way experiment with probability $Q$ such
that $| P - \frac{1}{2} |\leq Q$. The intuition is that an adversary
that constantly returns \ec{true} wins with probability
$\frac{1}{2}$. What we are measuring is essentially how much better
can an adversary do, and we are bounding it in terms of the
probability of suceeding in the one-way experiment.

This property is formalized in \EasyCrypt as follows

\ecimport{ }{../examples/br93_tutorial.ec}{conclusion}

The lemma \ec{Conclusion} is parametrized by an adversary \ec{A}. The
annotations \ec{\{Rand, RO\}} are memory access restrctions:
essentially, the adversary cannot access the memories of these modules
directly---only through oracle calls. The next parameter of the lemma
is a memory \ec{m}. Next, we have one hypothesis that states that if
the wrapped version of the random oracle terminates with probability
$1$, so does the adversary. The \ec{\%r} next to constants establishes
that they should be interpreted as real values. The existential
quantification binds a module \ec{I} of type \ec{Inverter}. The
expression \ec{Pr[CPA(BR,A).main() @ &m : res]} denotes the
probability of the event \ec{res} in the distribution obtained after
executing the \ec{main} function of module \ec{CPA}, instantiated with
the module \ec{BR} and the parametrized adversary $A$ in initial
memory \ec{m}. Similarly, the expression \ec{Pr[OW(BR_OW(A)).main() @
  &m : res]} denotes the probability of the event \ec{res} in the
distribution obtained after executing the \ec{main} function of module
\ec{OW}, instantiated with the existentially quantified module \ec{I},
in initial memory \ec{m}. These two expressions are of type real and
the \ec{<=} real less or equal operator.

The rest of the tutorial is devoted to introducing and explaining the
reasoning principles of \EasyCrypt required to establih this property.
%TODO: put forward pointers to françois' and guillaume's section

\subsubsection{Overview of the proof}
The proof proceeds by defining a sequence of transformation starting
on the initial game and proving a relationship between probabilities
of events of interests in each of these games. Each of these steps is
justified by reasoning in terms of probabilistic relational hoare
logic (pRHL for short).

The proof of the BR93 encryption scheme hinges on the following
sequence of games:
\begin{enumerate}
\item The first transformation we apply is to replace the call to the
  hash oracle in the encryption by a fresh randomly sampled value. The
  obtained encryption expression is $\Enc^2_{pk}(m) = f_{pk}(r) \concat
  m \xor r'$. We can show that the results of the encryption are
  observationally equivalent and that the resulting maps of the random
  oracle differ only in the query for value \ec{r}, provided that
  query done by the original encryption is fresh, therefore, if the
  adversary did not query \ec{r} to the random oracle. Hence, we bound
  the probability of \ec{b=b'} in the intitial game, in terms of the
  probability of winning in the second game, plus the probability of
  the event \ec{mem M.r ARO.s}, which means that the adversary was
  able to query \ec{r} to the random oracle.

\item Next, we modify the encryption scheme once again and replace the
  occurrence of $m\xor r'$ by $r'$ and we obtain $\Enc^3_{pk}(m) =
  f_{pk}(r) \concat r'$. This step is justified by means of optimistic
  sampling: $\Rand{r}{\bitstring{k};\Ass{v}{r\xor x}}$ and
  $\Rand{v}{\bitstring{k}}$ yield the same distribution of values of
  $v$.

\item  Note that at this point, the encryption algorithm does not depend on
  its input $m$ anymore. In particular, in the \ec{CPA} game, this
  means that the challenge \ec{c} that the adversary receives in the
  second round, does not depend on the bit \ec{b} anymore. We exploit
  this fact and at this point we modify de \ec{CPA} game by pushing
  the sampling of \ec{b} to the bottom of \ec{main}. At this point,
  the probability of \ec{b = b'} is exactly $\frac{1}{2}$.

\item We show that if the adversary manages to query \ec{r} to the
  random oracle, he can invert the one way function, since the only
  occurrence of \ec{r} in the cipher is as argument to the one way
  function. In doing so, we construct an inverter that receives a
  challenge \ec{y} and a public key, runs the first phase of the
  adversary, samples a value \ec{r'} and calls the second phase of the
  adversary with argument \ec{y || r'}. Afterwards, we go through
  the sets of queries performed by the adversary and look for $x$
  s.t. \ec{f pk x = y}. If we succeed, we return x.
\end{enumerate}

\subsubsection{Easycrypt proof}
In this section, we describe thoroughly the proof, as it is done in
easycrypt. We present intermediate games, and formally define the
relationships between them.

\paragraph{Reasoning up to failure: replacing \ec{H(r)} by fresh \ec{h}}
As mentioned above, the first step of the proof is to remove the hash
call in the encryption scheme and replace it by a randomly sampled
value. We define \ec{BR2} then, as follows

\ecimport{ }{../examples/br93_tutorial.ec}{br2}

Now, the question that arises is: when will an adversary be able to
distiguish \ec{h = H(r)} and \ec{h = $uniform_plain}? %$
If the query in the original scheme is fresh, it means that it will be
a randomly sampled value and in this case, the two values above are
indistinguishable. We formalize this reasoning step in pRHL as follows

\ecimport{ }{../examples/br93_tutorial.ec}{eq1enc}

The precondition states that when we run both encryptions with equal
arguments \ec{pk, m} and in inital states that coincide in the value
of \ec{RO.m}; if the value \ec{Rnd.r} has not been queried to
\ec{RO.m} on the right execution, the results coincide, the values of
\ec{Rnd.r} coincide and the mappings \ec{RO.m} are equal except in
\ec{Rnd.r}.

The proof proceeds by making use of a sequence of tactics. Among them
we have
\begin{itemize}
\item \ec{fun}: when called in a pRHL goal with two concrete
  procedures (such as in this case), it expands their definition. 
\item \ec{inline}: it expects a function identifier and inlines the
  calls in the current goal. In this case, it is used to inline the
  definition of RO.o in the current goal.
\item \ec{wp}: implements relational weakest precondition.
\item \ec{rnd}: implements the pRHL rule for random samplings. It
  takes a bijection (in the form of two functions $f$ and $g$) and ensures that
  the result of the random sampling on the left side is equal to $f$
  of the random sampling of the right side. When we ommit paramenters,
  the bijection is the identity.
\item \ec{skip}: allows to reduce the validity of the current
  judgement to the validity of a logical entailment between pre and
  post condition when the programs are ``empty''.
\item \ec{smt}: calls smt solvers in order to decide on the validity
  of a formula.
\end{itemize} 
For a detailed explanation of the tactics see Chapter (writting proofs).

At the point where the encryption scheme is called
within the CPA game, we know that all the values queried to the random
oracle correspond to adversary queries. Hence, the call is fresh if
the adversary has not queried this value. On the other hand, after the
encryption is called, we know that the oracle maps are equal, except
in the value of \ec{Rand.r}. Therefore, if the adversary in the second
round queries the hash oracle with \ec{Rand.r}, he manages to
distinguish between the two. To sum up, the behaviour is equivalent
except if the adversary manages to query \ec{Rand.r} either in the
first phase or in the second one. We formalize this reasoning in
easycrypt as follows

\ecimport{ }{../examples/br93_tutorial.ec}{eq1}

Upon starting the proof, after \ec{intros A Hll1 Hll2;fun}, we have
the following goal

%formatting needs to be fixed
\begin{easycrypt}[columns=fullflexible]{ }{\label{ec:proof1}}
Current goal

Type variables: <none>

A : Adv{RO, Rnd}
Hll1: forall (R <: ARO), islossless R.o_a => islossless A(R).a1
Hll2: forall (R <: ARO), islossless R.o_a => islossless A(R).a2
--------------------------------------
&1 (left ) : CPA(BR, A).main
&2 (right) : CPA(BR2, A).main

pre = (glob A){1} = (glob A){2}

RO.init()                                       (1)  RO.init()                       
(pk, sk) := CPA(BR, A).SO.kg()      (2)  (pk, sk) := CPA(BR2, A).SO.kg() 
(m0, m1) := CPA(BR, A).A.a1(pk)  (3)  (m0, m1) := CPA(BR2, A).A.a1(pk)
b =$ {0,1}                                    (4)  b =$ {0,1}                      
c := CPA(BR, A).SO.enc(pk,          (5)  c := CPA(BR2, A).SO.enc(pk,     
                       b ? m0 : m1)                                             b ? m0 : m1)                  
b' := CPA(BR, A).A.a2(c)               (6)  b' := CPA(BR2, A).A.a2(c)       

post = !(mem Rnd.r{2} RO.s{2}) => (b{1} = b'{1}) = (b{2} = b'{2})

\end{easycrypt}

The strategy we apply is the following:
\begin{itemize}
\item Before the second adversary call at the line 6, we know that the
  postcondition of \ec{enc} holds. Then, we use precondition

\ec{(!mem Rnd.r RO.s){2} => (={RO.s,c} /\\  eq_except RO.m{1} RO.m{2} Rnd.r{2}
                  /\\ (glob A){1} = (glob A){2})}

and postcondition \ec{((!mem Rnd.r RO.s){2} => ={res})}

In order to prove this specification, we use \ec{fun} with two
arguments:
\begin{itemize}
  \item The first one is a failure event $F$, in this case \ec{mem Rnd.r
      RO.s}.
    \item The second one, is an invariant $I$, in this case 
      \ec{(={RO.s} /\\ eq_except RO.m{1} RO.m{2} Rnd.r{2})}.
\end{itemize}
The idea is that the invariant will hold, as long as the failure event
doesn't. This tactic generates the following proof obligations:
\begin{itemize}
\item a logical entailment of the form $P \Rightarrow \textsf{ if } F
  \textsf{ then true else } I$, where $P$ is the precondition
  (discharged by \ec{smt};

\item a logical entailment of the form $(\lnot F \Rightarrow
  I)\Rightarrow Q$, where $Q$ is the postcondition (discharged by
  \ec{smt});

\item losslessness of the adversary, assuming losslessness of the
  oracles he has access to (in our case this is an assumption);

\item a pRHL judgement for each of the oracles the adversary has
  access to, with precondition $!F \land I \land =\{\mathsf{args}\}$
  and postcondition $!F \Rightarrow (I \land=\{\mathsf{res}\})$;

\item losslessness of the oracles the adversary has access to,
  assuming $F$ holds in the initial state;

\item preservation of $F$ for all the oracles the adversary has access
  to (a bounded probabilistic hoare logic judgement with precondition
  $F$ and postcondition $F$ and probability 1).
\end{itemize}
For a more detailes account of reasoning up to failure, we refer the
reader to Section (upto bad section).


\item For the call to the encryption scheme in line 5, we use the
  specification we established previously. This is done using
  \ec{call} with the same spec, and then applying the lemma
  \ec{eq_enc1}.

\item The random samplings of b in line 5 are handled using the
  \ec{rnd} tactic. This ensures that the values are considered equal. 

\item For the first adversary call in line 4, we provide a
  specification. For the precondition we use
 \ec{(={RO.m,RO.s,pk} /\\ (glob A){1} = (glob A){2} /\\ dom RO.m{2} =
   RO.s{2})}, and for the postcondition, the same formula, except that
 we require equality on \ec{res} rather than in the argument
 \ec{pk}. We prove this specification using \ec{fun} with invariant
 (I) defined as \ec{(={RO.m,RO.s} /\\ dom RO.m{2} = RO.s{2})}. This
 tactic generates the following proof obligations:
\begin{itemize}
\item a logical entaliment of the form $P \Rightarrow I \land
  (\mathsf{glob}\;A)\{1\} = (\mathsf{glob}\;A)\{2\} \land
  =\{\mathsf{args}\}$, where $P$ is the precondition,
  $\mathsf{glob}\;A$ represents the global variables of adversary
  \ec{A} (all the state variables in all the modules, except those
  modules to which access is explcitly restricted in the annotations)
  and $\mathsf{args}$ represents the arguments of the adversary;
\item a logical entailment of the form $I \land
  (\mathsf{glob}\;A)\{1\} = (\mathsf{glob}\;A) \land =\{\mathsf{res}\}
  \Rightarrow Q$, where $\mathsf{res}$ is the result of the adversary
  and $Q$ is the postcondition;
\item a pRHL judgement for each of the oracles the adversary has
  access to, with precondition $I \land =\{\mathsf{args}\}$ and
  postcondition $I \land =\{\mathsf{res}\}$.
 \end{itemize} 
For a more detailed account of the rule for adversary calls, we refer
the reader to Section(call for adversaries).
\item It remains to prove that the code before the call in line 3
  establishes the precondition. This is done by inlining the code and
  using \ec{wp} and \ec{rnd} when necessary. 

\item Once we have two empty programs, we use \ec{skip} to reduce the
  validity of the judgement to the validity of a logic formula. Then
  we apply \ec{progress}, which implements a simplification strategy
  for formulas, and we discharge the resulting goals using the
  \ec{smt} tactic, which interfaces with smt solvers and concludes the
  proof. 
\end{itemize}
From the pRHL judgement we have just proved, we can conclude the
following property

\ecimport{ }{../examples/br93_tutorial.ec}{prob1}

The proof proceeds by transitivity:
\begin{itemize}
\item First, we prove 

\ec{Pr[CPA(BR,A).main() @ &m : res] <=
Pr[CPA(BR2,A).main() @ &m : res \\/ mem Rnd.r RO.s]},
using our pRHL proof and the tactic \ec{equiv_deno}.

\item Next, we prove

\ec{Pr[CPA(BR2,A).main() @ &m : res \\/ mem Rnd.r RO.s] <=} 

\ec{Pr[CPA(BR2,A).main() @ &m : res]} +

\ec{Pr[CPA(BR2,A).main() @ &m : mem Rnd.r RO.s]}

using the tactic \ec{pr_or}, that implements the following reasoning
principle:
\ec{Pr[ f() @ &m : a \\/ b]} =  \ec{Pr[ f() @ &m : a]} + \ec{Pr[ f() @
  &m : b]} - \ec{Pr[ f() @ &m : a /\\ b]}.
 
\end{itemize}

\paragraph{Optmistic sampling: replacing \ec{m \^\^ r'} by \ec{r'}}
The second step of the proof consists on modifying again the
computation of the ciphertext. In this case, instead of computing the
$\xor$ of the message $m$ with the randomly sampled value $r'$, we
directly place $r'$ in that position. This transformation is defined
as follows
\ecimport{ }{../examples/br93_tutorial.ec}{br3}

We can prove that the results of the two versions of the encryption
are indistinguishable resorting to optimistic sampling. The following
\EasyCrypt script shows the desired property

\ecimport{ }{../examples/br93_tutorial.ec}{eq2enc}

The specification states that when the two versions of the encryption
function are called with equal arguments and in two states where the
maps associated to the random oracle are equal, the functions yield
the same result and produce states where the maps of the oracle are
equal and the randomness is equal.  

The key reasoning step is embodied by the tactic \ec{rnd (lambda v, v
  \^\^ m) (lambda v, v\^\^ m)}. In its most general form, the \ec{rnd}
tactic takes a bijection, represented as a pair of functions inverse
from eachother. When the arguments are ommitted, the identity function
is used as bijection. This tactic implments the pRHL rule for random
assignments shown in (Reference to Reasoning about random samplings)
and in this case, it allows us to conclude that ${h\{2\} = m\{1\} \xor
  h\{1\}}$.

Using this specification for \ec{enc}, we can conclude this step as
follows
\ecimport{ }{../examples/br93_tutorial.ec}{eq2}

Note that here we have the same code on both sides, operating on the
same state. The only difference is in the code for encryption, that we
already proved yields equal results. Hence, all the invariants we are
use consist of equalities on variables on both sides. 

Once more, using our pRHL logic judgements, we conclude a property on
the probabilities of th events we are interested in as follows

\ecimport{ }{../examples/br93_tutorial.ec}{prob2}





\paragraph{Code movement: sampling \ec{b} at the end}
At this point, the encryption function does not depend on the input
message anymore. We take advantage of this fact and modify the CPA
game to sample the bit \ec{b} at the bottom of the game; hence making
explicit that the adversary cannot gain any information regarding its
value by inspecting the cipher. The \ec{CPA2} game is defined as
follows
\ecimport{ }{../examples/br93_tutorial.ec}{cpa2}

Again, we are interested in showing the equivalence of the events of
interest. In \EasyCrypt we carry out this step in the following way
\ecimport{ }{../examples/br93_tutorial.ec}{eq3}

The key step in this case, is \ec{swap{2} -2}. This tactic moves the
last instruction of the second game \ec{b = $\{0,1\}} %$
up by two instructions. After this, we have the exact same code on
both sides, so we conclude the proof using a serie of invariants that
consists of equalities on variables on both states; as done in the
previous step. 

At this point we can prove the following result on probabilities
\ecimport{ }{../examples/br93_tutorial.ec}{prob3}

The proof consists of three steps:
\begin{itemize}
\item \ec{Pr[CPA(BR3,A).main() @ &m : res] = Pr[CPA2(BR3,A).main() @
    &m : res]} 
\item \ec{Pr[CPA(BR3,A).main() @ &m : mem Rnd.r RO.s] = Pr[CPA2(BR3,A).main() @
    &m : mem Rnd.r RO.s]}
\item \ec{Pr[CPA2(BR3,A).main() @  &m : res] = 1\%r/2\%r}
\end{itemize}
The first two are proved, as usual, relying on the previously proved
pRHL judgement and in \ec{equiv_deno}. The last one relies on bounded
probabilistic Hoare logic. This logic allows us to reason regarding
bounds of events in our probabilistic language. In particular, in this
case we show that the probability of \ec{b = b'} in a game where \ec{b}
is sampled at the end is $\frac{1}{2}$. This proof is relatively
straightforward and consists of two parts:
\begin{itemize}
\item Showing that all the code before the sampling of \ec{b} is
  lossless, {\em i.e.} terminates with probability 1;
\item showing that a program that consists uniquely of the sampling of
  a boolean \ec{b} yields a distribution where the event \ec{b = true}
  and \ec{b = false} have probability $\frac{1}{2}$.
\end{itemize}

For the first part, we do the same kind of reasoning as when we did
reasoning up to failure. Basically, we have to show that the program
terminates unconditionally. In doing so, we show that all function
calls are lossless: concrete calls are handled by inlining and
adversaries are handeled using our losslessness hypotheses.

For the second part, the key step is the use of the \ec{rnd (1\%r /
  2\%r) (lambda b, b = b')}. This tactic takes a bound and an event
(depending on the value sampled), consumes the random sampling and
produces the following goal


\ec{mu \{0,1\} (lambda (b0 : bool), b0 = CPA2(BR3, A).main.b') = 1\%r / 2\%r},

where \ec{mu} is an axiomatized that measures the probability of an
event in a distribution. In our case, we conclude by relying on the
definition of the \ec{\{0,1\}} distribution.


\paragraph{Constructing the inverter}
At this point, we construct an inverter that witnesses the reduction:
we construct module \ec{BR_OW}, parametrized on an adversary \ec{A},
that implements a function \ec{i} representing the inverter
\ecimport{ }{../examples/br93_tutorial.ec}{inverter}

The main idea is that we construct the challenge \ec{c} in such a way
that we place the challenge \ec{y}, received from the \ec{OW} game in
the position of the application of function \ec{f}. The function
initilializes the oracle, calls \ec{a1} with the public key \ec{pk}
recived from the one way experiment, samples the random value \ec{h}
to be used in the cipher and calls \ec{a2} with the challenge \ec{y ||
  h}. Afterwards, we look for a value \ec{x} in the adversary queries,
such that \ec{f pk x = y} and we return it. Then, we prove that if the
adversary manages to query \ec{Rnd.r} to the random oracle, our search
is succesful and the result of the \ec{OW} experiment is true. 

\ecimport{ }{../examples/br93_tutorial.ec}{eq4}

The proof uses similar invariants than the ones we have been using
witnessing the fact that we are able to succesfully simulate the
environment in which the adversary \ec{A} is run originally. The proof
is concluded by reasoning about the \ec{find} operator and using the
fact that the function $f$ is ``injective'' in the following sense

\ecimport{ }{../examples/br93_tutorial.ec}{finy}