diff --git a/config/tests.config b/config/tests.config index a5762df7d..9a4678f6a 100644 --- a/config/tests.config +++ b/config/tests.config @@ -13,5 +13,8 @@ exclude = examples/MEE-CBC examples/old examples/old/list-ddh !examples/incomple [test-mee-cbc] okdirs = examples/MEE-CBC +[test-tutorials] +okdirs = !doc/tutorials + [test-unit] okdirs = tests tests/exception diff --git a/doc/conf.py b/doc/conf.py index 568857a10..00c1b4cbd 100644 --- a/doc/conf.py +++ b/doc/conf.py @@ -15,7 +15,7 @@ # -- Project information ----------------------------------------------------- # https://www.sphinx-doc.org/en/master/usage/configuration.html#project-information -project = 'EasyCrypt refman' +project = 'EasyCrypt Documentation' copyright = '2026, EasyCrypt development team' author = 'EasyCrypt development team' diff --git a/doc/index.rst b/doc/index.rst index 8b6c7d9b2..21136c71a 100644 --- a/doc/index.rst +++ b/doc/index.rst @@ -1,7 +1,8 @@ -EasyCrypt reference manual +EasyCrypt Documentation ======================================================================== .. toctree:: :maxdepth: 2 - tactics + tutorials + reference diff --git a/doc/reference.rst b/doc/reference.rst new file mode 100644 index 000000000..0e5cce7c7 --- /dev/null +++ b/doc/reference.rst @@ -0,0 +1,8 @@ +Reference Material +======================================================================== + +.. toctree:: + :maxdepth: 1 + :glob: + + reference/* diff --git a/doc/tactics.rst b/doc/reference/tactics.rst similarity index 100% rename from doc/tactics.rst rename to doc/reference/tactics.rst diff --git a/doc/tactics/async-while.rst b/doc/reference/tactics/async-while.rst similarity index 100% rename from doc/tactics/async-while.rst rename to doc/reference/tactics/async-while.rst diff --git a/doc/tactics/cfold.rst b/doc/reference/tactics/cfold.rst similarity index 100% rename from doc/tactics/cfold.rst rename to doc/reference/tactics/cfold.rst diff --git a/doc/tactics/clear.rst b/doc/reference/tactics/clear.rst similarity index 100% rename from doc/tactics/clear.rst rename to doc/reference/tactics/clear.rst diff --git a/doc/tactics/hoare-split.rst b/doc/reference/tactics/hoare-split.rst similarity index 100% rename from doc/tactics/hoare-split.rst rename to doc/reference/tactics/hoare-split.rst diff --git a/doc/tactics/if.rst b/doc/reference/tactics/if.rst similarity index 100% rename from doc/tactics/if.rst rename to doc/reference/tactics/if.rst diff --git a/doc/tactics/proc.rst b/doc/reference/tactics/proc.rst similarity index 100% rename from doc/tactics/proc.rst rename to doc/reference/tactics/proc.rst diff --git a/doc/tactics/procstar.rst b/doc/reference/tactics/procstar.rst similarity index 100% rename from doc/tactics/procstar.rst rename to doc/reference/tactics/procstar.rst diff --git a/doc/tactics/rnd.rst b/doc/reference/tactics/rnd.rst similarity index 100% rename from doc/tactics/rnd.rst rename to doc/reference/tactics/rnd.rst diff --git a/doc/tactics/simplify-if.rst b/doc/reference/tactics/simplify-if.rst similarity index 100% rename from doc/tactics/simplify-if.rst rename to doc/reference/tactics/simplify-if.rst diff --git a/doc/tactics/skip.rst b/doc/reference/tactics/skip.rst similarity index 100% rename from doc/tactics/skip.rst rename to doc/reference/tactics/skip.rst diff --git a/doc/tactics/splitwhile.rst b/doc/reference/tactics/splitwhile.rst similarity index 100% rename from doc/tactics/splitwhile.rst rename to doc/reference/tactics/splitwhile.rst diff --git a/doc/tactics/swap.rst b/doc/reference/tactics/swap.rst similarity index 100% rename from doc/tactics/swap.rst rename to doc/reference/tactics/swap.rst diff --git a/doc/tutorials.rst b/doc/tutorials.rst new file mode 100644 index 000000000..3343f06fd --- /dev/null +++ b/doc/tutorials.rst @@ -0,0 +1,10 @@ +Tutorials +======================================================================== + +.. toctree:: + :maxdepth: 0 + :glob: + + tutorials/tutorials.rst + tutorials/introduction-itp-program-logics.rst + tutorials/encryption-from-prf.rst diff --git a/doc/tutorials/encryption-from-prf.rst b/doc/tutorials/encryption-from-prf.rst new file mode 100644 index 000000000..3ca317071 --- /dev/null +++ b/doc/tutorials/encryption-from-prf.rst @@ -0,0 +1,16 @@ +Encryption from a PRF +===================== + +As a warm-up, we’ll consider a simple nonce-based symmetric encryption +scheme for fixed-length messages. [1]_ Here, we assume some familiarity +with cryptographic definitions and proofs, but not with the specific +definitions and proofs used in this tutorial. + +You may find it beneficial to step through the `proof +file `__ as you +read through the basic tutorial. The “Going Further” tutorials each come +with their own proof files, referred to where relevant. + +.. [1] + Note the similarities to The Joy of Cryptography’s `Construction + 7.4 `__. diff --git a/doc/tutorials/encryption-from-prf/Construction.eca b/doc/tutorials/encryption-from-prf/Construction.eca new file mode 100644 index 000000000..35d3fb1d0 --- /dev/null +++ b/doc/tutorials/encryption-from-prf/Construction.eca @@ -0,0 +1,783 @@ +(* ****************** Requires/Imports ******************* *) +(* Built-in (i.e., standard library *) +require import AllCore Distr List. + + +(* ****************** Types (i.e., non-empty sets) ******************* *) +(* Keys, plaintexts and nonces *) +type key, ptxt, nonce. + +(* Ciphertexts (same set as for plaintexts) *) +type ctxt = ptxt. + + + +(* ****************** Operators ******************* *) +(* + A family of functions from nonces to plaintexts, indexed by + the set of keys. +*) +op f : key -> nonce -> ptxt. + +(* Binary operator over plaintexts *) +op (+) : ptxt -> ptxt -> ptxt. + +(* + Assumed associativity, commutativity, and "left self-cancellation" + properties of + operator, respectively. +*) +axiom addpA (x y z : ptxt) : x + y + z = x + (y + z). +axiom addpC (x y : ptxt) : x + y = y + x. +axiom addKp (x y : ptxt) : x + x + y = y. + +(* "Right self-cancellation" propery of + *) +lemma addpK (x y : ptxt) : x + y + y = x. +proof. +(* + Rewrite y + x + x as y + (x + x) + using above associativity axiom addpA +*) +rewrite addpA. +(* + Rewrite y + (x + x) as (x + x) + y (which is simply rendered as x + x + y) + using above commutativity axiom addpC +*) +rewrite addpC. +(* + Rewrite x + x + y as y + using above "left self-cancellation" axiom addKp +*) +rewrite addKp. +(* Trivially true: y = y *) +trivial. +qed. + + + +(* ****************** Distributions ******************* *) +(* (Sub)Distribution over keys **) +op dkey : key distr. + +(* + Proper, uniform distribution over the entire set of + plaintexts (and, hence, ciphertexts). +*) +op [lossless full uniform] dptxt : ptxt distr. + +(* + Alias to make it clear when we are conceptually considering + plaintexts and ciphertexts (even though they are really the same thing) +*) +op dctxt : ctxt distr = dptxt. + + + +(* ****************** Scheme ******************* *) +(* Module type (i.e., interface) for (symmetric) nonce-based encryption schemes *) +module type NBEncScheme = { + proc kgen() : key + proc enc(k : key, n : nonce, m : ptxt) : ctxt + proc dec(k : key, n : nonce, c : ctxt) : ptxt +}. + +(* Specification of the considered (symmetric) nonce-based encryption scheme *) +module E : NBEncScheme = { + proc kgen(): key = { + var k : key; + + (* Sample key k from (sub)distribution dkey *) + k <$ dkey; + + return k; + } + + proc enc(k : key, n : nonce, m : ptxt) : ctxt = { + (* + Compute f k n, combine it with the message using +, + and return the result + *) + return (f k n) + m; + } + + proc dec(k : key, n : nonce, c : ctxt) : ptxt = { + (* + Compute f k n, combine it with the ciphertext using +, + and return the result + *) + return (f k n) + c; + } +}. + + + +(* ****************** Security ******************* *) +(* + -- + INDistinguishability from RANDOM ciphertexts under Nonce-Respecting + Chosen-Plaintext Attacks (IND$-NRCPA) + + By observing ciphertext (supposedly) of chosen messages, it is hard + to determine whether the ciphertexts were honestly created by a + (symmetric nonce-based) encryption scheme or sampled uniformly at random. + -- +*) + +(* + Module type (i.e., interface) for oracles used in IND$-NRCPA game. + Note the "option" in "ctxt option" (the return type of enc); intuitively, + this means that enc can either return a valid ciphertext c (as Some c) or an + indication of failure (as None). This is needed as the oracles will indicate + a failure when being queried on a nonce that was already used in a previous + query. +*) +module type NRCPA_Oraclei = { + proc init() : unit + proc enc(n : nonce, m : ptxt) : ctxt option +}. + +(* + Module type (i.e., interface) for oracles provided to the adversaries + against the IND$-NRCPA game. Used to ensure we only expose the enc procedure + of the oracles to the adversaries, and not the init procedure. +*) +module type NRCPA_Oracle = { + (* Include only the enc procedure signature of the NRCPA_Oraclei module type *) + include NRCPA_Oraclei [enc] +}. + +(* + Real oracle used in IND$-NRCPA game (and, thus, of type NRCPA_Oraclei). + Defined with respect to an (abstract) nonce-based encryption scheme E that it + uses to encrypt messages. +*) +module O_NRCPA_real (S : NBEncScheme) : NRCPA_Oraclei = { + var k : key (* Secret key *) + var log : nonce list (* Log of queried nonces *) + + (* Perform necessary initialization *) + proc init() : unit = { + (* Generate secret key with key generation of provided scheme *) + k <@ S.kgen(); + + (* Initialize log to the empty list *) + log <- []; + } + + (* Encryption procedure exposed to the adversary *) + proc enc(n : nonce, m : ptxt) : ctxt option = { + var c : ctxt; + var r : ctxt option; (* return variable *) + + (* If the given nonce is not in the log of already queried nonces, ... *) + if (! (n \in log)) { + (* then prepend the current nonce to the log, ... *) + log <- n :: log; + + (* encrypt the message using the provided scheme, and ... *) + c <@ S.enc(k, n, m); + + (* store the resulting ciphertext in the return variable; ... *) + r <- Some c; + } else { + (* else, store an indication of failure in the return variable. *) + r <- None; + } + + return r; + } +}. + +(* + Ideal oracle used in IND$-NRCPA game (and, thus, of type NRCPA_Oraclei). + Instead of encrypting messages with an encryption scheme, it produces + ciphertexts by sampling them uniformly at random. +*) +module O_NRCPA_ideal : NRCPA_Oraclei = { + var log : nonce list (* Log of queried nonces *) + + (* Perform necessary initialization *) + proc init() : unit = { + (* Initialize log to the empty list *) + log <- []; + } + + (* Encryption procedure exposed to the adversary *) + proc enc(n : nonce, m : ptxt) : ctxt option = { + var c : ctxt; + var r : ctxt option; (* return variable *) + + (* If the given nonce is not in the log of already queried nonces, ... *) + if (! (n \in log)) { + (* then prepend the current nonce to the log, ... *) + log <- n :: log; + + (* sample a ciphertext from dctxt, and ... *) + c <$ dctxt; + + (* store the resulting ciphertext in the return variable; ... *) + r <- Some c; + } else { + (* else, store an indication of failure in the return variable. *) + r <- None; + } + + return r; + } +}. + +(* + Module type (i.e., interface) for adversaries (or distinguishers) against IND$-NRCPA. + In essence, this defines the relevant class of adversaries, containing + any algorithm that expects a NR-CPA oracle and defines a + procedure returning a boolean. +*) +module type Adv_IND_NRCPA (O : NRCPA_Oracle) = { + proc distinguish() : bool +}. + +(* IND$-NRCPA game/experiment *) +module Exp_IND_NRCPA (O : NRCPA_Oraclei) (D : Adv_IND_NRCPA) = { + proc run() : bool = { + var b : bool; + + (* Initialize oracle O *) + O.init(); + + (* + Call distinguish procedure of adversary D, providing oracle O. + Note that, even though O is of type NRCPA_Oraclei, providing it + to D does not expose the init procedure to D. This because D itself + only expects the provided oracle to have the enc procedure, due to + the type of D being defined with respect to a module of type NRCPA_Oracle. + *) + b <@ D(O).distinguish(); + + return b; + } +}. + + +(* + -- + "Nonce-Respecting" Pseudo-Random Function family (NR-PRF) + + By observing outputs (supposedly) of unique chosen inputs (nonces), it is hard to + distinguish whether the function is a randomly sampled function from the domain + of functions with the considered domain (nonce) and co-domain (ptxt), or + a randomly selected function from the hash function family f (i.e., a f k + where k is randomly sampled from the domain of (indexing) keys). + -- +*) +(* + Module type (i.e., interface) for oracles used in NR-PRF game. + Again, note the "option" in "ptxt option" (the return type of get) to + model that the oracle can return either valid plaintexts (as Some p) or + an indication of failure (as None). +*) +module type NRPRF_Oraclei = { + proc init() : unit + proc get(n : nonce) : ptxt option +}. + +(* + Module type (i.e., interface) for oracles used in NR-PRF game. + Used to ensure we only expose the get procedure of the oracles + to the advesaries, and not the init procedure. +*) +module type NRPRF_Oracle = { + (* Include only the get procedure signature of the NRCPA_Oraclei module type *) + include NRPRF_Oraclei [get] +}. + +(* + Real oracle used in NR-PRF game (and, thus, of type NRPRF_Oraclei). + Creates plaintexts by mapping a given nonce under f k, where k is a + secret key randomly sampled during initialization. +*) +module O_NRPRF_real : NRPRF_Oraclei = { + var k : key (* Secret key *) + var log : nonce list (* Log of queried nonces *) + + (* Perform necessary initialization *) + proc init() : unit = { + (* Sample secret key at random *) + k <$ dkey; + (* Initialize log to the empty list *) + log <- []; + } + + (* Get procedure exposed to the adversary *) + proc get(n : nonce) : ptxt option = { + var r : ptxt option; (* return variable *) + + (* If the given nonce is not in the log of already queried nonces, ... *) + if (! (n \in log)) { + (* then prepend the current nonce to the log and ... *) + log <- n :: log; + + (* compute f k n and store the result in the return variable; ... *) + r <- Some (f k n); + } else { + (* else, store an indication of failure in the return variable. *) + r <- None; + } + + return r; + } +}. + +(* + Ideal oracle used in NR-PRF game (and, thus, of type NRPRF_Oraclei). + Instead of mapping given nonces under f k, it produces + plaintexts by sampling them uniformly at random. +*) +module O_NRPRF_ideal : NRPRF_Oraclei = { + var log : nonce list (* Log of queried nonces *) + + (* Perform necessary initalization *) + proc init() = { + (* Initialize log to the empty list *) + log <- []; + } + + (* Get procedure exposed to the adversary *) + proc get(n : nonce) = { + var y : ptxt; + var r : ptxt option; (* return variable *) + + (* If the given nonce is not in the log of already queried nonces, ... *) + if (! (n \in log)) { + (* then prepend the current nonce to the log and ... *) + log <- n :: log; + + (* sample a plaintext from dptxt, and ... *) + y <$ dptxt; + + (* store the resulting plaintext in the return variable; ... *) + r <- Some y; + } else { + (* else, store an indication of failure in the return variable. *) + r <- None; + } + + return r; + } +}. + +(* Module type (i.e., interface) for adversaries (or distinguishers) against NR-PRF. *) +module type Adv_NRPRF (O : NRPRF_Oracle) = { + proc distinguish() : bool +}. + +(* NR-PRF game/experiment *) +module Exp_NRPRF (O : NRPRF_Oraclei) (D : Adv_NRPRF) = { + proc run() : bool = { + var b : bool; + + (* Initialize oracle O *) + O.init(); + + (* + Call distinguish procedure of adversary D, providing oracle O. + Again, even though O is of type NRPRF_Oraclei, providing it + to D does not expose the init procedure to D as it expects an oracle + of type NRPRF_Oracle (i.e., an oracle that is only guaranteed to + implement get). + *) + b <@ D(O).distinguish(); + + return b; + } +}. + + +(* + Reduction adversary that, given an adversary against IND$-NRCPA, plays in the + NR-PRF game. As such, it takes a (adversary) module of type Adv_IND_NRCPA and + a (oracle) module of type NRPRF_Oracle and implements a distinguish procedure. + Here, the order of the module arguments is crucial for obtaining a module + of the correct type. Namely, a module of type Adv_NRPRF should only be defined w.r.t. + a module of type NRPRF_Oracle, and not w.r.t. both a module of type Adv_IND_NRCPA *and* + a module of type NRPRF_Oracle. Since we can instantiate the module parameters partially + (yet only from left to right), the module parameter of type Adv_IND_NRCPA should come before + the module parameter of type NRPRF_Oracle. Then, only instantiating the first module parameter + (e.g., R_NRPRF_IND_NRCPA(D), where D is a concrete module of type Adv_IND_NRCPA) results + in a module that is only still defined w.r.t. a module of type NRPRF_Oracle, as desired. + Lastly, note that the explicit typing of R_NRPRF_IND_NRCPA (D : Adv_IND_NRCPA) is not necessary + and, hence, the module signature of the reduction adversary could equivalently be written as + "module R_NRPRF_IND_NRCPA (D : Adv_IND_NRCPA) (O_NRPRF : NRPRF_Oracle)". However, even though + types can often be inferred, it is good practice to state the types explicitly for documentation + purposes. +*) +module (R_NRPRF_IND_NRCPA (D : Adv_IND_NRCPA) : Adv_NRPRF) (O_NRPRF : NRPRF_Oracle) = { + (* + Using the provided NRPRF oracle, construct a NRCPA oracle to provide + to the given adversary. + *) + module O_NRCPA : NRCPA_Oracle = { + (* Encryption procedure exposed to the given adversary *) + proc enc(n : nonce, m : ptxt) : ctxt option = { + var p : ptxt option; + var r : ctxt option; (* return variable *) + + (* + Get plaintext (or failure indication) corresponding to n + by querying given NRPRF oracle + *) + p <@ O_NRPRF.get(n); + + (* + Compute a ciphertext or failure indication as follows: + If p is a failure indication (i.e., p = None), + r is also a failure indication (i.e., r = None); + else (i.e., p = Some x for some x of type ptxt), + r is Some (x + m). + *) + r <- if p = None then None else Some (oget p + m); + + return r; + } + } + + (* Distinguish procedure called by the NR-PRF game/experiment *) + proc distinguish() : bool = { + var b : bool; (* return variable *) + + (* + Call the distinguish procedure of the given adversary, providing + the above-defined NRCPA oracle O_NRCPA + *) + b <@ D(O_NRCPA).distinguish(); + + return b; + } +}. + + +(* + Start a section for the security proof. + Although we could perform the entire proof without a section, this would + require us to define the considered adversary module (and all the corresponding + restrictions) anew for each (intermediate) lemma we prove. Furthermore, + every intermediate lemma we prove would become a permanent part of the theory + (defined by the file), even if it is completely useless outside the proof. + A section allows us, among others, to "declare" the relevant modules (with restrictions) + once and have them available throughout the entire section (but not outside the section). + Additionally, we can define local types, operators, module types, modules, and lemmas; + these are only available/visible within the section and, as such, can be used to perform + any auxiliary intermediate proof steps without any of it being exposed to the outside. + Any non-local lemmas inside the section (i.e., lemmas that are exposed to the outside + after closing the section) are extended with a universal quantification over module types + of the modules declared earlier in the section. +*) +section E_IND_NRCPA. + +(* + Declare the relevant adversary module. + Note that, by default, a module can access any other module's variables. + So, to prevent the adversary from illegally sabotaging the games that it is used in, + we need to restrict the adversary from accessing the variables of the modules used in + these games. +*) +declare module D <: Adv_IND_NRCPA { -O_NRCPA_real, -O_NRCPA_ideal, -O_NRPRF_real, -O_NRPRF_ideal }. + +(* + Lemma. + The probability of D returning true in the IND$-NRCPA game when given the + real NR-CPA oracle is equal to the probability of R_NRPRF_IND_NRCPA returning true + when given D and the real NR-PRF oracle. + + This lemma is local (indicated by the "local" keyword), meaning that it is only + useable inside the section and, as such, can depend on local entities. +*) +local lemma EqPr_IND_NRCPA_NRPRF_real &m: + Pr[Exp_IND_NRCPA(O_NRCPA_real(E), D).run() @ &m : res] + = + Pr[Exp_NRPRF(O_NRPRF_real, R_NRPRF_IND_NRCPA(D)).run() @ &m : res]. +proof. +(* + Prove the equality of probabilities by showing the pRHL equivalence of the programs + where the programs start out with adversary D having the same + environment (precondition) and end up with the same result (postcondition). + + We can combine tactics using a semicolon. + Specifically, "t1; t2." first applies tactic t1 on the goal and, afterward, + applies tactic t2 on all of the subgoals generated by applying t1. + So, here, "; trivial" applies trivial to all subgoals generated by applying byequiv, + solving/closing all generated trivial subgoals. +*) +byequiv (_ : ={glob D} ==> ={res}); trivial. +(* + Since both procedures in the pRHL equivalence are concrete, + prove the equivalence by reasoning about the actual code of the procedures. +*) +proc. +(* + In both programs, replace all calls to concrete procedures by the corresponding code + to be able to reason about the concrete code. +*) +inline *. +(* + Since both programs are sufficiently similar and call to the same abstract procedure + that only differ in the implementation of the provided oracles, we can use the sim tactic. + To infer the correct equality of program variables from the postcondition, we provide an + explicit equality in form of an invariant that should be maintained throughout oracles + calls. (in this case: the keys and logs of the oracles are equal) +*) +sim (_ : ={k}(O_NRCPA_real, O_NRPRF_real) /\ ={log}(O_NRCPA_real, O_NRPRF_real)). +(* + Goal generated by sim tactic. + pRHL equivalence between the enc procedures of the provided oracles + where, as a precondition, we have equality of the inputs and the truth of + the invariant, and, as a postcondition, we need to prove the equality + of the (distribution of the) outputs as well as the truth of the + invariant. +*) +(* proc, and inline * tactics used similarly to above. *) +proc. +inline *. +(* + Although it looks convoluted, the programs in the current goal can be trivially + seen to be equivalent and, hence, solved by straightforward manipulations (e.g., + unfolding definitions). The auto tactic uses various program logic tactics in attempt + to reduce the goal and in is suffient to solve it in this case. + We could also use wp. skip. trivial. to solve the goal. These tactics are used + and explained in the next proof. +*) +auto. +qed. + +(* + Lemma. + The probablity of D returning true in the IND$-NRCPA game when given the + ideal NR-CPA oracle is equal to the probability of R_NRPRF_IND_NRCPA returning true + when given D and the ideal NR-PRF oracle. + + This lemma is local (indicated by the "local" keyword), meaning that it is only + useable inside the section and, as such, can depend on local entities. +*) +local lemma EqPr_IND_NRCPA_NRPRF_ideal &m: + Pr[Exp_IND_NRCPA(O_NRCPA_ideal, D).run() @ &m: res] + = + Pr[Exp_NRPRF(O_NRPRF_ideal, R_NRPRF_IND_NRCPA(D)).run() @ &m: res]. +proof. +(* + Most of the tactics and their application in this proof + are similar to those in the previous proof. As such, we do not provide + comments for each and every tactic, but rather only wherever novel + concepts arise. +*) +(* + The trailing "=> //" is semantically equivalent to "; trivial", but syntactically + more convenient/clean (especially when specifying more introduction patterns; + see below for more information on these patterns). +*) +byequiv (_ : ={glob D} ==> ={res}) => //. +proc; inline *. +(* + From the end of the programs, consume all statements for which we know how to + adapt the postcondition as to reflect the execution of the statements without + actually executing them. In other words, transform the current pRHL equivalence + to a new one that implies the current one by removing as many statements + from the end of the programs as possible while accordingly adapting the postcondition. +*) +wp. +(* + Since both programs end with calls to the same abstract procedure that only differ + in the implementation of the provided oracles, argue that the procedure + must behave the same (and, hence, with the same probability produce the same + output) as long as the module's view remains equal on both sides during the call. + This requires the following: + - The module's environment (in this case: glob D) is the same in both programs + at the start of the call. + - The procedure's arguments (in this case: none) are the same on both sides. + - The (distribution of the) oracle outputs is the same on both sides; this may + require some invariant (in this case: the logs of the oracles are equal) + to be maintained throughout oracles calls. + The first two requirements are proved based on the code preceding the calls; the final + requirement is proved with a separate pRHL equivalence on the oracle procedures (using + the invariant that is supplied to the call tactic, following the colon). +*) +call (_ : ={log}(O_NRCPA_ideal, O_NRPRF_ideal)). + (* + First subgoal generated by call tactic. + pRHL equivalence between the enc procedures of the provided oracles + where, as a precondition, we have equality of the inputs and the truth of + the invariant, and, as a postcondition, we need to prove the equality + of the (distribution of the) outputs as well as the truth of hte + invariant. + *) +- proc; inline *. + (* + Analogous to wp, but removes statements from the beginning of the programs + (instead of the end) and accordingly adjusts the precondition (instead of the + postcondition). + *) + sp. + (* + Since both programs *start* with an if-statement, we can prove this + pRHL equivalence by showing the following: + - The guards of the if-statements are equivalence (i.e., the if-guard of the left program + evaluates to true iff the if-guard of the right program evaluates to true); this means + the left and right program go into the same branch. + - An appropriate pRHL equivalence where both programs take the then branch. + - An appropriate pRHL equivalence where both programs take the else branch. + + As the equivalence of the guards is trivial, we clear the corresponding subgoal + using "=> //". + *) + if => //. + (* First subgoal generated by if tactic. *) + - wp. + (* + Whenever both programs end with a sampling from the same distribution (remember, dctxt is + simply an alias for dptxt), we oftentimes want to assume that the same value is sampled + on both sides using the rnd tactic. This tactic removes the samplings and adjusts the + postcondition to capture that the sampled values are the same. (This produces some + additional proof obligations in the postcondition that make sure this is actually + sound.) + However, since in the postcondition we do not require the equality of the sampled values, + but rather of a random value and the addition of a random value with a fixed value, + we want to "uniquely link" two sampled values that satisfy this equivalence. + In other words, if + we can specify a bijection (defined by, say, f and g = f^-1) between elements from + the distribution of the left program and elements from the distribution of + the right program (in this case: "a bijection on the set of plaintexts/ciphertexts"), + we can assume that if we sample an element p in the left program, we sample f p in the + right program. + + To perform sampling that uses a certain bijection, we can provide f and g to the rnd + tactic (syntax: rnd f g). If f = g, then we can leave out the g (syntax: rnd f). + This latter case is applicable here. + *) + rnd (fun (p : ptxt) => p + m{2}). + wp. + (* + The skip tactic proves the pRHL equivalence where both programs are empty by showing that, + for all possible program memories, the precondition implies the postcondition. + Here, "=> /> &2 _" does several things. Foremost, "=>" after a tactic allows us + to specify several so-called "introduction patterns" (such as the "//" seen earlier) + that will be applied to all subgoals generated by the preceding tactics (in this + case: skip, only generating a single subgoal). Then, the first introduction pattern, + />, simplfies the resulting subgoal as much as possible; the second introduction + pattern, &2, specifies the name for the arbitrary memory introduced into the + context, removing the "forall memory" quantification in the subgoal's conclusion; + lastly, _ deletes the foremost antecedent of the subgoal's conclusion (we don't + need it to prove the remainder). + *) + skip => />. + move => &2 _. + (* + We prove a conjunction of predicates by splitting up the goal and + proving each of the predicates individually. + *) + split. + (* First subgoal generated by split tactic. *) + (* + The move tactic does nothing, but still allows us to use + introduction patterns (with "=>") + *) + - move => y _. + (* + The rewrite tactic allows for some nice syntactic sugar. + Instead of "rewrite lemma1; rewrite lemma2.", we can use "rewrite lemma1 lemma2.". + Similarly, instead of "rewrite lemma1 => //", we can use "rewrite lemma1 //.". + *) + rewrite addpK //. + (* Second subgoal generated by split tactic. *) + move => _ c _. + rewrite addpK //. + (* Second subgoal generated by if tactic. *) + auto. +(* Second subgoal generated by call tactic. *) +auto. +qed. + + +(* + Lemma. + The advantage of D against IND$-NRCPA of E is equal to the advantage of + R_NRPRF_IND_NRCPA against NRPRF of f (when given D). + + This lemma is non-local, meaning it will be exposed outside the section and + will be preceded by a universal quantification for each module declared in + the section. Moreover, it cannot depend on local entities (as these are + non-existant outside the section). +*) +lemma EqAdvantage_IND_NRCPA_NRPRF &m: + `| Pr[Exp_IND_NRCPA(O_NRCPA_real(E), D).run() @ &m: res] + - Pr[Exp_IND_NRCPA(O_NRCPA_ideal, D).run() @ &m: res] | + = + `| Pr[Exp_NRPRF(O_NRPRF_real, R_NRPRF_IND_NRCPA(D)).run() @ &m: res] + - Pr[Exp_NRPRF(O_NRPRF_ideal, R_NRPRF_IND_NRCPA(D)).run() @ &m: res] |. +proof. +(* + The by keyword can be put in front of (a sequence of) tactics to try and + close all subgoals generated by the (sequence of) tactics. This will + only be successful if the generated subgoals are trivially solvable. + + The minuses in front of lemma names in a rewrite tactic + indicate that the rewriting should occur in the opposite direction + of the equality/equivalence denoted by the lemma. For example, + suppose we have a lemma eqXY that shows X = Y. Then, rewrite eqXY + rewrites all X in the goal's conclusion to Y, and rewrite -eqXY rewrites + all Y in the goal's conclusion to X. +*) +by rewrite EqPr_IND_NRCPA_NRPRF_real EqPr_IND_NRCPA_NRPRF_ideal. +qed. + +end section E_IND_NRCPA. + +(** +(** BONUS: A cost logic **) +require import Xint CHoareTactic. + +clone import AllCore.Cost. + +op t_oplus: { int | 0 < t_oplus } as gt0_t_oplus. + +op t_prf: { int | 0 < t_prf } as gt0_t_prf. + +(** Assumptions on cost **) +schema cost_omap `{P} {f : 'a -> 'b } { o : 'a option }: + cost [P : omap f o] = cost [P : f (oget o)]. + +schema cost_transpose `{P} {f : 'a -> 'b -> 'c } { x : 'a } { y : 'b }: + cost [P : transpose f y x] = cost [P : f x y]. + +schema cost_oplus `{P} { x y : ptxt }: + cost[P : x + y] = cost[P : x] + cost[P : y] + N t_oplus. + +schema cost_prf `{P} { k : key } { n : nonce }: + cost[P : f k n] = cost[P : k] + cost [P : n] + N t_prf. + +section. +declare op q_enc : { int | 0 < q_enc } as gt0_q_enc. +declare op t_distinguish : { int | 0 < t_distinguish } as gt0_t_distinguish. + +declare module D <: CPA_Distinguisher { -NR_CPA_Experiment, -PRF_Experiment, -CPA_Real, -PRF_Real } [distinguish : `{N t_distinguish, #O.enc : q_enc }]. + +lemma cost_return: + cost(_: {m : ptxt, n : nonce, r : ptxt option}) [true : omap (transpose Top.(+) m) r] + = N (t_oplus + 1). +proof. +instantiate -> := (cost_omap {m : ptxt, n : nonce, r : ptxt option } `(true) (fun x=> x + m) r). +instantiate -> := (cost_transpose {m : ptxt, n : nonce, r : ptxt option } `(true) (+) (oget r) m). +instantiate -> := (cost_oplus {m : ptxt, n : nonce, r : ptxt option } `(true) (oget r) m). +instantiate -> := (cost_oget {m : ptxt, n : nonce, r : ptxt option } `(true) r). +have ->: cost (_ : {m : ptxt, n : nonce, r : ptxt option})[true : r] = N 0 by auto. +have ->: cost (_ : {m : ptxt, n : nonce, r : ptxt option})[true : m] = N 0 by auto. +by rewrite -!N_D /#. +qed. + +lemma reduction_cost (P <: PRF_Oracle { -D, -R } [f : `{N t_prf}]): + choare[R(D, P).distinguish] time [N (t_distinguish + q_enc * (t_oplus + 1)); P.f : q_enc]. +proof. +proc true: time [R(D, P).E.enc : [N (t_oplus + 1); P.f: 1]]=> //. ++ by auto=> />; rewrite Bigxint.bigi_constz 2:StdBigop.Bigint.bigi_constz 1,2:ltzW 1,2:gt0_q_enc /#. +move=> k Hk; proc=> //. ++ by right; rewrite cost_return. +by call (: true; time []); auto=> />; rewrite cost_return. +qed. +end section. +**) diff --git a/doc/tutorials/encryption-from-prf/IVbased.ec b/doc/tutorials/encryption-from-prf/IVbased.ec new file mode 100644 index 000000000..601145792 --- /dev/null +++ b/doc/tutorials/encryption-from-prf/IVbased.ec @@ -0,0 +1,569 @@ +require import AllCore List Distr FSet. +require (* *) Construction Birthday. + +(** Non-empty sets for keys, plaintexts and nonces **) +type key, ptxt, rndness. +type ctxt = ptxt. + +(** Some (arbitrary, here) distribution over keys **) +op [lossless] dkey: key distr. + +(** Some (arbitrary, here) distribution over randomness **) +op [lossless full uniform] drndness: rndness distr. + +(** Some (arbitrary, here) distribution over plaintexts/ciphertexts **) +op [lossless full uniform] dptxt : ptxt distr. +op dctxt = dptxt. + +(** And a family of functions from nonces to plaintexts, indexed by + the set of keys **) +op f: key -> rndness -> ptxt. + +(** Some associative, commutative, self-cancelling operator over + plaintexts **) +op (+): ptxt -> ptxt -> ptxt. +axiom addpA x y z: x + y + z = x + (y + z). +axiom addpC x y: x + y = y + x. +axiom addKp x y: x + x + y = y. + +lemma addpK x y: y + x + x = y. +proof. by rewrite addpA addpC addKp. qed. + +(** The scheme!! **) +module type Enc_Scheme = { + proc kgen(): key + proc enc(k : key, r : rndness, m : ptxt): ctxt + proc dec(k : key, r : rndness, c : ctxt): ptxt +}. + +module E : Enc_Scheme = { + proc kgen(): key = { + var k; + + k <$ dkey; + return k; + } + + proc enc(k : key, r : rndness, m : ptxt) : ctxt = { + var x; + + x <- f k r; + return x + m; + } + + proc dec(k : key, r : rndness, c : ctxt) : ptxt = { + var x; + + x <- f k r; + return x + c; + } +}. + +clone import Construction as C with + type key <- key, + type ptxt <- ptxt, + type nonce <- rndness, + op f <- f, + op (+) <- (+), + op dkey <- dkey, + op dptxt <- dptxt + (* Why can't I do E <- E, they are literally the same. I do not want duplicates. *) +proof *. +realize addpA by exact/addpA. +realize addpC by exact/addpC. +realize addKp by exact/addKp. +realize dptxt_ll by exact/dptxt_ll. +realize dptxt_uni by exact/dptxt_uni. +realize dptxt_fu by exact/dptxt_fu. + +(** CPA security **) +module type CPA_Oracle_IV_i = { + proc init(): unit + proc enc(m : ptxt) : rndness * ctxt +}. + +module O_IV_ideal : CPA_Oracle_IV_i = { + proc init() : unit = { + } + + proc enc(m : ptxt) : rndness * ctxt = { + var r, c; + + r <$ drndness; + c <$ dctxt; + return (r, c); + } +}. + +module O_IV_real (E : Enc_Scheme) : CPA_Oracle_IV_i = { + var k : key + + proc init() : unit = { + k <@ E.kgen(); + } + + proc enc(m : ptxt) : rndness * ctxt = { + var r, c; + + r <$ drndness; + c <@ E.enc(k, r, m); + return (r, c); + } +}. + +(** The type of encryption oracles **) +module type CPA_Oracle_IV = { + include CPA_Oracle_IV_i [enc] +}. + +module type CPA_Distinguisher_IV (O : CPA_Oracle_IV) = { + proc distinguish() : bool +}. + +module Exp_IV_CPA (D : CPA_Distinguisher_IV) (O : CPA_Oracle_IV_i) = { + proc run() = { + var b; + + O.init(); + b <@ D(O).distinguish(); + return b; + } +}. + +module Counting_O (O : CPA_Oracle_IV_i) : CPA_Oracle_IV_i = { + var counter : int + var log : rndness list + + proc init() : unit = { + O.init(); + Counting_O.log <- []; + } + + proc enc(m : ptxt) : rndness * ctxt = { + var rc; + + counter <- counter + 1; + + rc <@ O.enc(m); + log <- rc.`1 :: log; + + return rc; + } +}. + +(* +module (Counting_D (D : CPA_Distinguisher_IV) : CPA_Distinguisher_IV) (O : CPA_Oracle_IV) = { + var counter : int + + module O_Counting : CPA_Oracle_IV = { + proc enc(m : ptxt) : rndness * ctxt = { + var rc; + + counter <- counter + 1; + + rc <@ O.enc(m); + + return rc; + } + } + + proc distinguish() = { + var b : bool; + + b <@ D(O_Counting).distinguish(); + + return b; + } +}.*) + +module (Reduction (D : CPA_Distinguisher_IV) : Adv_IND_NRCPA) (O: NRCPA_Oracle) = { + module IV_Oracle : CPA_Oracle_IV = { + var log : rndness list + + proc enc(m : ptxt) : rndness * ctxt = { + var r : rndness; + var c : ctxt option; + + r <$ drndness; + log <- r :: log; + + c <@ O.enc(r, m); + + return (r, oget c); + } + } + + proc distinguish() : bool = { + var b : bool; + + IV_Oracle.log <- []; + + b <@ D(IV_Oracle).distinguish(); + + return b /\ uniq IV_Oracle.log; + } +}. + +(** Proof for security of IV-based encryption **) +section. + +declare module D <: CPA_Distinguisher_IV{ -O_NRCPA_real, -O_NRCPA_ideal, -O_IV_real, -O_IV_ideal, -O_NRPRF_ideal, -O_NRPRF_real, -Reduction, -Counting_O }. + +lemma Counting_real &m: + Pr[Exp_IV_CPA(D, O_IV_real(E)).run() @ &m: res] = + Pr[Exp_IV_CPA(D, Counting_O(O_IV_real(E))).run() @ &m: res]. +proof. +byequiv (: ={glob D} ==> ={res})=> //. +proc; inline *. +call (: ={O_IV_real.k}). ++ by proc; inline *; auto. +by auto. +qed. + +lemma Counting_ideal &m: + Pr[Exp_IV_CPA(D, O_IV_ideal).run() @ &m: res] = + Pr[Exp_IV_CPA(D, Counting_O(O_IV_ideal)).run() @ &m: res]. +proof. +byequiv => //; proc; inline *. sp. +call (: true). +proc. inline *. auto. skip => //=. +qed. + +declare axiom D_ll (O <: CPA_Oracle_IV {-D}): islossless O.enc => islossless D(O).distinguish. + +(** maximal number of queries to the encryption oracle **) +declare op q : { int | 0 <= q } as ge0_q. + +local clone import Birthday as BB with + op q <- q, + type T <- rndness, + op uT <- drndness +proof *. +realize ge0_q by exact: ge0_q. +(*realize maxuP. by move=> x; rewrite (drndness_uni x maxu) 1,2:drndness_fu. qed. (* change that in birthday theory! *)*) + +declare axiom D_bounded (O <: CPA_Oracle_IV_i {-D}) : + hoare[D(Counting_O(O)).distinguish : Counting_O.counter = 0 ==> Counting_O.counter <= q]. + +local lemma Counting_bounded_real : + hoare[Exp_IV_CPA(D, Counting_O(O_IV_real(E))).run : Counting_O.counter = 0 ==> Counting_O.counter <= q]. +proof. proc; inline *. seq 3 : #pre. auto. call (D_bounded (O_IV_real(E))) => //=. qed. + +local lemma Counting_bounded_ideal : + hoare[Exp_IV_CPA(D, Counting_O(O_IV_ideal)).run : Counting_O.counter = 0 ==> Counting_O.counter <= q]. +proof. proc; inline *. call (D_bounded (O_IV_ideal)) => //=. auto. qed. + +local module O_IV_S_real (S: Sampler) (E: Enc_Scheme) : CPA_Oracle_IV_i = { + var k : key + + proc init() : unit = { + k <@ E.kgen(); + S.init(); + } + + proc enc(m : ptxt) : rndness * ctxt = { + var r : rndness; + var c : ctxt; + + r <@ S.s(); + c <@ E.enc(O_IV_S_real.k, r, m); + + return (r, c); + } +}. + +local module O_IV_S_ideal (S: Sampler) : CPA_Oracle_IV_i = { + var k : key + + proc init() : unit = { + S.init(); + } + + proc enc(m : ptxt) : rndness * ctxt = { + var r : rndness; + var c : ctxt; + + r <@ S.s(); + c <$ dctxt; + + return (r, c); + } +}. + +local lemma Sample_real &m: + Pr[Exp_IV_CPA(D, O_IV_real(E)).run() @ &m: res] = + Pr[Exp_IV_CPA(D, O_IV_S_real(Sample, E)).run() @ &m: res]. +proof. +byequiv => //. +proc; inline *. +sim (: ={k}(O_IV_real, O_IV_S_real)). +proc; inline *. +by wp; rnd; skip. +qed. + +local lemma Sample_ideal &m: + Pr[Exp_IV_CPA(D, O_IV_ideal).run() @ &m: res] = + Pr[Exp_IV_CPA(D, O_IV_S_ideal(Sample)).run() @ &m: res]. +proof. +byequiv => //. +proc; inline *. +call(: true). ++ proc; inline *. + by wp; rnd; wp; rnd; skip. +by wp. +qed. + +local lemma IV_S_real_uniq &m: + Pr[Exp_IV_CPA(D, O_IV_S_real(Sample, E)).run() @ &m: res /\ uniq Sample.l] + = + Pr[Exp_IND_NRCPA(O_NRCPA_real(E), Reduction(D)).run() @ &m: res]. +proof. +byequiv => //. +proc; inline *. +wp. +call (: ! uniq Reduction.IV_Oracle.log, + ={k}(O_IV_S_real, O_NRCPA_real) + /\ Sample.l{1} = Reduction.IV_Oracle.log{2} + /\ Reduction.IV_Oracle.log{2} = O_NRCPA_real.log{2}, + uniq Sample.l{1} = uniq Reduction.IV_Oracle.log{2}) => //=. ++ apply D_ll. ++ proc; inline *. + seq 2 2 : ( ={m} + /\ r0{1} = r{2} + /\ O_IV_S_real.k{1} = O_NRCPA_real.k{2} + /\ Sample.l{1} = Reduction.IV_Oracle.log{2} + /\ Reduction.IV_Oracle.log{2} = r{2} :: O_NRCPA_real.log{2}). + - wp. rnd. skip => //. + case (uniq Reduction.IV_Oracle.log{2}); last first. + - conseq (: _ ==> true) => />. + by wp. + rcondt{2} 3; 1: by move=> ?; wp; skip. + by wp; skip. ++ move=> &2 uql. + proc; inline *. + wp; rnd; skip => />. + rewrite uql => &1 -> /=. + by rewrite drndness_ll. ++ move=> &1. + proc; inline *. + wp; rnd; skip => />. + by rewrite drndness_ll. +by wp; rnd; skip => /> /#. +qed. + +local lemma IV_S_ideal_uniq &m: + Pr[Exp_IV_CPA(D, O_IV_S_ideal(Sample)).run() @ &m: res /\ uniq Sample.l] + = + Pr[Exp_IND_NRCPA(O_NRCPA_ideal, Reduction(D)).run() @ &m: res]. +proof. +byequiv => //. +proc; inline *. +wp. +call (: ! uniq Reduction.IV_Oracle.log, + Sample.l{1} = Reduction.IV_Oracle.log{2} + /\ Reduction.IV_Oracle.log{2} = O_NRCPA_ideal.log{2}, + uniq Sample.l{1} = uniq Reduction.IV_Oracle.log{2}) => //=. ++ apply D_ll. ++ proc; inline *. + seq 2 2 : ( ={m} + /\ r0{1} = r{2} + /\ Sample.l{1} = Reduction.IV_Oracle.log{2} + /\ Reduction.IV_Oracle.log{2} = r{2} :: O_NRCPA_ideal.log{2}). + - by wp; rnd; skip. + case (uniq Reduction.IV_Oracle.log{2}); last first. + - conseq (: _ ==> true) => />. + wp; sp. + if{2} => /=. + * by wp; rnd; wp; skip. + by rnd{1}; wp; skip. + rcondt{2} 3; 1: by move=> ?; wp; skip. + by wp; rnd; wp; skip. ++ move=> &2 uql. + proc; inline *. + rnd; wp; rnd; skip => />. + rewrite uql => &1 -> /=. + by rewrite dptxt_ll drndness_ll. ++ move=> &1. + proc; inline *. + wp. + seq 1 : #pre => //. + - by rnd; skip; rewrite drndness_ll. + - sp; if. + * wp; rnd; wp; skip. + by rewrite dptxt_ll /#. + by wp; skip => />. + hoare => /=. + by rnd; skip. +by wp; skip => /> /#. +qed. + +local module S' (S : ASampler) = { + include S + + proc init() = {} +}. + +local module (BB_Reduction_real (E : Enc_Scheme) : Adv) (S : ASampler) = { + proc a() = { + O_IV_S_real(S'(S), E).init(); + + D(O_IV_S_real(S'(S), E)).distinguish(); + } +}. + +local module (BB_Reduction_ideal : Adv) (S : ASampler) = { + proc a() = { + O_IV_S_ideal(S'(S)).init(); + + D(O_IV_S_ideal(S'(S))).distinguish(); + } +}. + +local equiv blop: + D(O_IV_S_real(S'(Sample), E)).distinguish + ~ D(Counting_O(O_IV_S_real(S'(Sample), E))).distinguish: + ={glob D, O_IV_S_real.k, Sample.l} /\ (size Sample.l = Counting_O.counter){2} + ==> ={res, O_IV_S_real.k, Sample.l} /\ (size Sample.l = Counting_O.counter){2}. +proof. +proc (={O_IV_S_real.k, Sample.l} /\ (size Sample.l = Counting_O.counter){2})=> //. +by proc; inline *; auto=> /> &2 _ _; rewrite addzC. +qed. + +local equiv blopii: + D(O_IV_S_ideal(S'(Sample))).distinguish + ~ D(Counting_O(O_IV_S_ideal(S'(Sample)))).distinguish: + ={glob D, O_IV_S_ideal.k, Sample.l} /\ (size Sample.l = Counting_O.counter){2} + ==> ={res, O_IV_S_ideal.k, Sample.l} /\ (size Sample.l = Counting_O.counter){2}. +proof. +proc (={O_IV_S_ideal.k, Sample.l} /\ (size Sample.l = Counting_O.counter){2})=> //. +by proc; inline *; auto=> /> &2 _ _; rewrite addzC. +qed. + +local lemma Counting_BB_Reduction_real : + hoare[BB_Reduction_real(E, Sample).a : size Sample.l = 0 ==> size Sample.l <= q]. +proof. +proc; inline *; seq 2 : #pre; auto. +call (: size Sample.l = 0 ==> size Sample.l <= q)=> //. +conseq blop (: Counting_O.counter = 0 ==> Counting_O.counter <= q)=> />. ++ move=> &1 size_0; exists (glob D){1} 0 O_IV_S_real.k{1} Sample.l{1}=> />. +by conseq (D_bounded (O_IV_S_real(S'(Sample), E))). +qed. + +local lemma Counting_BB_Reduction_ideal : + hoare[BB_Reduction_ideal(Sample).a : size Sample.l = 0 ==> size Sample.l <= q]. +proof. +proc; inline *. +call (: size Sample.l = 0 ==> size Sample.l <= q)=> //. +conseq blopii (: Counting_O.counter = 0 ==> Counting_O.counter <= q)=> />. ++ move=> &1 size_0; exists (glob D){1} 0 O_IV_S_ideal.k{1} Sample.l{1}=> />. +by conseq (D_bounded (O_IV_S_ideal(S'(Sample)))). +qed. + +local lemma help1 &m: + Pr[Exp_IV_CPA(D, O_IV_S_real(Sample, E)).run() @ &m : ! uniq Sample.l] = + Pr[Exp(Sample, BB_Reduction_real(E)).main() @ &m : ! uniq Sample.l]. +proof. +byequiv (: _ ==> ={Sample.l}) => //=. +proc; inline *. +call (: ={O_IV_S_real.k, Sample.l}) => //. +* proc; inline *. + by wp; rnd; skip. +by wp; rnd; wp; skip. +qed. + +local lemma help2 &m: + Pr[Exp_IV_CPA(D, O_IV_S_ideal(Sample)).run() @ &m : ! uniq Sample.l] = + Pr[Exp(Sample, BB_Reduction_ideal).main() @ &m : ! uniq Sample.l]. +proof. +byequiv (: _ ==> ={Sample.l}) => //=. +proc; inline *. +call (: ={Sample.l}) => //. +- proc; inline *. + by rnd; wp; rnd; skip. +by wp; skip. +qed. + + +lemma IV_security_NR &m: + `| Pr[Exp_IV_CPA(D, O_IV_real(E)).run() @ &m: res] + - Pr[Exp_IV_CPA(D, O_IV_ideal).run() @ &m: res] | + <= + `| Pr[Exp_IND_NRCPA(O_NRCPA_real(E), Reduction(D)).run() @ &m: res] + - Pr[Exp_IND_NRCPA(O_NRCPA_ideal, Reduction(D)).run() @ &m: res] | + + (q * (q - 1))%r / 2%r * mu1 drndness witness. +proof. +rewrite Sample_real Sample_ideal Pr[mu_split (uniq Sample.l)]. +have ->: + Pr[Exp_IV_CPA(D, O_IV_S_ideal(Sample)).run() @ &m : res] + = + Pr[Exp_IV_CPA(D, O_IV_S_ideal(Sample)).run() @ &m : res /\ uniq Sample.l] + + Pr[Exp_IV_CPA(D, O_IV_S_ideal(Sample)).run() @ &m : res /\ ! uniq Sample.l]. ++ by rewrite Pr[mu_split uniq Sample.l]. +rewrite StdOrder.RealOrder.Domain.opprD -StdOrder.RealOrder.Domain.addrCA. +apply (StdOrder.RealOrder.ler_trans + (`| Pr[Exp_IV_CPA(D, O_IV_S_real(Sample, E)).run() @ &m : res /\ uniq Sample.l] - + Pr[Exp_IV_CPA(D, O_IV_S_ideal(Sample)).run() @ &m : res /\ uniq Sample.l] | + + `| Pr[Exp_IV_CPA(D, O_IV_S_real(Sample, E)).run() @ &m : res /\ ! uniq Sample.l] - + Pr[Exp_IV_CPA(D, O_IV_S_ideal(Sample)).run() @ &m : res /\ ! uniq Sample.l] |)). ++ smt(StdOrder.RealOrder.ler_norm_add). +rewrite StdOrder.RealOrder.ler_add 1:StdOrder.RealOrder.ler_eqVlt. ++ by rewrite IV_S_real_uniq IV_S_ideal_uniq. +apply (StdOrder.RealOrder.ler_trans + (StdOrder.RealOrder.maxr + Pr[Exp_IV_CPA(D, O_IV_S_real(Sample, E)).run() @ &m : res /\ ! uniq Sample.l] + Pr[Exp_IV_CPA(D, O_IV_S_ideal(Sample)).run() @ &m : res /\ ! uniq Sample.l])). ++ by rewrite StdOrder.RealOrder.ler_norm_maxr Pr[mu_ge0]. +rewrite StdOrder.RealOrder.maxrE (: mu1 drndness witness = mu1 drndness maxu). ++ by rewrite (drndness_uni witness maxu) 1,2:drndness_fu. +case (Pr[Exp_IV_CPA(D, O_IV_S_ideal(Sample)).run() @ &m : res /\ ! uniq Sample.l] <= + Pr[Exp_IV_CPA(D, O_IV_S_real(Sample, E)).run() @ &m : res /\ ! uniq Sample.l]) => ?. ++ apply (StdOrder.RealOrder.ler_trans + (Pr[Exp_IV_CPA(D, O_IV_S_real(Sample, E)).run() @ &m : ! uniq Sample.l])). + - byequiv (: ={glob D} ==> ={Sample.l}) => //. + proc; inline *. + call (: ={O_IV_S_real.k, Sample.l}). + * proc; inline *. + by wp; rnd; skip. + by wp; rnd; skip. + rewrite help1. + apply (pr_collision (BB_Reduction_real(E))); 1: move=> T Tll. + - proc; inline *. + call (: true); 1: by apply D_ll. + * proc; inline *. + by wp; call(: true). + by wp; rnd; skip; rewrite dkey_ll. + by apply Counting_BB_Reduction_real. +apply (StdOrder.RealOrder.ler_trans + (Pr[Exp_IV_CPA(D, O_IV_S_ideal(Sample)).run() @ &m : ! uniq Sample.l])). ++ byequiv (: ={glob D} ==> ={Sample.l}) => //. + proc; inline *. + call (: ={Sample.l}). + - proc; inline *. + by rnd; wp; rnd; skip. + by wp; skip. +rewrite help2. +apply (pr_collision (BB_Reduction_ideal)); 1: move=> T Tll. ++ proc; inline *. + call (: true) => //; 1: by apply D_ll. + proc; inline *. + by rnd; call(: true); skip; rewrite dptxt_ll. +by apply Counting_BB_Reduction_ideal. +qed. + +lemma IV_security_PRF &m: + `| Pr[Exp_IV_CPA(D, O_IV_real(E)).run() @ &m: res] + - Pr[Exp_IV_CPA(D, O_IV_ideal).run() @ &m: res] | + <= + `| Pr[Exp_NRPRF(O_NRPRF_real, R_NRPRF_IND_NRCPA(Reduction(D))).run() @ &m: res] + - Pr[Exp_NRPRF(O_NRPRF_ideal, R_NRPRF_IND_NRCPA(Reduction(D))).run() @ &m: res] | + + (q * (q - 1))%r / 2%r * mu1 drndness witness. +proof. +apply (StdOrder.RealOrder.ler_trans + (`| Pr[Exp_IND_NRCPA(O_NRCPA_real(E), Reduction(D)).run() @ &m: res] + - Pr[Exp_IND_NRCPA(O_NRCPA_ideal, Reduction(D)).run() @ &m: res] | + + (q * (q - 1))%r / 2%r * mu1 drndness witness)). ++ by apply IV_security_NR. +by rewrite (EqAdvantage_IND_NRCPA_NRPRF (Reduction(D))). +qed. + +end section. diff --git a/doc/tutorials/encryption-from-prf/Including.ec b/doc/tutorials/encryption-from-prf/Including.ec new file mode 100644 index 000000000..facc9bfcf --- /dev/null +++ b/doc/tutorials/encryption-from-prf/Including.ec @@ -0,0 +1,27 @@ +require import AllCore BitEncoding. + +require BitWord Construction. + +clone import BitWord as Bitstring with + op n <- 256 +proof gt0_n by trivial +rename + "word" as "bits" + "dunifin" as "dbits". +import DWord. + +clone import Construction as C with + type ptxt <- bits, + type nonce <- bits, + op (+) <- (+^), + op dptxt <- dbits +proof *. +realize addpA. proof. move => x y z. by rewrite xorwA. qed. +realize addpC. proof. move => x y. by rewrite xorwC. qed. +realize addKp. proof. move => x y. by rewrite xorwK xorwC xorw0. qed. +realize dptxt_ll by exact/dbits_ll. +realize dptxt_uni by exact/dbits_uni. +realize dptxt_fu by exact/dbits_fu. + + +print E. diff --git a/doc/tutorials/encryption-from-prf/context.rst b/doc/tutorials/encryption-from-prf/context.rst new file mode 100644 index 000000000..12424dffd --- /dev/null +++ b/doc/tutorials/encryption-from-prf/context.rst @@ -0,0 +1,421 @@ +Defining the Preliminaries/Context +================================== + +We will start off by defining the preliminaries and context of our +security proof, both mathematically (“pen-and-paper”) and in EasyCrypt. +This includes everything from the relevant sets and functions to the +actual scheme; this does not yet include anything regarding security. + +Defining the Basics, Pen-and-Paper +---------------------------------- + +We assume the existence of the following artifacts; these artifacts will +be used to construct the encryption scheme. - A set :math:`\mathcal{K}` +of keys called the *key space*. - A set :math:`\mathcal{P}` of +plaintexts called the *plaintext space*. - A set :math:`\mathcal{N}` of +nonces called the *nonce space*. - A set :math:`\mathcal{C}` of +ciphertexts called the *ciphertext space*. In this case, the ciphertext +space happens to be equal to the plaintext space; that is, +:math:`\mathcal{C} = \mathcal{P}`. - An associative and commutative +binary operator :math:`\oplus : \mathcal{P} + \times \mathcal{P} \rightarrow \mathcal{P}` such that +:math:`x \oplus x + \oplus y = y` for any :math:`x, y \in \mathcal{P}`. - A family of +functions +:math:`\left(f_{k} : \mathcal{N} \rightarrow \mathcal{P}\right)_{k \in \mathcal{K}}` +from nonces (in :math:`\mathcal{N}`) to plaintexts (in +:math:`\mathcal{P}`), indexed by keys (in :math:`\mathcal{K}`). - A +distribution :math:`\mathcal{D}_{\mathcal{K}}` over +:math:`\mathcal{K}`. [1]_ + +Defining the Scheme, Pen-and-Paper +---------------------------------- + +The (symmetric) encryption scheme we consider is a straightforward one; +we call it nonce-based because it uses a nonce (that it takes as an +input) to perform its encryption and decryption procedures. Formally, we +define the encryption scheme as a triple of algorithms +:math:`\mathcal{E} = \left(\mathsf{KGen}, \mathsf{Enc}, \mathsf{Dec}\right)`, +the implementations of which are provided below. + +.. math:: + + + \begin{align*} + \begin{align*} + & \underline{\smash{\mathsf{KGen}()}}\\ + & \left\lfloor~ + \begin{align*} + & k \operatorname{\smash{\overset{\$}{\leftarrow}}} \mathcal{D}_{\mathcal{K}}\\ + & \mathsf{return}\ k + \end{align*} + \right. + \end{align*} + &&&& + \begin{align*} + & \underline{\smash{\mathsf{Enc}(k, n, m)}}\\ + & \left\lfloor~ + \begin{align*} + & \mathsf{return}\ f_{k}(n) \oplus m + \end{align*} + \right.\\ + & + \end{align*} + &&&& + \begin{align*} + & \underline{\smash{\mathsf{Dec}(k, n, c)}}\\ + & \left\lfloor~ + \begin{align*} + & \textsf{return}\ f_{k}(n) \oplus c + \end{align*} + \right.\\ + & + \end{align*} + \end{align*} + +As you can see, this is a relatively basic nonce-based encryption +scheme, not containing more than a single sampling and a handful of +simple function/operator evaluations. Correctness of the scheme—that is, +whether the decryption of any encryption returns the original +message—can be seen to hold as follows. + +.. math:: + + + \begin{align*} + \forall_{k \in \mathcal{D}_{\mathcal{K}}, n \in \mathcal{N}, m \in \mathcal{M}}: + &\ \mathcal{E}.\mathsf{Dec}(k, n, \mathcal{E}.\mathsf{Enc}(k, n, m)) =\\ + &\ \mathcal{E}.\mathsf{Dec}(k, n, f_{k}(n) \oplus m) =\\ + &\ f_{k}(n) \oplus (f_{k}(n) \oplus m) =\\ + &\ f_{k}(n) \oplus f_{k}(n) \oplus m =\\ + &\ m + \end{align*} + +Here, the first two equalities are obtained by respectively replacing +the identifiers of the encryption and decryption procedures by their +specifications; the final two equalities are a consequence of the +assumed associativity and “self-inverse” properties of :math:`\oplus`. + +If you want to get an overview first before you dive into the +formalization in EasyCrypt, you can directly jump to the `paper-based +definition of the security model `__ from here. + +:::note From pen-and-paper to computer + +In standard cryptographic practice, :math:`\mathcal{K}`, +:math:`\mathcal{P}`, :math:`\mathcal{N}`, +:math:`\mathcal{D}_{\mathcal{K}}`, and :math:`\oplus` would be given +concrete definitions. In EasyCrypt, we tend to make proofs as generic as +possible, only afterward instantiating the proof with concrete types. +For example, anything we prove on the construction above will also hold +in the case where :math:`\mathcal{K} = \mathcal{N} = \{0,1\}^{\lambda}` +(for some key length :math:`\lambda`), +:math:`\mathcal{P} = \{0,1\}^{\ell}` (for some plaintext length +:math:`\ell`), :math:`\mathcal{D}_{\mathcal{K}}` is the uniform +distribution over :math:`\mathcal{K}`, and :math:`\oplus` is bitwise XOR +over :math:`\{0,1\}^{\ell}`. We will elaborate on this in a later +section. ::: + +Interlude: EasyCrypt’s Languages +-------------------------------- + +EasyCrypt provides a combination of two specification languages for the +formalization of (pen-and-paper) definitions such as the above. +Specifically, it provides the following two languages. + Expression +language. This is a polymorphic lambda calculus used to describe +mathematical structure. + :math:`\texttt{pWhile}` language. This is a +simple probabilistic imperative language used to describe any +(potentially probabilistic) program. + +Programmatic constructs in these languages are wrapped inside +*theories*. For now, to keep things simple, we will use a single +monolithic theory containing specialized definitions. At a later stage, +we will explain how developments in EasyCrypt can be split across +multiple theories, some of which can even be generalized for reuse +across multiple proofs. + +Defining the Basics, EasyCrypt +------------------------------ + +Starting from scratch, we formalize the above pen-and-paper definitions +in EasyCrypt as follows. [2]_ + +:: + + (* Types for keys, plaintexts, nonces, respectively *) + type key, ptxt, nonce. + + (* Type for ciphertexts *) + type ctxt = ptxt. + + (* Binary infix operator on plaintexts *) + op (+) : ptxt -> ptxt -> ptxt. + + (* Family of functions from nonces to plaintexts, indexed by keys *) + op f : key -> nonce -> ptxt. + + (* Subdistribution over keys *) + op dkey : key distr. + + (* Associativity, commutativity, and "self-inverse" property of the binary operator, respectively *) + axiom addpA (x y z : ptxt) : x + y + z = x + (y + z). + axiom addpC (x y : ptxt) : x + y = y + x. + axiom addKp (x y : ptxt) : x + x + y = y. + +Foremost, note that each declaration is terminated by a full stop ``.``, +which marks the end of a “formal sentence” (e.g., declarations, +definitions, axioms, lemmas, or atomic proof steps) in EasyCrypt. Let us +now discuss the various kinds of declarations that appear in this +preamble. + +:::note From pen-and-paper to computer + +On paper, we often refer to the formal description of an artifact as a +“definition”. However, when talking about the corresponding descriptions +in EasyCrypt, we deliberately make a distinction between *declarations* +and *definitions*. Intuitively, a *declaration* is a (formal) sentence +that describes some abstract artifact, but does not provide a particular +realization of this artifact. For example, most (formal) sentences in +the above snippet are declarations: they merely specify the existence of +a certain type/function/distribution, but do not specify this +type/function/distribution concretely. Contrarily, a *definition* is a +(formal) sentence that describes some artifact with a specific +realization. One can turn a declaration into a definition by providing a +realization (that still satisfies the restrictions imposed by the +declaration, e.g., the types). This can be done by either (1) directly +changing the code and appending a “=” followed by a definition to the +declaration (e.g., ``type key = int.``), or (2) cloning the theory and +providing instantiations of the abstract artifact(s). [3]_ This latter +approach will be explained at a later stage of the tutorial. ::: + +Types +~~~~~ + +First, we *declare* three *types* (which can be thought of as non-empty +sets): ``key`` (denoting :math:`\mathcal{K}`), ``ptxt`` (denoting +:math:`\mathcal{P}`) and ``nonce`` (denoting :math:`\mathcal{N}`). We +also *define* a type of ciphertexts, ``ctxt``—in this case, it is +defined to be the same as the type of plaintexts (corresponding to the +fact that :math:`\mathcal{C} = \mathcal{P}`). + +Operators and Distributions +~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Following, we *declare* the operators using the ``op`` keyword (standing +for operator). + +The first operator we declare is :math:`\oplus`, specifying we want to +use it as an infix by enclosing it in parentheses. More specifically, by +declaring the operator ``(+)``, we can subsequently use it as ``a + b`` +(where ``a`` and ``b`` are operands of the appropriate type). After the +colon, we specify the type of the declared operator; so, ``(+)`` is of +type ``ptxt -> ptxt -> ptxt``. This might strike you as strange, since +this type intuitively corresponds to a (pen-and-paper) function +:math:`\oplus : \mathcal{P} \rightarrow \mathcal{P} \rightarrow \mathcal{P}`. +However, since ``->`` is right associative, i.e., +``ptxt -> ptxt -> ptxt`` is equal to ``ptxt -> (ptxt -> ptxt)``, we have +that ``ptxt -> ptxt -> ptxt`` is actually equal to +``ptxt * ptxt -> ptxt`` (which corresponds to the pen-and-paper +:math:`\mathcal{P} \times \mathcal{P} \rightarrow \mathcal{P}`). This +translation of functions that take multiple arguments into sequences of +functions that each take a single argument is called +`currying `__. In computer-based +treatments, the curried form of the type (i.e., the type corresponding +to sequences of functions that each take a single argument) is more +customary, mainly because it eases the manipulation of individual +operands and the partial application of operators. + +As a second operator, we declare the function family :math:`f`, giving +it the ``key -> nonce -> ptxt`` type. As desired, this type intuitively +corresponds to the (pen-and-paper) set :math:`\mathcal{K} \rightarrow +(\mathcal{N} \rightarrow \mathcal{P})` of functions from nonces to +plaintexts, indexed by keys. (Note that +:math:`f : \mathcal{K} \rightarrow (\mathcal{N} \rightarrow \mathcal{P})` +is just a less fancy way of writing +:math:`\left(f_{k} : \mathcal{N} \rightarrow \mathcal{P}\right)_{k \in \mathcal{K}}`.) + +Finally, the `(sub)distribution `__ +:math:`\mathcal{D}_{\mathcal{K}}` is simply declared as a constant +``dkey`` of type ``key distr``, the type of (sub)distributions over +elements in type ``key``. [4]_ Here, ``distr`` is a so-called *type +constructor*; such constructors can be instantiated (in prefix notation) +by any type to construct another type. We discuss the details of +parameterized (or polymorphic) types at a later stage, as they are not +useful/necessary yet. + +Axioms +~~~~~~ + +With the operators declared, it remains to restrict the set of valid +candidates for :math:`\oplus` or, equivalently, state the properties we +want/assume :math:`\oplus` to satisfy. We achieve this by declaring the +appropriate *axioms*. + +More precisely, we restrict our infix ``+`` operator by declaring three +axioms, each capturing one of the properties we want :math:`\oplus` to +satisfy: ``addpC`` captures commutativity, ``addpA`` captures +associativity, and ``addKp`` captures the “self-inverse” property. + +The general shape of an axiom declaration is +``axiom < name > < parameters > : < boolean expression >.``, where the +parameters are universally quantified (typed) variables. For example, +axiom ``addpC`` formally states + +.. math:: + + + \forall x, y \in \mathcal{P}.\ x \oplus y = y \oplus x + +Interpreting Declarations +~~~~~~~~~~~~~~~~~~~~~~~~~ + +So far, we have laid down formal declarations, but how should they be +interpreted? In essence, everything in the remainder of the file +(including definitions and proofs) can be thought of as *parameterized* +by the declared artifacts. So, in this case, everything in the remainder +of the file can be applied to (and is valid for) any set of keys, +plaintext and nonces, and any operators and distributions that meet the +axioms. + +We’ll discuss how to actually instantiate constructions and proofs at a +later point. + +Defining the Scheme, EasyCrypt +------------------------------ + +With these preliminaries laid down formally, we can now use them to +formalize the (minimal) *syntax* of (symmetric) nonce-based encryption +schemes—that is, the signatures of the procedures that any such scheme +is expected to implement and, thus, can be called from other code that +has access to such a scheme by using the appropriate call statements—as +well as the specification of :math:`\mathcal{E}`. The following snippet +presents these formalizations in EasyCrypt using `module types and +modules `__. + +:: + + (* + Module type for (symmetric) nonce-based encryption schemes. + Intuitively, this specifies the interface that such + encryption schemes are expected to implement. + *) + module type NBEncScheme = { + proc kgen(): key + proc enc(k : key, n : nonce, m : ptxt): ctxt + proc dec(k : key, n : nonce, c : ctxt): ptxt + }. + + (* + Specification of the considered nonce-based encryption scheme. + Because the module implements all the procedures specified in the NBEncScheme + module type, the module has this type (making it valid to give it this type). + *) + module E : NBEncScheme = { + proc kgen() : key = { + var k; + + k <$ dkey; + + return k; + } + + proc enc(k : key, n : nonce, m : ptxt) : ctxt = { + return (f k n) + m; + } + + proc dec(k : key, n : nonce, c : ctxt) : ptxt = { + return (f k n) + c; + } + }. + +Here, we start by defining a module type called ``NBEncScheme`` which +defines the (minimal) *syntax* of nonce-based encryption schemes. More +precisely, it states that any module of type ``NBEncScheme`` *must* +implement the following three procedures (but may implement more). + +- A procedure ``kgen`` which takes no arguments and outputs a value of + type ``key``. +- A procedure ``enc`` which, given a value of type ``key``, a value of + type ``nonce`` and a value of type ``ptxt``, outputs a value of type + ``ctxt``. +- A procedure ``dec`` which, given a value of type ``key``, a value of + type ``nonce`` and a value of type ``ctxt`` produces a value of type + ``ptxt``. + +As a result, code that has access to a module of type ``NBEncScheme`` +(which may be abstract) can always call these procedures by using the +appropriate call statements. + +Surely, the above formalization of nonce-based encryption schemes +accurately captures the corresponding generic pen-and-paper definition +we gave earlier: any triple of algorithms consisting of a key generation +algorithm, taking no inputs and producing a key; an encryption +algorithm, taking a key, nonce, and plaintext, and producing a +ciphertext; and a decryption algorithm, taking a key, nonce, and +ciphertext, and producing a plaintext. + +After defining the module type, we formalize the considered encryption +scheme :math:`\mathcal{E}` as the module ``E``. As expected, this module +is of type ``NBEncScheme`` and, hence, provides an implementation of all +the procedures specified by this module type. Other code can issue calls +to these procedures; for example, the encryption procedure may be called +as ``idc <@ E.enc(idk, idn, idm)`` (or ``E.kgen(idk, idn, idm)`` when +you do not want to store the return value of the procedure), where +``idc``, ``idk``, ``idn``, and ``idm`` are identifiers for variables of +type ``ctxt``, ``key``, ``nonce``, and ``ptxt``, respectively. [5]_ In +this case, ``E`` does not implement more procedures than specified by +``NBEncScheme``, so its concrete syntax is fully captured by the generic +syntax defined by its module type. However, if ``E`` would implement +more procedures, other code would also be able to issue direct calls to +these procedures through the corresponding call statements, even though +these procedures would not be part of the module type definition. + +The procedures’ *bodies* then specify the scheme’s operation. In this +particular case, ``E.kgen`` samples a key from ``dkey``, the +formalization of distribution :math:`\mathcal{D}_{\mathcal{K}}`, into a +*local variable* ``k`` and returns this value; ``E.enc`` and ``E.dec`` +straightforwardly use ``f`` and ``+``, the formalization of +:math:`\left(f_{k} : \mathcal{N} \rightarrow \mathcal{P}\right)_{k \in \mathcal{K}}` +and :math:`\oplus`, to behave as specified mathematically. Note that, in +the syntax of expressions, spaces rather than parentheses are used to +denote operator application: ``f k n`` denotes the value obtained by +applying the operator ``f`` to ``k`` and further applying the resulting +value (an operator of type ``nonce -> ptxt``) to ``n``. Indeed, this is +where the aforementioned currying comes into play: Instead of taking a +``key``-``input`` two-tuple and returning a ``ptxt`` value, ``f`` takes +a ``key`` value and returns an operator that takes a ``nonce`` value and +returns a ``ptxt`` value. + +.. [1] + There are subtleties with this; in certain cases, we might instead + want to only assume a key generation algorithm—which may not directly + define a distribution (for example, if it involves interaction). We + keep these discussions for a subsequent tutorial. + +.. [2] + In EasyCrypt, ``(*`` and ``*)`` delimit a (potentially multi-line) + comment. + +.. [3] + Oftentimes, the realizations given to artifacts in a definition are + based on other declarations (i.e., other abstract artifacts). + Nevertheless, we refer to these as definitions since the artifact is + technically still given a realization (even though this realization + is based on other abstract artifacts). + +.. [4] + In this context, the use of the word “constant” might be a bit + confusing: Wasn’t the ``op`` keyword used to declare/define + operators? The answer is *yes, but operators are constants.* For + example, when you declare an operator ``op g : ptxt -> ctxt``, you + denote a *single, fixed* function (abstract perhaps, but fixed) from + plaintexts to ciphertexts. Surely, this is the same as defining a + (potentially abstract) constant of type ``ptxt -> ctxt``. Similarly, + we can use the ``op`` keyword to declare/define constants of any + type, including non-function types such as ``key`` or ``key distr``. + +.. [5] + When calling a module’s procedure from other code, it is not + necessary to have the identifiers of the provided arguments match the + identifiers in the syntax definition; these are merely placeholders + that may be used for documentation purposes. diff --git a/doc/tutorials/encryption-from-prf/going-further/layering-proofs.rst b/doc/tutorials/encryption-from-prf/going-further/layering-proofs.rst new file mode 100644 index 000000000..223762c0f --- /dev/null +++ b/doc/tutorials/encryption-from-prf/going-further/layering-proofs.rst @@ -0,0 +1,8 @@ +Layering Proofs: Towards Counter Mode +===================================== + +Multi-Block Plaintexts +---------------------- + +Padding and Parsing +------------------- diff --git a/doc/tutorials/encryption-from-prf/going-further/reusing-proof-components.rst b/doc/tutorials/encryption-from-prf/going-further/reusing-proof-components.rst new file mode 100644 index 000000000..e6082477a --- /dev/null +++ b/doc/tutorials/encryption-from-prf/going-further/reusing-proof-components.rst @@ -0,0 +1,492 @@ +Reusing Proof Components +======================== + +A huge advantage of using tools to machine-check cryptographic proofs +lies in their ability to argue about generic and modularized proof +elements. We can therefore easily define or reason about cryptographic +primitives and properties in a reusable way. This reusability is also +supported by EasyCrypt and therefore topic of this more advanced +tutorial. + +In the following sections, we will dive into the concept of abstract +theories in EasyCrypt and explore how they can be effectively reused in +different proofs. + +Using Reusable Definitions +-------------------------- + +In EasyCrypt we can write so-called abstract theories that for example +include formal representations of mathematical concepts (rings, groups, +…) or security definitions (CPA security, PRF assumption, …). Abstract +theories allow for the generalization of underlying primitives such that +we can reason for a whole category of the same structure. An abstract +theory does not define concrete objects unless it is instantiated in +another theory. It can then be applied to various cryptographic +scenarios, reducing the need to recreate formal definitions and proofs +for commonly used primitives. The difference between a concrete and an +abstract theory is that we cannot import an abstract theory without +copying it. This is solved by cloning abstract theories in EasyCrypt +which also allows us to set abstract types and operators in this theory +to concrete values from the theory one is currently working in. + +:: + + clone import AbstractTheory as AT with + type a <- b, + op f <- 1. + +In this tutorial, we are going to show two examples how to reuse the +abstract ``Construction`` theory that is introduced in the basic +tutorial. In contrast to the basic tutorial, we introduce most of the +definitions directly in EasyCrypt. + +Example: Nonce-Based Security of a Concrete Construction +-------------------------------------------------------- + +Until now our construction gives generic results for a nonce-based +encryption scheme without specifying the exact types or functions used +for encryption. It is straight forward to reason that if something is +secure for all types and functions fulfilling some axioms, it should be +especially secure for one specific instantiation of those types and +functions. In our case of a nonce-based encryption scheme we could for +example want to choose our plaintexts and ciphertexts to be bitstrings +of a certain length and the ``(+)`` operator to be the XOR operator. To +do so in EasyCrypt, we first need to define what a bitstring is in +general before we can have fixed length bitstrings. Luckily there exists +already an abstract theory in the standard library called ``BitWord`` +which we can use for defining strings of 256 bits. We will use the +cloning mechanism of EasyCrypt as mentioned above. Make sure you first +require the ``BitWord`` theory to make it available in your theory. + +:: + + clone import BitWord as Bitstring with + op n <- 256 + proof gt0_n by trivial + rename + "word" as "bits" + "dunifin" as "dbits". + import DWord. + +In the ``BitWord`` theory the operator n determines the length of a word +(same as a string) consisting of bits. In the instantiation we set this +operator to the specific value of 256 bits. To be able to apply the +theorems from that theory, we have to fulfill the assumptions stated for +this operator. In this case the only condition of ``n`` is to be greater +than zero. We prove the axiom ``gt0_n`` by using the ``trivial`` tactic. +The renaming to bits is more cosmetic and used to be consistent in +naming of lemmas. As last step we import the ``DWord`` theory which +makes lemmas about the distribution of bitstrings we imported available. +Those are used in the next clone to have a distribution that satisfies +all axioms for the distribution of ciphertexts. + +Additionally, we require the ``BitEncoding`` theory for the definition +of the XOR operator. With that we have all types and operators to +instantiate the nonce-based encryption scheme in the basic tutorial. + +:: + + clone import Construction as C with + type ptxt <- bits, + type nonce <- bits, + op (+) <- (+^), + op dctxt <- dbits + proof *. + realize addpA. proof. move => x y z. by rewrite xorwA. qed. + realize addpC. proof. move => x y. by rewrite xorwC. qed. + realize addKp. proof. move => x y. by rewrite xorwK xorwC xorw0. qed. + realize dctxt_ll by exact/dbits_ll. + realize dctxt_uni by exact/dbits_uni. + realize dctxt_fu by exact/dbits_fu. + +As described above we clone the ``Construction`` using ``bits`` and the +XOR operator denoted as ``(+^)``. To get an overview which assumptions +of the ``Construction`` we need to prove, we can use ``proof *`` +here. [1]_ It is not necessary to use it, but it helps to not forget +about realizing any of the assumptions and checks whether all +assumptions are consistent. In this case we get six assumptions we have +to show. The first three of them are axioms about the ``(+)`` operator +and are proven by using axioms about the XOR operator we can find in the +``BitEncoding`` theory. The latter three are the assumptions about the +distribution of ciphertexts which are exactly met by the axioms about +the distribution of bitstrings. + +Since this new definition if a scheme using bitstrings and the XOR +operator satisfies all assumptions of the ``Construction`` we get that +all proofs about the security also hold in this case. o8 + +Example: IV-Based Security from Nonce-Based Security +---------------------------------------------------- + +In the ``Construction`` we looked at the security of nonce-based +encryption guaranteeing that the nonce is not reused. The example above +illustrated how to use this abstract definition to apply the results to +a more concrete scheme. In contrast to that, this second example +instantiates the ``Construction`` in a more conceptual way to build a +bigger abstract theory about IV-based security and its relations to +nonce-based security. + +We start by defining the preliminaries for the security of IV-based +encryption schemes and giving an overview of the reasoning in the +security proof. Then we will present the detailed steps of the proof in +EasyCrypt. + +Difference between IV-Based and Nonce-Based Security +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Both IV-based and nonce-based encryption are techniques to randomize the +encryption process. The randomization is necessary to be able to ensure +the security when we encrypt multiple messages using the same key. +Instead of letting the adversary choose a nonce as input to the oracle, +the IV (Initialization Vector) is a fixed-length random value generated +inside the oracle. The encryption algorithm is not changed and expects +still a random value as input. We can illustrate the difference between +IV-based and nonce-based by looking on the real oracles (nr stands for +nonce respecting). + +.. math:: + + + \begin{align*} + \begin{align*} + & \smash{\mathcal{CPA}^{nr\textrm{-}real}_{\Sigma_{NR}}}\\ + \\ + & \begin{align*} + & \underline{\smash{\mathsf{init}()}}\\ + & \left\lfloor~ + \begin{align*} + & k \operatorname{\smash{\overset{\$}{\leftarrow}}} \Sigma_{NR}.\mathsf{KGen}()\\ + & U \leftarrow \emptyset + \end{align*} + \right. + \end{align*} + \\ + & \begin{align*} + & \underline{\smash{\mathsf{enc}(n, m)}}\\ + & \left\lfloor~ + \begin{align*} + & \textsf{if}\ n \notin U\\ + & \left\lfloor~ + \begin{align*} + & U \leftarrow U \cup \{n\}\\ + & c \leftarrow \Sigma_{NR}.\mathsf{Enc}(k, n, m)\\ + & \textsf{return}\ c + \end{align*} + \right.\\ + & \textsf{else}\\ + & \left\lfloor~ + \begin{align*} + & \textsf{return}\ \bot + \end{align*} + \right. + \end{align*} + \right. + \end{align*} + \end{align*} + &&&&&&&& + \begin{align*} + & \smash{\mathcal{CPA}^{iv\textrm{-}real}_{\Sigma_{IV}}}\\ + \\ + & \begin{align*} + & \underline{\smash{\mathsf{init}()}}\\ + & \left\lfloor~ + \begin{align*} + & k \operatorname{\smash{\overset{\$}{\leftarrow}}} \Sigma_{IV}.\mathsf{KGen}() + \end{align*} + \right. + \end{align*} + \\ + & \begin{align*} + & \underline{\smash{\mathsf{enc}(m)}}\\ + & \left\lfloor~ + \begin{align*} + & r \operatorname{\smash{\overset{\$}{\leftarrow}}} \mathcal{R}\\ + & c \leftarrow \Sigma_{IV}.\mathsf{Enc}(k, r, m)\\ + & \textsf{return}\ (r, c) + \end{align*} + \right. + \end{align*} + \end{align*} + \end{align*} + +Since the adversary is not allowed to input the randomness for the +encryption anymore, we can omit the check whether the given nonce is +unique and the initialization of the log. The randomness r is sampled +from a uniform distribution on the set :math:`\mathcal{R}` called the +*randomness space*. To make the randomness used in the encryption +accessible, we return this time both the value r and c. All changes also +apply for the ideal case. + +Definitions for IV-Based Security in EasyCrypt +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +We start the same way as in the ``Construction`` before by defining all +needed types and operators with the needed axioms in an EasyCrypt +theory. To be more precise, we reuse the same types except for the +``nonce`` type (see the code). Instead, we introduce the ``rndness`` +type and a full and uniform distribution ``drndness`` for it. Since +those types are abstract, this mainly changes the name and our +understanding. + +:: + + type rndness. + op [lossless full uniform] drndness: rndness distr. + +As mentioned before the encryption scheme does not change except for the +type of the second parameter to the ``enc`` and ``dec`` procedures that +is set to ``rndness``. Similarly, we rewrite the definitions for the +oracles, the distinguisher and the experiment to adapt to the setting of +the IV-based scheme. The interesting changes are in the oracles for the +CPA security for the IV-based encryption scheme and therefore presented +here. + +:: + + module type CPA_Oracle_IV_i = { + proc init(): unit + proc enc(m : ptxt) : rndness * ctxt + }. + + module O_IV_ideal : CPA_Oracle_IV_i = { + proc init() : unit = { + } + + proc enc(m : ptxt) : rndness * ctxt = { + var r, c; + + r <$ drndness; + c <$ dctxt; + return (r, c); + } + }. + + module O_IV_real (E : Enc_Scheme) : CPA_Oracle_IV_i = { + var k : key + + proc init() : unit = { + k <@ E.kgen(); + } + + proc enc(m : ptxt) : rndness * ctxt = { + var r, c; + + r <$ drndness; + c <@ E.enc(k, r, m); + return (r, c); + } + }. + +This corresponds to the changes we saw in the pen-and-paper version of +the section above. Since the oracle has different return values, we +first define a new module type that describes the interface of an +IV-based oracle. + +The last definition we include in this section is the instantiation of +the ``Construction``. This is crucial to be able to define a reduction +from an IV-based adversary to a nonce-based adversary in the later +sections. We clone the ``Construction`` using our new types and +operators. We especially want to match the ``nonce`` type with the new +defined ``rndness`` type in the clone. + +:: + + clone import Construction as C with + type key <- key, + type ptxt <- ptxt, + type nonce <- rndness, + op f <- f, + op (+) <- (+), + op dkey <- dkey, + op dctxt <- dctxt + proof *. + realize addpA by exact/addpA. + realize addpC by exact/addpC. + realize addKp by exact/addKp. + realize dctxt_ll by exact/dctxt_ll. + realize dctxt_uni by exact/dctxt_uni. + realize dctxt_fu by exact/dctxt_fu. + +This time the cloning of the ``Construction`` theory is straight forward +since we have formulated the same axioms for the operators in this +theory as well. Therefore, we can prove them by saying exact and then +the name of the axiom in this theory. + +Note that this does not mean we get around to prove those axioms for a +concrete instantiation. When cloning the ``IVbased`` theory to apply its +results we still need to prove all assumptions and axioms. This is why +we write this as an abstract theory as well. + +Proof Overview +~~~~~~~~~~~~~~ + +For the IV-based encryption scheme the advantage of :math:`\mathcal{D}` +distinguishing ciphertexts produced using the encryption scheme +:math:`\Sigma_{IV}` from random ciphertexts is given by: + +.. math:: + + + \mathsf{Adv}^{\mathsf{iv\textrm{-}cpa}}_{\mathcal{E}}(\mathcal{D}) + = \left|\mathsf{Pr}\left[\mathsf{Exp}^{\mathsf{iv\textrm{-}cpa}}_{\mathcal{CPA}^{\mathit{iv\textrm{-}real}}_{\Sigma_{IV}}}(\mathcal{D}): 1\right] + - \mathsf{Pr}\left[\mathsf{Exp}^{\mathsf{iv\textrm{-}cpa}}_{\mathcal{CPA}^{\mathit{iv\textrm{-}ideal}}}(\mathcal{D}): 1\right]\right| + +Our goal with this theory is to prove the relation between the IND-CPA +security of IV-based encryption schemes and nonce-based schemes. In +particular, we show that the result from the ``Construction`` implies +IV-based security. + +To make the implication more clear, we start by comparing the real +oracles. So in both the NR and the IV real oracle, we call the ``enc`` +procedure of the scheme with some random value of type ``rndness``. Note +that we set ``nonce`` to match ``rndness``. The difference is that we +did not restrict the IV to be unique. Informally, that should not +compromise the security, since the adversary has no influence on the +sampling on the randomness and the case that the same random value is +sampled is very unlikely for a large set :math:`\mathcal{R}`. We can be +more precise and say that the probability that the sampling is returning +the same value twice is bounded by the so-called Birthday bound, which +is known to be negligible for large sets. + +So with a great certainty we can assume that the random values sampled +are unique. In that case the IV-based security is directly related to +the nonce-based security since the nonces are restricted to be unique. +This gives us the following inequality we aim to prove. + +.. math:: + + + \mathsf{Adv}^{\mathsf{iv\textrm{-}cpa}}_{\mathcal{E}}(\mathcal{D}) + \leq \left|\mathsf{Pr}\left[\mathsf{Exp}^{\mathsf{nr\textrm{-}cpa}}_{\mathcal{CPA}^{\mathit{nr\textrm{-}real}}_{\Sigma_{NR}}}(\mathcal{D'}): 1\right] + - \mathsf{Pr}\left[\mathsf{Exp}^{\mathsf{nr\textrm{-}cpa}}_{\mathcal{CPA}^{\mathit{nr\textrm{-}ideal}}}(\mathcal{D'}): 1\right]\right| + + \frac{(q \cdot (q-1))}{2N} + +The last term is the Birthday bound where :math:`q` denotes the number +of oracle queries by the adversary and :math:`N` is the size of the set +:math:`\mathcal{R}`. Note that we used :math:`\mathcal{D'}` in the +nonce-based setting since :math:`\mathcal{D}` is not a nonce-respecting +CPA distinguisher. :math:`\mathcal{D'}` defines a reduction turning the +IV adversary :math:`\mathcal{D}` into a distinguisher against a +nonce-based encryption scheme :math:`\Sigma_{NR}`. + +In EasyCrypt we can state our goal that we want to show in the following +lemma. Since we do not know the number of distinct elements of type +``rndness``, we instead use the probability of drawing an element which +is implemented as ``mu1 drndness witness``. [2]_ We denote the reduction +by ``Reduction(D)``. This module which has an IV distinguisher as +parameter is presented in the reduction section. + +:: + + lemma IV_security_NR &m: + `| Pr[Exp_IV_CPA(D, O_IV_real(E)).run() @ &m: res] + - Pr[Exp_IV_CPA(D, O_IV_ideal).run() @ &m: res] | + <= + `| Pr[Exp_NR_CPA(CPA_real(E), Reduction(D)).run() @ &m: res] + - Pr[Exp_NR_CPA(CPA_ideal, Reduction(D)).run() @ &m: res] | + + (q * (q - 1))%r / 2%r * mu1 drndness witness. + +What are the steps for that in EasyCrypt to be able to prove the lemma +above? [//]: # (Will write this at the end) + +Sampling +~~~~~~~~ + +The first step we take is to import the ``Birthday`` theory to be able +to use the lemmas stated about the birthday bound. More precisely, we +clone the theory to adapt it to the types we need. The operator q is +used to denote the number of queries made to the oracle. + +Note that we write our proof inside a section to quantify all lemmas +over ``D`` - an IV distinguisher with restricted access to the memories +of oracles and the reduction. Therefore, we also use declare for the +operator ``q`` and local for the following modules and lemmas. + +:: + + declare op q : { int | 0 <= q } as ge0_q. + + local clone import Birthday as BB with + op q <- q, + type T <- rndness, + op uT <- drndness + proof *. + realize ge0_q by exact: ge0_q. + +The lemma about the birthday theory argues about an adversary against a +Sampler. [//]: # (Link to standard library) In order to apply this we +have to wrap an oracle around a sampler of the type ``Sampler``. +Therefore, we define new oracles for both the real and ideal side that +instead of sampling the randomness itself calls the sampler ``S``. The +code shows the real oracle, the ideal is defined respectively. + +:: + + local module O_IV_S_real (S: Sampler) (E: Enc_Scheme) : CPA_Oracle_IV_i = { + var k : key + + proc init() : unit = { + k <@ E.kgen(); + S.init(); + } + + proc enc(m : ptxt) : rndness * ctxt = { + var r : rndness; + var c : ctxt; + + r <@ S.s(); + c <@ E.enc(O_IV_S_real.k, r, m); + + return (r, c); + } + }. + +So the first lemma that we actually proof in EasyCrypt states that +pushing the sampling into another module as we do in this oracle is +equivalent to the original oracle. So if we have the same key as +invariant between the modules ``O_IV_real`` and ``O_IV_S_real``, and we +relate the sampled randomness (from same distribution) the behavior +should be identical. + +:: + + local lemma Sample_real &m: + Pr[Exp_IV_CPA(D, O_IV_real(E)).run() @ &m: res] = + Pr[Exp_IV_CPA(D, O_IV_S_real(Sample, E)).run() @ &m: res]. + proof. + byequiv => //. + proc; inline *. + sim (: ={k}(O_IV_real, O_IV_S_real)). + proc; inline *. + by auto. + qed. + +The lemma is stated using an equality between probability statements. +The proof works as described above. The important steps are the ``sim`` +tactic to introduce the invariant and the ``rnd`` tactic that relates +the distributions of the sampled random values. [//]: # (need to explain +sim and auto tactic (Fix EC code)) + +Reduction +~~~~~~~~~ + +Counting +~~~~~~~~ + +Security statement +~~~~~~~~~~~~~~~~~~ + +Final lemma +~~~~~~~~~~~ + +.. [1] + ``proof *.`` This line in a clone import will return all open + assumptions of the cloned theory that we have to prove. They are + displayed as a list in another buffer when using proof general in + emacs. + +.. [2] + ``mu1 dtype element`` The operator ``mu1`` is defined in the theory + of distributions in the standard library. It gives the probability to + sample the ``element`` of some type from a distribution ``dtype`` + over that type. diff --git a/doc/tutorials/encryption-from-prf/proof.rst b/doc/tutorials/encryption-from-prf/proof.rst new file mode 100644 index 000000000..4aab06db6 --- /dev/null +++ b/doc/tutorials/encryption-from-prf/proof.rst @@ -0,0 +1,1031 @@ +Proving Security +================ + +Having formalized the relevant context and the more general +security-related definitions (which, arguably, can also be considered +part of the context), we move on to the proof-specific aspects of the +formalization, culminating in the formal verification of the proof +itself. + +High-Level Proof Sketch +----------------------- + +Before diving into the details, we provide a high-level sketch or +intuition of the proof and its structure. + +Foremost, recall that our aim is to show that our symmetric nonce-based +encryption scheme is IND$-NRCPA secure as long as the function family it +uses is a NRPRF. The predominant approach to proving such a statement +*reduces* the problem of breaking the NRPRF property of the function +family *to* the problem of breaking the IND$-NRCPA security of the +encryption scheme; proofs of this type are often referred to as +*reductionist proofs*. In our case, such a proof would essentially boil +down to defining, for every adversary :math:`\mathcal{D}` against the +IND$-NRCPA security of the encryption scheme, an adversary +:math:`\mathcal{R}^{\mathcal{D}}` against the NRPRF property of the +function family that “outperforms” :math:`\mathcal{D}` (i.e., the +advantage of :math:`\mathcal{R}^{\mathcal{D}}` is greater than or equal +to the advantage of :math:`\mathcal{D}`). Then, if there would exist any +adversary that is “unacceptably effective” at breaking the IND$-NRCPA +security of the encryption scheme, it immediately follows that there +also exists an adversary that is “unacceptably effective” in breaking +the NRPRF property of the employed function family. However, since it is +assumed (or “conjectured”) that a latter such adversary does not exist, +one can conclude that a former such adversary also does not exist and, +hence, that the encryption scheme is IND$-NRCPA secure. + +As it turns out, EasyCrypt is specifically designed for the formal +verification of such reductionist proofs; for this reason, we stick to +this type of proof here. Particularly, we build a reduction adversary +(against the NRPRF property of +:math:`\left(f_{k} : \mathcal{N} \rightarrow \mathcal{P}\right)_{k \in \mathcal{K}}`) +that, given any (black-box) adversary against the IND$-NRCPA security of +:math:`\mathcal{E}`, simulates a regular run of the IND$-NRCPA +experiment in a way that allows the reduction adversary to win whenever +the given adversary “wins” the simulated run. A high-level illustration +of this dynamic is provided in the following image. + +.. figure:: reduction.jpg + :alt: alt text + + alt text + +Here, the left-hand side depicts a regular run of the IND$-NRCPA +experiment where the IND$-NRCPA adversary directly interacts with the +given NRCPA oracle; the right-hand side depicts a run of the NRPRF +experiment where the environment—particularly, oracle interactions—of +the IND$-NRCPA adversary is fully controlled by the reduction adversary, +who uses its NRPRF oracle to perfectly simulate the +environment—particularly, answers to oracle queries—in a way that +matches the environment of a regular run of the IND$-NRCPA experiment +and simultaneously allows making use of the eventual return value of the +given adversary. + +Setup and Security Statements +----------------------------- + +Prior to proving or formally verifying anything, we go over the +definition and formalization of the necessary proof-specific and +relevant security statements. Here, we take a top-down approach, +starting with the final goal and moving toward the lower-level steps. + +The Main Result: IND$-NRCPA Security +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Once again, intuitively, the end goal is to demonstrate that +:math:`\mathcal{E}` is IND$-NRCPA secure based on the assumption that +:math:`\left(f_{k} : \mathcal{N} \rightarrow \mathcal{P}\right)_{k \in \mathcal{K}}` +is a NRPRF. More formally, the end goal is to prove the following +(pen-and-paper) theorem. + +**Theorem 1.** *For all adversaries :math:`\mathcal{D}` against +IND$-NRCPA of :math:`\mathcal{E}`, there exists an adversary +:math:`\mathcal{B}` against NRPRF of +:math:`\left(f_{k} : \mathcal{N} \rightarrow \mathcal{P}\right)_{k \in \mathcal{K}}` +— with a running time close to that of :math:`\mathcal{D}` — such that +the following holds:* + +.. math:: + + + \mathsf{Adv}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\mathcal{E}}(\mathcal{D}) \leq \mathsf{Adv}^{\mathrm{NRPRF}}(\mathcal{B}) + +As alluded to before, we prove this theorem using a proof by +construction: Given any adversary :math:`\mathcal{D}` against IND$-NRCPA +security of :math:`\mathcal{E}`, we construct a reduction adversary +:math:`\mathcal{R}` against NRPRF of +:math:`\left(f_{k} : \mathcal{N} \rightarrow \mathcal{P}\right)_{k \in \mathcal{K}}` +— with a running time close to that of :math:`\mathcal{D}` — that +obtains an advantage that is *equal to* the advantage of the given +adversary. In fact, having defined such a reduction adversary, say +:math:`\mathcal{R}^{\mathcal{D}}`, the following theorem implies the one +above. + +**Theorem 2.** *For all adversaries :math:`\mathcal{D}` against +IND$-NRCPA of :math:`\mathcal{E}`, the following holds.* + +.. math:: + + + \mathsf{Adv}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\mathcal{E}}(\mathcal{D}) = \mathsf{Adv}^{\mathrm{NRPRF}}(\mathcal{R}^{\mathcal{D}}) + +In EasyCrypt, there is no notion of running time; consequently, there is +also no way to formalize the restriction “with a running time close to +that of some algorithm”. For this reason, we typically formalize +theorems akin to **Theorem 2**, where the reasonableness of the +operations performed by the considered reduction adversary (i.e., in +terms of running time) is to be manually evaluated (by humans). + +Before advancing to the formalization of **Theorem 2**, `recall that we +cannot formalize short-hands for the advantage expressions like we do on +paper `__; therefore, we +directly formalize the absolute difference in probabilities that these +advantages define. For convenience, the (pen-and-paper) definitions of +the relevant advantage expressions are restated below. + +.. math:: + + + \mathsf{Adv}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\mathcal{E}}(\mathcal{D}) + = \left|\mathsf{Pr}\left[\mathsf{Exp}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\mathcal{D}, \mathcal{O}^{CPA\textrm{-}real}_{\mathcal{E}}} = 1\right] + - \mathsf{Pr}\left[\mathsf{Exp}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\mathcal{D}, \mathcal{O}^{CPA\textrm{-}ideal}} = 1\right]\right| + +.. math:: + + + \mathsf{Adv}^{\mathrm{NRPRF}}(\mathcal{R}^{\mathcal{D}}) + = \left|\mathsf{Pr}\left[\mathsf{Exp}^{\mathrm{NRPRF}}_{\mathcal{R}^{\mathcal{D}}, \mathcal{O}^{PRF\textrm{-}real}} = 1\right] + - \mathsf{Pr}\left[\mathsf{Exp}^{\mathrm{NRPRF}}_{\mathcal{R}^{\mathcal{D}}, \mathcal{O}^{PRF\textrm{-}ideal}} = 1\right]\right| + +Here, `remember that these probability statements are only well-defined +if the initial memory/context are fixed and that, in EasyCrypt, we +explicitly indicate this initial +memory/context `__. Then, in +actuality, we want the above theorems to hold for any initial +memory/context. Apart from this explicit memory indication, the +formalization of `probability statements in +EasyCrypt `__ closely follows +the pen-and-paper definitions. Essentially, given some specific initial +memory (variable) ``&m``, we can formalize the probability expressions +by replacing all algorithms by their formalized counterparts, appending +``@ &m`` (indicating that the execution starts in memory ``&m``), +writing a colon instead of an equality sign, and formalizing the +relevant event (where the special keyword ``res`` may be used to refer +to the output of the considered procedure). For example, for some +initial memory corresponding to ``&m``, + +.. math:: \mathsf{Pr}\left[\mathsf{Exp}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\mathcal{D}, \mathcal{O}^{CPA\textrm{-}real}_{\mathcal{E}}} = 1 \right] + +is formalized as +``Pr[Exp_IND_NRCPA(O_NRCPA_real(E), D).run() @ &m : res]``. (Here, since +the output of ``Exp_IND_NRCPA(O_NRCPA_real(E), D).run()``—and, hence, +``res``—is a boolean, ``res`` is equivalent to ``res = true``.) + +Finally, theorems/lemmas are formalized `similarly to +axioms `__, merely replacing the ``axiom`` keyword by +the ``lemma`` keyword. [1]_ Combining everything, we can formalize +**Theorem 2** as follows. + +:: + + lemma EqAdvantage_IND_NRCPA_NRPRF &m: + `| Pr[Exp_IND_NRCPA(O_NRCPA_real(E), D).run() @ &m: res] + - Pr[Exp_IND_NRCPA(O_NRCPA_ideal, D).run() @ &m: res] | + = + `| Pr[Exp_NRPRF(O_NRPRF_real, R_NRPRF_IND_NRCPA(D)).run() @ &m: res] + - Pr[Exp_NRPRF(O_NRPRF_ideal, R_NRPRF_IND_NRCPA(D)).run() @ &m: res] |. + +In this lemma, ``D`` denotes the formalization of :math:`\mathcal{D}` +(i.e., an arbitrary IND$-NRCPA adversary); where and how we declare this +arbitrary/abstract module will be discussed in one of the upcoming +sections on the formal verification of the statements. Furthermore, +``R_NRPRF_IND_NRCPA(D)`` denotes the formalization of +:math:`\mathcal{R}^{\mathcal{D}}`, which we discuss imminently. + +Reduction Adversary +~~~~~~~~~~~~~~~~~~~ + +The main proof-specific artifact we must formalize is the reduction +adversary. This reduction adversary is given an IND$-NRCPA adversary but +is a NRPRF adversary itself, meaning it also gains access to a NRPRF +oracle. As touched upon in `the high-level proof +sketch `__, the crux of the argument is +that the reduction adversary perfectly simulates a run of the IND$-NRCPA +experiment for the given adversary using the NRPRF oracle in a way that +allows for the reduction adversary to win the NRPRF experiment whenever +the given adversary would have won the simulated IND$-NRCPA experiment. +Somewhat more precisely, the reduction adversary executes the given +adversary while simulating the NRCPA oracle by encrypting each of the +queried plaintexts using the values returned from the NRPRF oracle (when +querying it on the same plaintexts). If done properly, the view of the +given adversary is (distributed) exactly the same as the view it would +have in a regular run of its own experiment. Consequently, the behavior +of the given adversary—and, hence, (the distribution of) its +output—matches the behavior it would exhibit in a regular run of its own +experiment. Furthermore, since the encryptions returned to the given +adversary were constructed using the NRPRF oracle, the reduction +adversary can directly translate a correct (or incorrect) choice by the +given adversary regarding the validity of the provided encryptions into +a correct (or incorrect) choice regarding the validity of the values +provided by the NRPRF oracle. As such, the reduction adversary will +invariably be correct (and incorrect) with the exact same probability as +the given adversary, *independent of the actual implementation of the +given adversary*. + +Because the reduction adversary itself is a NRPRF adversary, we +formalize it as a module of type ``Adv_NRPRF``. To indicate that the +module formalizes the ``R``\ eduction adversary that reduces from +``NRPRF`` to ``IND_NRCPA``, we name the module ``R_NRPRF_IND_NRCPA``. +However, because a module of type ``Adv_NRPRF`` *only* expects a module +of type ``NRPRF_Oracle`` as parameter, the module parameter of type +``Adv_IND_NRCPA`` (formalizing the given IND$-NRCPA adversary) must come +first. Indeed, loosely speaking, a module is of type ``Adv_NRPRF`` *only +if* it still expects a single module parameter of type ``NRPRF_Oracle``; +if there are any other module parameters, these must first be +instantiated before the module “becomes” of type ``Adv_NRPRF``. This is +reflected in the (module) type annotations of the module definition, +provided in the snippet below. + +:: + + module (R_NRPRF_IND_NRCPA (D : Adv_IND_NRCPA) : Adv_NRPRF) (O_NRPRF : NRPRF_Oracle) = { + module O_NRCPA : NRCPA_Oracle = { + proc enc(n : nonce, m : ptxt) : ctxt option = { + var p : ptxt option; + var r : ctxt option; + + p <@ O_NRPRF.get(n); + + r <- if p = None then None else Some (oget p + m); + + return r; + } + } + + proc distinguish() : bool = { + var b : bool; + + b <@ D(O_NRCPA).distinguish(); + + return b; + } + }. + +Here, we see that the reduction adversary defines a *sub-module* +``O_NRCPA`` of type ``NRCPA_Oracle``; as the type enforces, this +sub-module implements an ``enc`` procedure. In this ``enc`` procedure, +the reduction adversary directly queries the provided NRPRF oracle +module (``O_NRPRF``) on ``n``. Subsequently, if the value ``p`` returned +by the NRPRF oracle is a failure indication, then the reduction +adversary returns a failure indication as well; else, if the value ``p`` +returned by the NRPRF oracle contains a valid plaintext, the reduction +adversary returns the ciphertext obtained by mapping this plaintext and +``m`` using the ``+`` operator. (Indeed, the ``oget`` operator takes a +value of any option type and, if the value equals ``Some x``, it returns +``x``; else, it returns an arbitrary value of the original type.) + +In its ``distinguish`` procedure, the reduction adversary uses its +sub-module as the NRCPA oracle that is exposed to the given adversary. +This formalizes the simulation of oracle interactions by the reduction +adversary for the given adversary. In the end, the reduction adversary +simply returns the value returned by the given adversary. + +Intermediate Results: Equal Probabilities in Real and Ideal Cases +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +To separate concerns, we break the main part of the proof down into two +independent pieces: equality of the “real case” probabilities and +equality of the “ideal case” probabilities. More formally, we proceed by +separately proving the following two equalities. + +.. math:: + + + \mathsf{Pr}\left[\mathsf{Exp}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\mathcal{D}, \mathcal{O}^{CPA\textrm{-}real}_{\mathcal{E}}} = 1\right] + = \mathsf{Pr}\left[\mathsf{Exp}^{\mathrm{NRPRF}}_{\mathcal{R}^{\mathcal{D}}, \mathcal{O}^{PRF\textrm{-}real}} = 1\right] + +.. math:: + + + \mathsf{Pr}\left[\mathsf{Exp}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\mathcal{D}, \mathcal{O}^{CPA\textrm{-}ideal}} = 1\right] + = \mathsf{Pr}\left[\mathsf{Exp}^{\mathrm{NRPRF}}_{\mathcal{R}^{\mathcal{D}}, \mathcal{O}^{PRF\textrm{-}ideal}} = 1\right] + +At this point, it might be good to note (and convince yourself) that the +defined reduction adversary indeed does what we want in both of the +considered cases (“real” and “ideal”); in particular, it properly +simulates the NRCPA oracle in either case. If the provided NRPRF oracle +module is the real one (``O_NRPRF_real``), then ``get(n)`` returns a +failure indication if ``n`` was already queried, and a plaintext +obtained by applying the function ``f`` to ``k`` and ``n`` otherwise. In +the former case, the reduction adversary returns a failure indication as +well. In the latter case, the reduction adversary returns a ciphertext +constructed by mapping the received plaintext and ``m`` using ``+``. +Certainly, that is equivalent to the real NRCPA oracle module +``O_NRPRF_real`` using the encryption scheme ``NBEncScheme`` to obtain +the same ciphertext given that the input and the key are the same. +Meaning that the reduction adversary perfectly simulates the real NRCPA +oracle module (O_NRCPA_real) when it is given the real NRPRF oracle +module (O_NRPRF_real). When providing the ideal oracle ``O_NRCPA_ideal`` +to the reduction adversary the intresting case is again, when the nonce +was not queried before and the ``get(n)`` procedure returns a randomly +(uniformly) sampled plaintext. Again the reduction adversary returns a +ciphertext constructed by mapping the received plaintext and ``m`` using +``+``. Since the received plaintext is uniformly distributed, it +essentially functions as a one-time pad in this mapping; hence, the +resulting ciphertext is uniformly distributed as well. Following, even +though the ideal NRCPA oracle module (``O_NRCPA_ideal``) does not +perform this mapping (but instead directly samples a ciphertext +uniformly at random and returns this), the distribution of the returned +ciphertext is identical. As a result, the reduction adversary simulates +the ideal case perfectly. + +The veracity of these equalities almost immediately follows from the +previous discussion concerning the reduction adversary. That is, in +either case, :math:`\mathcal{R}^{\mathcal{D}}` perfectly simulates the +corresponding case for :math:`\mathcal{D}`, meaning (the distribution +of) the output of :math:`\mathcal{D}` is identical to what it would be +in a run of its own game. Then, since :math:`\mathcal{R}^{\mathcal{D}}` +directly returns the value returned by :math:`\mathcal{D}`, the +probability of this value being 1 is trivially equal to the probability +of the value returned by :math:`\mathcal{D}` being 1 in a run of its own +game. + +In EasyCrypt, the equality of the “real case” probabilites is formalized +as the lemma shown in the snippet below. + +:: + + lemma EqPr_IND_NRCPA_NRPRF_real &m: + Pr[Exp_IND_NRCPA(O_NRCPA_real(E), D).run() @ &m : res] + = + Pr[Exp_NRPRF(O_NRPRF_real, R_NRPRF_IND_NRCPA(D)).run() @ &m : res]. + +Similarly, the equality of the “ideal case” probabilites is formalized +as follows. + +:: + + lemma EqPr_IND_NRCPA_NRPRF_ideal &m: + Pr[Exp_IND_NRCPA(O_NRCPA_ideal, D).run() @ &m: res] + = + Pr[Exp_NRPRF(O_NRPRF_ideal, R_NRPRF_IND_NRCPA(D)).run() @ &m: res]. + +Following `the previous discussion about lemmas in +EasyCrypt `__, these +formalizations should be relatively easy to interpret and understand. +Nevertheless, some more details including the declaration of the +arbitrary/abstract module ``D``, will be covered +`momentarily `__. + +Formal Verification +------------------- + +At last, we advance to the formal verification of the security +statements. That is, in the remainder, we go over the process of proving +the previously formalized lemmas in EasyCrypt. As before, we take a +top-down approach to the discussion, starting with the formal +verification of the main result (temporarily assuming the veracity of +the intermediate result) and only then proceeding to the formal +verfication of the intermediate lemmas. Nevertheless, before anything, +we introduce the concept of sections in Easycrypt, elucidating several +aspects that we skimmed over previously (e.g., the declaration of an +arbitrary/abstract module and the ``local`` keyword). + +Sections +~~~~~~~~ + +Oftentimes, instead of formally verifying the main result(s) at once, it +is more convenient and more manageable (both for the prover and the +reader) to first formally verify some useful auxiliary results, and then +combining these to formally verify the main result(s). These auxiliary +results are generally quite proof-specific, so much so that you wouldn’t +really want them (or any related auxiliary artifacts) to be +saved/exposed after you have used them for their specific purpose. +Furthermore, these auxiliary results frequently pertain to/quantify over +the same artifacts as the eventual main result(s) (e.g., an adversary); +it is cumbersome to repeat the precise declaration/quantification of +these artifacts over and over for each individual result. + +A useful and convenient feature of EasyCrypt that alleviates the above +issues is the (proof) section environment; this environment is delimited +by the sentences ``section X.`` and ``end section X.`` (where ``X`` is +an optional name for the section). Inside of a section, we can “declare” +modules with the desired restrictions using the ``declare`` keyword. +Afterward, we can refer to these declared modules throughout the entire +remainder of the section; without this feature, we would need to +declare/quantify these modules (and the restrictions) anew everywhere we +need to use them. In our case, all our results (both intermediate and +final) quantify over IND$-NRCPA adversaries. As such, in the beginning +of our section, we ``declare`` a module ``D`` of type ``Adv_IND_NRCPA`` +with the appropriate restrictions; see the following snippet. + +:: + + section E_IND_NR_CPA. + + declare module D <: Adv_IND_NRCPA { -O_NRCPA_real, -O_NRCPA_ideal, -O_NRPRF_real, -O_NRPRF_ideal }. + + (* Can use D anywhere here *) + + end section E_IND_NR_CPA. + +By default, any module in EasyCrypt has access to the module variables +of other modules (as well as its own, of course). This also holds for +modules that are declared in sections. However, we do not want +adversaries to have access to the state of the oracles used in the +experiments. (In pen-and-paper proofs, this is also always a given.) To +specify the modules of which a declared module may not access the +variables, we provide a a comma-separated list of the names of these +exempted modules (preceded by a ``-``) in between curly brackets +following the type annotation. + +In addition to declaring modules, a section allows us to mark +definitions of types, operators, module types, modules and lemmas as +local (using the ``local`` keyword) such that they are only accessible +inside the section (i.e., they are not exposed outside the section). As +we see +`later `__, +we mark our two intermediate lemmas as ``local``; this is because these +lemmas are proof-specific auxiliary results used to make the formal +verification of the main result more manageable. Contrarily, the lemma +for the main result is not marked as ``local`` since it is the primary +result that we would like to be available outside the section. +Nevertheless, this lemma still refers to ``D``, the module declared +inside of the section (and that is not exposed outside of the section). +As a result, after closing the section, the lemma for the main result +will be extended with the appropriate quantification over modules of +type ``Adv_IND_NRCPA`` (including the desired restrictions). + +.. _the-main-result-ind-nrcpa-security-1: + +The Main Result: IND$-NRCPA Security +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +At this point, we really have everything in place to start formally +verifying our security statements. Following a top-down approach to the +discussion, we start with the formal verification of the main result. To +this end, assume (for now) that we have already formally verified the +intermediate results and, hence, have them at our disposal in the formal +verification of the main result. + +Everytime we write down a lemma statement, we are expected to prove +(“formally verify”) the statement immediately. In fact, the tool will +not continue processing any further commands until a full proof is +provided. Once the proof is complete, the lemma is saved and is +available for us to use in any subsequent proofs. To start proving a +lemma, we write the sentence ``proof.``; to save a lemma after proving +it, we write the sentence ``qed.``. Considering the lemma for our main +result, this looks as follows. + +:: + + lemma EqAdvantage_IND_NRCPA_NRPRF &m: + `| Pr[Exp_IND_NRCPA(O_NRCPA_real(E), D).run() @ &m: res] + - Pr[Exp_IND_NRCPA(O_NRCPA_ideal, D).run() @ &m: res] | + = + `| Pr[Exp_NRPRF(O_NRPRF_real, R_NRPRF_IND_NRCPA(D)).run() @ &m: res] + - Pr[Exp_NRPRF(O_NRPRF_ideal, R_NRPRF_IND_NRCPA(D)).run() @ &m: res] |. + proof. + (* Proof *) + qed. + +Between ``proof.`` and ``qed.``, we provide the actual proof of the +considered statement. + +Throughout any proof in EasyCrypt, the tool maintains a so-called *proof +state*, a sequence of one or more *proof goals*. Each proof goal +consists of a *context* and a *conclusion*: the context contains all +locally (i.e., goal-specific) considered variables and properties +(“hypotheses”); the conclusion is a boolean expression that is to be +shown to evaluate to true. Initially, for any proof, the proof state +consist only of a single proof goal: the one corresponding to the +original lemma statement. As a proof progresses, already existing goals +change and new goals may appear. Whenever a goal’s conclusion is shown +to be true, the goal is “closed” (i.e., removed from the proof state); +after closing all goals, the proof is complete and the original lemma +may be saved. + +In interactive mode (which is practically required for developing), +EasyCrypt can display the proof state and update it as the proof +progresses. By default, only the currently considered proof goal of the +proof state (i.e., the first goal in the sequence of goals in the state) +is displayed. For example, the following is what is initially displayed +for our main result (which can be reached by processing up to and +including ``proof.``). + +:: + + Current goal + + Type variables: + + &m: {} + ---------------------------------------------------------------------------------------------- + `|Pr[Exp_IND_NRCPA(O_NRCPA_real(E), D).run() @ &m : res] + - Pr[Exp_IND_NRCPA(O_NRCPA_ideal, D).run() @ &m : res]| + = + `|Pr[Exp_NRPRF(O_NRPRF_real, R_NRPRF_IND_NRCPA(D)).run() @ &m : res] + - Pr[Exp_NRPRF(O_NRPRF_ideal, R_NRPRF_IND_NRCPA(D)).run() @ &m : res]| + +Here, everything above the dotted line is part of the goal’s context, +and everything below the dotted line is part of the goal’s conclusion. +In an initial proof goal like this one, the context always only contains +the (type) variables declared between the lemma’s name and the lemma’s +statement; indeed, in this case, this is only the memory variable +``&m``. Furthermore, the conclusion of such an initial goal always +equals the lemma’s statement. + +To go from opening the initial proof goal to closing the final proof +goal and saving the lemma, we repeatedly apply *tactics*. In essence, a +tactic represents a reasoning principle that may be applied to make +progress in a proof. EasyCrypt provides many tactics, covering a wide +range of scenarios; we will introduce and elaborate on the ones we use +in this tutorial as we go. For a comprehensive overview of the tactics +and their individual variations, consult the reference manual. + +Assuming we have access to the intermediate results (i.e., lemmas +``EqPr_IND_NRCPA_NRPRF_real`` and ``EqPr_IND_NRCPA_NRPRF_ideal``), +proving the above goal is rather straightforward: we can simply use that +the left-hand side minuend and subtrahend are respectively equal to +their right-hand side counterparts. To do so, we make use of the +``rewrite`` tactic. Given the name of a lemma/axiom that defines an +equality (say ``X = Y``), this tactic searches the current goal’s +conclusion for ``X`` and replaces it with ``Y``. Thus, in our case, +issuing ``rewrite EqPr_IND_NRCPA_NRPRF_real.`` should replace +``Pr[Exp_IND_NRCPA(O_NRCPA_real(E), D).run() @ &m : res]`` with +``Pr[Exp_NRPRF(O_NRPRF_real, R_NRPRF_IND_NRCPA(D)).run() @ &m : res]``. +Certainly, doing so changes the proof goal to the following. + +:: + + Current goal + + Type variables: + + &m: {} + ---------------------------------------------------------------------------------------------- + `|Pr[Exp_NRPRF(O_NRPRF_real, R_NRPRF_IND_NRCPA(D)).run() @ &m : res] + - Pr[Exp_IND_NRCPA(O_NRCPA_ideal, D).run() @ &m : res]| + = + `|Pr[Exp_NRPRF(O_NRPRF_real, R_NRPRF_IND_NRCPA(D)).run() @ &m : res] + - Pr[Exp_NRPRF(O_NRPRF_ideal, R_NRPRF_IND_NRCPA(D)).run() @ &m : res]| + +Subsequently issuing ``rewrite EqPr_IND_NRCPA_NRPRF_real.`` results in +the proof goal below. + +:: + + Current goal + + Type variables: + + &m: {} + ---------------------------------------------------------------------------------------------- + `|Pr[Exp_NRPRF(O_NRPRF_real, R_NRPRF_IND_NRCPA(D)).run() @ &m : res] + - Pr[Exp_NRPRF(O_NRPRF_ideal, R_NRPRF_IND_NRCPA(D)).run() @ &m : res]| + = + `|Pr[Exp_NRPRF(O_NRPRF_real, R_NRPRF_IND_NRCPA(D)).run() @ &m : res] + - Pr[Exp_NRPRF(O_NRPRF_ideal, R_NRPRF_IND_NRCPA(D)).run() @ &m : res]| + +Obviously, this goal’s conclusion is true: the right-hand side and +left-hand side are literally the same. For these kind of trivial goals, +we can use the ``trivial`` tactic to try and close the goal. Indeed, +issuing ``trivial.`` closes the goal and, since this was the only proof +goal left in the proof state, completes the proof. Everything combined, +we obtain the following for our main result. + +:: + + lemma EqAdvantage_INDNRCPA_NRPRF &m: + `|Pr[Exp_IND_NRCPA(O_NRCPA_real(E), D).run() @ &m: res] + - Pr[Exp_IND_NRCPA(O_NRCPA_ideal, D).run() @ &m: res]| + = + `|Pr[Exp_NRPRF(O_NRPRF_real, R_NRPRF_INDNRCPA(D)).run() @ &m: res] + - Pr[Exp_NRPRF(O_NRPRF_ideal, R_NRPRF_INDNRCPA(D)).run() @ &m: res]|. + proof. + rewrite EqPr_INDNRCPA_NRPRF_real. + rewrite EqPr_INDNRCPA_NRPRF_ideal. + trivial. + qed. + +To make this proof a bit cleaner, we can make use of the *tactical* +``by`` and a particular feature of the ``rewrite`` tactic. First, a +tactical combines or modifies (a sequence of) tactics in some way. In +the case of ``by``, it executes the tactic(s) directly following it and +then attempts to close the resulting goal(s) using ``trivial``. If the +goal(s) cannot be closed after applying ``trivial``, ``by`` will throw +an error. Second, rewrite can be given multiple lemma/axiom names. For +example, issuing ``rewrite Lemma1 Lemma2.``, the tactic will first +rewrite the current goal’s conclusion according to ``Lemma1``, and then +rewrite according to ``Lemma2`` in the conclusion of the goal(s) +generated by the rewriting of ``Lemma1``. Employing these features, we +can reduce the proof to the following one-liner. + +:: + + proof. + by rewrite EqPr_INDNRCPA_NRPRF_real EqPr_INDNRCPA_NRPRF_ideal. + qed. + +Intermediate Result 1: Equal Probabilities in Real Case +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +*We strongly recommend you follow the explanation in this section while +stepping through the code yourself (in interactive mode)* + +In the formal verification of the main result, we assumed that we had +already formally verified the intermediate results. Now, we actually go +over the formal verification of these intermediate results, starting +with the one concerning the equality of the “real case” probabilities. +The following snippet the corresponding lemma together with a complete +proof in EasyCrypt. Note that we declare the lemma using the keyword +``local`` as discussed `before `__. + +:: + + local lemma EqPr_IND_NRCPA_NRPRF_real &m: + Pr[Exp_IND_NRCPA(O_NRCPA_real(E), D).run() @ &m : res] + = + Pr[Exp_NRPRF(O_NRPRF_real, R_NRPRF_IND_NRCPA(D)).run() @ &m : res]. + proof. + byequiv (_ : ={glob D} ==> ={res}); trivial. + proc. + inline *. + sim (_ : ={k}(O_NRCPA_real, O_NRPRF_real) /\ ={log}(O_NRCPA_real, O_NRPRF_real)). + proc. + inline *. + auto. + qed. + +The initial sentence of the proof consists of two tactics, ``byequiv`` +and ``trivial``, combined through the tactical ``;``. Combining two +tactics by means of ``;``, as in ``t1; t2.``, first applies tactic +``t1`` to the current goal, and then applies tactic ``t2`` to the +goal(s) generated by the application of ``t1``. In our case, we combine +``byequiv`` and ``trivial`` to immediately close some of the trivial +goals generated by the application of ``byequiv``. The ``byequiv`` +tactic is more interesting. Namely, this tactic allows us to prove +certain (in)equalities of probabilities concerning program executions by +demonstrating a particular *equivalence* between the considered +programs. This equivalence of programs is always with respect to a +certain pre and postcondition, which are specified in the argument +provided to ``byequiv``; the format of this argument is +``(_ : pre ==> post)``, where ``pre`` and ``post`` respectively denote +the pre and postcondition. In our case, the precondition is +``={glob D}`` (which is syntactic sugar for +``(glob D){1} = (glob D){2}``), [2]_ i.e., we require the accessible +module variables (read: environment/view) of module ``D`` to start out +the same in both executions; the postcondition is ``={res}``, i.e., we +require the output of the programs to be (distributed) the same. +Processing this intial sentence results in a goal that precisely +corresponds to the program equivalence with this pre and postcondition. + +In the second sentence of the proof, we apply the ``proc`` tactic; this +tactic can be used on goals with a conclusion corresponding to a program +logic statement on procedure identifiers (i.e., not on actual code). The +program logics of EasyCrypt are Hoare Logic (HL), probabilistic Hoare +Logic (pHL), and probabilistic Relation Hoare Logic (pRHL). The current +goal’s conclusion denotes a pRHL statement with identifiers of +*concrete* procedures; in such a case, ``proc`` simply replaces the +identifiers by the code of the procedures. + +After applying ``proc``, we see that the code of the procedures contains +several calls to various concrete procedures. To get a better view of +what actually happens, we inline all of these concrete procedure calls +by applying the ``inline`` tactic. In particular, since we want to +inline *all* concrete procedure calls, we apply ``inline *``. (If we +wanted to inline only a particular concrete procedure call, say +``O_NRCPA_real(E).init``, we could’ve used +``inline O_NRCPA_real(E).init``.) + +Looking at the programs in the goal, we notice that they are really +quite similar. Essentially, ignoring auxiliary assignments, the only +difference is the oracle that is provided to the adversary ``D`` when +calling its (abstract) ``distinguish`` procedure. By construction, we +know that these oracles should behave identically *provided* that they +have the same keys and logs throughout the execution. For cases like +this, EasyCrypt provides the convenient higher-level ``sim`` tactic. +Reasoning backward from the end of the programs, this tactic attempts to +prove a program equivalence by keeping track of (and +extending/adjusting) a conjunction of equalities that implies the +original postcondition; if the tactic manages to work through both +programs completely, it tries to show that the original precondition +implies the final conjunction of equalities, which proves the original +equivalence. Indeed, for the current goal, it suffices to maintain the +fact that ``k`` and ``log`` of ``O_NRCPA_real`` and ``O_NRPRF_real`` are +equal throughout the execution of the programs to guarantee that the +oracles provided to ``D`` behave identically and, hence, that ``D`` +outputs the same value (distribution) in both programs as well. Although +``sim`` can be used without any arguments to let EasyCrypt infer the +invariant from the postcondition, this is not sufficient in the current +case; therefore, we provide the invariant explicitly as +``(_ : ={k}(O_NRCPA_real, O_NRPRF_real) /\ ={log}(O_NRCPA_real, O_NRPRF_real))``, +where ``={x}(M, N)`` is syntactic sugar for ``M.x{1} = N.x{2}``. +Applying the ``sim`` tactic with this invariant leaves us with a +*single* goal asking us to prove an equivalence of the ``enc`` +procedures of the oracles provided to ``D``; specifically, the goal asks +us to prove that, whenever the inputs to the oracles are the same *and* +the above invariant holds, the outputs of the oracles are (distributed) +the same *and* the invariant still holds. This shows that the +application of ``sim`` managed to close the original goal *under the +assumption that* the oracles behave identically and maintain the +invariant when called. Now, we are expected to still prove this +assumption to complete the proof. + +Once again, the current goal concerns a pRHL equivalence on concrete +procedure identifiers; so, we apply ``proc``. Then, since the resulting +code contains several calls to concrete procedure, we inline all of them +by applying ``inline *``. Considering the definition of the ``omap`` +operator, the programs are almost trivially seen to be semantically +identical. Furthermore, the code merely contains assignment statements +and if-then-else constructs. As such, this goal is a good target for +another relatively high-level tactic called ``auto``. This tactic +applies a sequence of several basic program logic tactics, afterward +solving the goal if it is trivial. In this case, ``auto`` manages to +solve the goal and, thereby, complete the proof. + +Intermediate Result 2: Equal Probabilities in Ideal Case +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +*We strongly recommend you follow the explanation in this section while +stepping through the code yourself (in interactive mode)* + +Bringing everything to a close, we discuss the formal verification of +the second intermediate result: the equality of the “ideal case” +probabilities. Here, we focus on novel (uses of) tactics that did not +occur in the previous formal verifications. The following snippet +presents the corresponding lemma along with a full proof in EasyCrypt. +Again we use the keyword ``local`` as discussed +`before `__. + +:: + + local lemma EqPr_INDNRCPA_NRPRF_ideal &m: + Pr[Exp_IND_NRCPA(O_NRCPA_ideal, D).run() @ &m: res] + = + Pr[Exp_NRPRF(O_NRPRF_ideal, R_NRPRF_INDNRCPA(D)).run() @ &m: res]. + proof. + byequiv (_ : ={glob D} ==> ={res}) => //. + proc; inline *. + wp. + call (_ : ={log}(O_NRCPA_ideal, O_NRPRF_ideal)). + - proc; inline *. + sp. + if => //. + - wp. + rnd (fun (p : ptxt) => p + m{2}). + wp. + skip => />. + move => &2 _. + split. + - move => y _. + rewrite addpK //. + move => _ c _. + rewrite addpK //. + auto. + auto. + qed. + +As in the formal verification of the first equality of probabilities, we +start off with an application of the ``byequiv`` tactic with equality on +the initial environment of ``D`` and (distribution of the) outputs as +pre and postcondition, respectively. However, instead of combining this +with the ``trivial`` tactic by means of ``;``, we append the +semantically equivalent, but slightly cleaner, ``=> //``. In EasyCrypt, +the ``=>`` can be tacked onto any (sequence of) tactic(s) to start a +sequence of so-called “introduction patterns”. In order, each of the +introduction patterns in the sequence is applied to the goal(s) +generated by the preceding (sequence of) tactic(s) and introduction +pattern(s). An important application of introduction patterns is the +*introduction* of universally quantified variables and hypothesis *from* +a goal’s conclusion *to* a goal’s context. For example, if a goal’s +conclusion starts with ``forall (i : int), ...``, the introduction +pattern ``=> j`` will remove the quantification from the goal’s +conclusion and add ``j: int`` to the goal’s context (note that the +introduced variable’s identifier does not need to match the auxiliary +identifier in the quantification). Similarly, if a goal’s conclusion +starts with, e.g., ``x <> y => ...``, then the introduction pattern +``=> H`` will remove the ``x <> y`` antecedent (and the corresponding +implication arrow) from the goal’s conclusion and add ``H: x <> y`` to +the goal’s context. In the remainder of the proof for that goal, ``H`` +is available as if it were a regular axiom/lemma. + +After applying ``byequiv``, we obtain a single goal denoting a pRHL +equivalence on procedure identifiers, as desired. We replace the +procedure identifiers with the code of the procedures and immediately +inline all calls to concrete procedures in the resulting programs by +applying ``proc; inline *``. This leaves us with two programs that are +nearly identical, only differing in the oracle provided to ``D`` and an +auxiliary assignment. Now, the right-hand side program ends in a simple +assignment; we would like to get rid of this statement so that we can +reason about and relate the abstract procedure calls on both sides +(which requires these calls to be the very last statement in both +programs). To do so, we apply the “weakest precondition” tactic, ``wp``. +In essence, this tactic consumes assignment statements from the end of +the programs while adapting the postcondition in a way that reflects the +execution of these statements; the pRHL equivalence that results from +this implies the original one. + +At this point, both programs end with a call to the same abstract +procedure, i.e., ``distinguish`` of ``D``; however, the exposed oracles +differ and the equivalence between them cannot be proven using the +``sim`` tactic. So, the main points we want to argue is that (1) the +adversary starts out with the same view/environment on both sides, and +(2) even though the provided oracles differ, their behavior is +identical. In turn, the adversary’s view—and, hence, its behavior—is the +same on both sides throughout its execution; particularly, this means +that the adversary’s output (distribution) is the same on both sides. +For this kind of reasoning, we use the ``call`` tactic in EasyCrypt. +This tactic removes the abstract procedure calls and allows us to claim +that the returned value is equally distributed on both sides. However, +to make sure this is sound, it produces two goals that formally +encompass the two previously mentioned conditions. One asks us to prove +that, right before the procedure calls are made, the environment of the +considered module (i.e., ``glob D`` in this case) is equal on both +sides; the other asks us to prove a pRHL equivalence essentially +capturing that, given the same input, the exposed oracles produce the +same output (distribution) on both sides. To assist in (or even make +possible at all) proving the latter, the ``call`` tactic takes an +invariant (as ``(_ : invariant)``) that is maintained throughout the +oracle calls. Naturally, the fact that this invariant holds at the start +*and* is maintained throughout becomes part of the goals. Indeed, all we +need as an invariant in this case is equality of the logs +(``={log}(O_NRCPA_ideal, O_NRPRF_ideal)``), guaranteeing that the +exposed oracles are synchronized with respect to failure indication. + +In the interest of keeping our code somewhat clean and readable (to +those who can understand EasyCrypt code in the first place), we indent +our proof code whenever the previous tactic application more than one +goal, hence resulting in a proof state with more goals than before the +application. (Similarly, we unindent whenever the previous tactic +application closed a goal.) In our case, since the application of +``call`` resulted in the generation of two goals, we indent the next +sentence of proof code by starting it with the indentation symbol ``-`` +and a single whitespace. This sentence will apply to the first goal +generated by ``call``, and we indent all subsequent sentences applying +to this first goal by two whitespaces. After closing this goal and +arriving at the last goal generated by ``call``, we return to the same +indentation level we used for the ``call`` tactic itself. Of course, we +use this styling rule recursively; for example, if, during the proof of +the first goal, we were to apply a tactic that again generated more than +one goal, we indent another level in the same manner as before. + +The first goal generated by the ``call`` tactic concerns the behavioral +equivalence of the exposed oracles. As per usual, we apply ``proc`` and +``inline *`` to first change this pRHL equivalence on procedure +identifiers to one on the code of the procedures, and subsequently +inlining all concrete procedure calls in this code. This leaves us with +two programs for which we want to show, among others, that their output +value (``r``) is (distributed) the same, as indicated by the ``={r}`` +term in the postcondition. Inspecting the programs (and keeping the +precondition in mind), we foremost note that the same branch of the +if-statement will be executed on both sides due to the inputs and logs +being equal. Now, if the else-branch is taken, the equality of (the +distribution of) ``r`` trivially holds; namely, ``r`` will simply be +``None`` on both sides (recall that ``omap`` outputs None if its second +argument is ``None``). However, if the then-branch is taken, the +(distributions of the) return values are not trivially identical: On the +left-hand side, the return value is the value sampled in the +then-branch; on the right-hand side, the return value is the value +obtained from mapping the value sampled in the then-branch (with the +input plaintext) using ``+``. Surely, since the sampled value +essentially functions as a one-time pad in this mapping, the +distribution of the return values is still the same on both sides; +nevertheless, this is not trivial (at least not for the tool) and, +therefore, we will need to do some more work than simply applying some +of the higher-level automated tactics. + +Following from the above, one approach to proving the current goal is +showing that (1) both sides invariably execute the same branch of the +if-statement, and (2) the equivalence holds independent of the executed +branch. Fortunately, the ``if`` tactic enables us to take this exact +approach. However, this tactic is only applicable when the if-statements +are the first statement in both programs. So, to achieve this, we need +to get rid of the assignment statement preceding the if-statement in the +right-hand side program. In turn, we achieve this by means of the +“strongest precondition” tactic, ``sp``, which is basically the dual of +``wp``. As you might have guesses, ``sp`` consumes assignment statements +from the beginning of both programs while accordingly adapting the +precondition. After applying ``sp``, we apply ``if``, and immediately +close one of the trivial goals it generates by appending ``=> //``. +Specifically, this trivial goal concerns the equivalence of the +if-guards on both sides, i.e., the fact that both sides invariably enter +the same branch; this is a trivial goal in this case because the +equality of the variables stated in the precondition makes the guards +exactly the same. Of course, the other goals generated by the ``if`` +tactic concern the veracity of the pRHL equivalence when executing the +different branches. + +Since the application of ``if => //`` generated more than one goal, we +indent the code another level, as before. The current goal is the first +goal generated by ``if => //`` and regards the equivalence of the +programs when executing the then-branch of the if-statement. Starting +off, we apply ``wp`` to consume the assignment statements at the end of +the programs; this results in both of the programs ending with a +sampling from the same distribution (recall that ``dctxt`` and ``dptxt`` +refer to the same *uniform* distribution over all +plaintexts/ciphertexts) that we want to relate somehow. Now, whenever we +want to relate samplings, we use the ``rnd`` tactic. [3]_ Oftentimes, we +use this tactic without any arguments, which essentially assumes that +the *same* value is sampled on both sides. However, sometimes, we want +to say that whenever we sample a certain value on the left-hand side, we +sample a uniquely-linked value on the right-hand side. Surely, as long +as all of the linked values have the same probability of being sampled +on each side, this is sound. For such cases, the ``rnd`` tactic takes +two more arguments that, together, form a bijection between the supports +of the considered distributions. Indeed, this bijection is what +establishes the unique link between the values from the distributions; +of course, you must then still prove that the probability of each of the +linked values in their respective distribution is identical. As some +nice syntactic sugar, whenever the bijection consists of the same +function twice, you only have to provide it once as the first argument. +Looking at the postcondition of our current goal, we see that the value +sampled on the right-hand side (``c``) should be equal to the value +sampled on the left-hand side (``y``) after combining it with the input +plaintext (``m``) using ``+``. So, if the sampling on the left-hand side +gives us ``x``, we want the sampling on the right-hand side to give us +``x + m{2}``, and vice versa. The bijection that captures this link is +defined by two identical functions, viz., ``fun (p : ptxt) => p + m{2}`` +(written as lambda/anonymous function). Therefore, we apply +``rnd (fun (p : ptxt) => p + m{2})``, which consumes the samplings and +adjust the postcondition accordingly. + +After removing the samplings, both programs only have assignments +statements left; once again, we remove these statements using ``wp``, +leaving a goal with empty programs. Now, a pRHL equivalence with empty +programs is true if, for all possible program memories (for both +programs), the precondition implies the postcondition. The ``skip`` +tactic captures this reasoning principle, and transforms a pRHL +equivalence with empty programs into the appropriate, universally +quantified implication. To make our lives a bit easier, we ask the tool +to automatically simplify the expresssion generated by ``skip`` as much +as it can; specifically, we do so using the introduction pattern +commonly referred to as “crush”, ``/>``. + +The application of ``skip => />`` produces a goal that, intuitively, +asks us to show that for any possible program memory, the bijection that +we provided to the ``rnd`` tactic is actually a bijection on the support +of the considered distribution (``dctxt`` or, equivalently, ``dptxt``). +Contemplating the experession following the universal quantification, we +see that it contains an antecedent that is useless in proving the actual +consequent (i.e., the validity of the bijection). To remove the +universal quantification as well as the useless antecedent without doing +anything else, we combine the “identity tactic” ``move`` with the +introduction patterns ``&2`` and ``_`` as ``move => &2 _``. Being the +“identity tactic”, ``move`` does absolutely nothing, but the subsequent +introduction patterns respectively introduce a program memory variable +``&2`` into the context (removing the universal quantification from the +goal’s conclusion) and remove the first (and only) antecedent from the +goal’s conclusion. + +Looking past some of the technical details (e.g., useless antecedents), +we notice that the goal we are left with basically asks us to prove same +thing twice: given any plaintext ``m``, it holds that ``x = x + m + m`` +for each plaintext ``x``. But this is just a “right self-cancellation” +property of ``+``, which we can prove generically as the following lemma +that follows directly from the axioms stated in the context. + +:: + + lemma addpK (x y : ptxt) : x + y + y = x. + proof. + by rewrite addpA addpC addKp. + qed. + +(Note that, in order to use this ``addpK`` in the current proof, it must +be saved beforehand.) With this lemma at our disposal, we continue the +proof by applying the ``split`` tactic. As its name suggests, this +tactic “splits up” a goal whose conclusion constitutes a conjunction +into two goals, each having a different term of the conjuction as its +conclusion (but the same context). We close both of the generated goals +by, first, removing universal quantification and useless antecedents as +before, and subsequently applying ``rewrite addpK //``; the latter is +syntactic sugar for ``rewrite addpK => //``. Naturally, we indent and +unindent according to the aforementioned styling rules as we go. + +The preceding closed the first goal generated by the application of +``if => //`` a while back; hence, we now arrive at the second goal +generated by this application. As discussed before, this goal +corresponds to the equivalence of the programs when the else-branch of +the if-statement executed which, because both return values equal +``None`` and the logs are not changed, is obviously true. Because the +programs merely comprise assignment statements, simply applying ``auto`` +closes the goal; we unindent and proceed to the final goal of the proof. + +Finally, we arrive at the last goal of the proof: the second goal +generated by the application of the ``call`` tactic all the way in the +beginning. Intuitively, this goal now asks us to prove that, when the +adversary is called in the original programs, (1) the environment/view +of the adversary is equal on both sides, (2) the invariant given to the +``call`` tactic holds (i.e., the oracles’ logs are equal), and (3) the +equality of (the distribution of the) return values as well as the +veracity of the invariant imply the original postcondition (i.e., the +postcondition of the goal the ``call`` tactic was applied to). Now, +first, because the equality on the adversary’s environment is assumed by +the precondition and not affected by the remaining statements of the +programs, the first proof obligation is trivial. Second, because the +remaining statements initialize the logs on both sides to the empty +list, the second proof obligation is trivial. Lastly, because the +original postcondition merely required the return value of ``D`` to be +equal on both sides, the third proof obligation is also trivial. +Concluding, since the remaining statements of the programs only concern +assignments, a simple application of ``auto`` closes the goal and +finishes the proof. + +.. [1] + Naturally, as opposed to axioms, lemmas require a proof/formal + verification; these proofs are given directly succeeding the + formalization of the lemma statement. Nevertheless, the formalization + of the statements themselves are identical between lemmas and axioms + (barring the used keyword). + +.. [2] + For the record, variables annotated with ``{1}``, as in ``x{1}``, are + given values according to the memory corresponding to the *left-hand + side* program; similarly, variables annotated with ``{2}``, as in + ``x{2}``, are given values according to the memory corresponding to + the *right-hand side* program. + +.. [3] + The samplings you want to compare should be the final statements in + the considered programs. diff --git a/doc/tutorials/encryption-from-prf/reduction.jpg b/doc/tutorials/encryption-from-prf/reduction.jpg new file mode 100644 index 000000000..4943598cb Binary files /dev/null and b/doc/tutorials/encryption-from-prf/reduction.jpg differ diff --git a/doc/tutorials/encryption-from-prf/security.rst b/doc/tutorials/encryption-from-prf/security.rst new file mode 100644 index 000000000..66f8cfadc --- /dev/null +++ b/doc/tutorials/encryption-from-prf/security.rst @@ -0,0 +1,936 @@ +Defining Security +================= + +Now that we have a scheme, we can define its security. For the time +being, EasyCrypt exclusively allows exact—rather than +asymptotic—security definitions. As such, we will only consider exact +security definitions. Furthermore, we will be a bit more generic than +necessary, starting with a definition of security for *any* symmetric +nonce-based encryption scheme, not just for the particular scheme we are +currently interested in. As alluded to before, in general, we aim to be +rather generic when formalizing and proving security in EasyCrypt. The +reason for this is that, if done properly, this can significantly +increase (and cannot decrease) the strength and reusability of the +result. Nevertheless, at this point, we will keep things somewhat more +concrete than usual for clarity purposes. Later on, we will cover +writing and reusing fully generic proof components. + +IND$-NRCPA Security for Symmetric Nonce-Based Encryption Schemes, Pen-and-Paper +------------------------------------------------------------------------------- + +For the security property, we consider INDistinguishability from RANDOM +ciphertexts under Nonce-Respecting Chosen-Plaintext Attacks +(IND$-NRCPA): An adversary with access to a chosen-plaintext +oracle—which takes a nonce and plaintext as input, outputs a ciphertext, +and does not allow for repeating nonces—should not be able to +distinguish (except with a “small” probability) the actual encryption +scheme with a fixed and properly generated secret key from an oracle +that returns freshly and uniformly sampled ciphertexts. Intuitively, +this property captures the extent to which the ciphertexts of a +(symmetric nonce-based) encryption scheme can be distinguished from +uniformly random ciphertexts: The smaller this extent, the better the +security of the scheme. For defining this indistinguishability property, +it’s crucial to ensure that nonces are not used more than once, as this +could trivially break security; indeed, if we would not impose this +restriction, the adversary could distinguish by simply reusing a nonce. + +More formally, consider the two oracles shown below, +:math:`\mathcal{O}^{CPA\textrm{-}real}_{\Sigma}` (which is defined with +respect to an abstract symmetric nonce-based encryption scheme +:math:`\Sigma`, instantiable by any concrete such scheme) and +:math:`\mathcal{O}^{CPA\textrm{-}ideal}`. + +.. math:: + + + \begin{align*} + \begin{align*} + & \underline{\smash{\mathcal{O}^{CPA\textrm{-}real}_{\Sigma}}}\\ + & \begin{align*} + & \underline{\smash{\mathsf{init}()}}\\ + & \left\lfloor~ + \begin{align*} + & k \operatorname{\smash{\overset{\$}{\leftarrow}}} \Sigma.\mathsf{KGen}()\\ + & \mathrm{log} \leftarrow [\ ] + \end{align*} + \right. + \end{align*} + \\ + & \begin{align*} + & \underline{\smash{\mathsf{enc}(n, m)}}\\ + & \left\lfloor~ + \begin{align*} + & \textsf{if}\ n \notin \mathrm{log}\\ + & \left\lfloor~ + \begin{align*} + & \mathrm{log} \leftarrow n\ ||\ \mathrm{log}\\ + & c \leftarrow \Sigma.\mathsf{Enc}(k, n, m)\\ + & \textsf{return}\ c + \end{align*} + \right.\\ + & \textsf{else}\\ + & \left\lfloor~ + \begin{align*} + & \textsf{return}\ \bot + \end{align*} + \right. + \end{align*} + \right. + \end{align*} + \end{align*} + &&&&&&&& + \begin{align*} + & \underline{\smash{\mathcal{O}^{CPA\textrm{-}ideal}}}\\ + & \begin{align*} + & \underline{\smash{\mathsf{init}()}}\\ + & \left\lfloor~ + \begin{align*} + & \\ + & \mathrm{log} \leftarrow [\ ] + \end{align*} + \right. + \end{align*} + \\ + & \begin{align*} + & \underline{\smash{\mathsf{enc}(n, m)}}\\ + & \left\lfloor~ + \begin{align*} + & \textsf{if}\ n \notin \mathrm{log}\\ + & \left\lfloor~ + \begin{align*} + & \mathrm{log} \leftarrow n\ ||\ \mathrm{log}\\ + & c \operatorname{\smash{\overset{\$}{\leftarrow}}} \mathcal{U}_{\mathcal{C}}\\ + & \textsf{return}\ c + \end{align*} + \right.\\ + & \textsf{else}\\ + & \left\lfloor~ + \begin{align*} + & \textsf{return}\ \bot + \end{align*} + \right. + \end{align*} + \right. + \end{align*} + \end{align*} + \end{align*} + +Evidently, these oracles are extremely similar: The only difference +between the two concerns the creation of ciphertexts (and the +corresponding initialization differences). Then, we capture the +“insecurity” of a (symmetric nonce-based) encryption scheme +:math:`\Sigma` against a nonce-respecting chosen-plaintext distinguisher +:math:`\mathcal{D}`—i.e., a (potentially probabilistic) algorithm +:math:`\mathcal{D}` with the appropriate interface—as the (absolute) +difference between the likelihood of (1) :math:`\mathcal{D}` outputting +:math:`\texttt{true}` when given access to (the :math:`\mathsf{enc}` +procedure of) :math:`\mathcal{O}^{CPA\textrm{-}real}_{\Sigma}` and (2) +:math:`\mathcal{D}` outputting :math:`\texttt{true}` when given access +to (the :math:`\mathsf{enc}` procedure of) +:math:`\mathcal{O}^{CPA\textrm{-}ideal}`. Conceptually, the truth value +output by the distinguisher can be interpreted as the distinguisher’s +“guess” of which oracle it was given. In general terms, this (absolute) +difference is often called *the advantage of :math:`\mathcal{D}` in +distinguishing :math:`\Sigma` from random*; however, since we have +already established a slick name for the exact security property, we +will be more precise and refer to it as *the advantage of +:math:`\mathcal{D}` against IND$-NRCPA of :math:`\Sigma`*. +Mathematically, this advantage is expressed as follows. + +.. math:: + + + \mathsf{Adv}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\Sigma}(\mathcal{D}) + = \left|\mathsf{Pr}\left[\mathsf{Exp}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\mathcal{D}, \mathcal{O}^{CPA\textrm{-}real}_{\Sigma}} = 1\right] + - \mathsf{Pr}\left[\mathsf{Exp}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\mathcal{D}, \mathcal{O}^{CPA\textrm{-}ideal}} = 1\right]\right| + +Here, the experiment + +.. math:: \mathsf{Exp}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\mathcal{D}, \mathcal{O}} + +\ is defined below. This experiment is rather straightforward: It +initializes the given oracle, runs the distinguisher while providing +access to the :math:`\mathsf{enc}` function of the oracle, and directly +outputs the return value received from the distinguisher. + +.. math:: + + + \begin{align*} + & \underline{\smash{\mathsf{Exp}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\mathcal{D}, \mathcal{O}}}}\\ + & \left\lfloor + \begin{align*} + & \mathcal{O}.\mathsf{init}()\\ + & b \operatorname{\smash{\overset{\$}{\leftarrow}}} \mathcal{D}^{\mathcal{O}.\mathsf{enc}}.\mathsf{distinguish}()\\ + & \textsf{return}\ b + \end{align*} + \right. + \end{align*} + +Surely, with these oracle and game definitions, + +.. math:: \mathsf{Adv}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\Sigma}(\mathcal{D}) + +matches the intuitive description of insecurity we gave earlier. Namely, +because + +.. math:: \mathsf{Exp}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\mathcal{D}, \mathcal{O}^{CPA\textrm{-}real}_{\Sigma}} + +and + +.. math:: \mathsf{Exp}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\mathcal{D}, \mathcal{O}^{CPA\textrm{-}ideal}} + +merely differ in the oracle they provide to :math:`\mathcal{D}`, a +difference in probability of :math:`\mathcal{D}` outputting a certain +truth value (arbitrarily chosen to be 1, or :math:`\texttt{true}`, here) +between the experiments must be a consequence of distinguishing the +oracles somehow. Certainly, this is precisely what + +.. math:: + + \left|\mathsf{Pr}\left[\mathsf{Exp}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\mathcal{D}, \mathcal{O}^{CPA\textrm{-}real}_{\Sigma}} = 1\right] - + \mathsf{Pr}\left[\mathsf{Exp}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\mathcal{D}, \mathcal{O}^{CPA\textrm{-}ideal}} = 1\right]\right| + +captures. + +Finally, we say that a (symmetric nonce-based encryption) scheme +:math:`\Sigma` is IND$-NRCPA secure if, for any nonce-respecting +chosen-plaintext adversary :math:`\mathcal{D}`, + +.. math:: \mathsf{Adv}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\Sigma}(\mathcal{D}) + +\ is “small”. Because we exclusively consider exact security, “small” +essentially means “bounded by other *concrete values/probabilities* that +we believe are small in practice”. + +To directly read further on the security definitions of PRFs for the pen +and paper setting, jump +`here <#nonce-respecting-pseudo-random-function-family-property-pen-and-paper>`__. + +IND$-NRCPA Security for Symmetric Nonce-Based Encryption Schemes, EasyCrypt +--------------------------------------------------------------------------- + +To formalize the above-discussed oracles, adversary class, and +experiment in EasyCrypt, we will make use of `module types and +modules `__, as +well as several libraries from the *standard library*. Specifically, we +will make use of the ``AllCore.ec``, ``List.ec``, and ``Distr.ec`` +libraries for the definitions and properties of basic concepts, lists, +and distributions, respectively. To have those theories available, we +issue the following command at the beginning of the file. + +:: + + require import AllCore List Distr. + +The keyword ``require`` loads the content of a library and the +``import`` keyword makes all the symbols available without +qualification. For more information regarding loading and importing, +`click here `__. + +NRCPA Oracle Type +~~~~~~~~~~~~~~~~~ + +Before formalizing the oracles, we will formalize their type. From the +pen-and-paper definition of the oracles, we can see that they implement +two algorithms: + +.. math:: \mathsf{init()} + +\ and + +.. math:: \mathsf{enc}(n, m) + +, where + +.. math:: n + +is a nonce, + +.. math:: m + +is a plaintext, and + +.. math:: \mathsf{enc}(n, m) + +outputs either a valid ciphertext or an indication of failure ( + +.. math:: \bot + +). The module type that captures this is shown below. + +:: + + module type NRCPA_Oraclei = { + proc init() : unit + proc enc(n : nonce, m : ptxt) : ctxt option + }. + +Here, notice that the procedures’ output types. First, the output type +of ``init`` is ``unit``, which is a built-in type that only contains a +single value. Among others, this type is used as the type of the return +value of procedures that do not return an actual value. Certainly, we do +not expect the initialization procedure of a NRCPA oracle to return +anything; as such, we use ``unit`` to denote its output type. Second, +the output type of ``enc`` is ``ctxt option`` (instead of the ``ctxt`` +type you might have expected). ``option`` is an example of a *type +constructor* (as is ``distr``, which we briefly mentioned +`earlier `__). Such constructors +can be used to construct types by instantiating them (using prefix +notation) with already-existing types. In the specific case of +``option``, any type—say ``t``—can be used to create a corresponding +option type that is denoted by ``t option``. This option type contains a +value ``Some x`` for each value ``x`` of type ``t``, and an additional +value ``None``. In the formalization of the oracles, we use the +``ctxt option`` type as a convenient way to let ``enc`` return either a +valid ciphertext (as ``Some c`` where ``c`` is a ciphertext) or an +indication of failure (as ``None``). + +Real NRCPA Oracle +~~~~~~~~~~~~~~~~~ + +Next, we formalize + +.. math:: \mathcal{O}^{CPA\textrm{-}real}_{\Sigma} + +, the real oracle. Particularly, we do so using a module of type +``NRCPA_Oraclei``. However, in contrast to the encryption scheme we +formalized as a module +`before `__, + +.. math:: \mathcal{O}^{CPA\textrm{-}real}_{\Sigma} + +is defined with respect to some other entity :math:`\Sigma` from a +certain class; in this case, this is the class of symmetric nonce-based +encryption schemes. In EasyCrypt, we formalize this using a so-called +`functor or higher-order +module `__—i.e., +a module parameterized on other module(s)—that takes a module of the +type that represents this class; indeed, here this is the +`previously-defined `__ +``NBEncScheme`` module type. So, we can formalize + +.. math:: \mathcal{O}^{CPA\textrm{-}real}_{\Sigma} + +as follows. + +:: + + module O_NRCPA_real (S : NBEncScheme) : NRCPA_Oraclei = { + var k : key + var log : nonce list + + proc init() : unit = { + k <@ S.kgen(); + + log <- []; + } + + proc enc(n : nonce, m : ptxt) : ctxt option = { + var c : ctxt; + var r : ctxt option; + + if (! (n \in log)) { + log <- n :: log; + + c <@ S.enc(k, n, m); + + r <- Some c; + } else { + r <- None; + } + + return r; + } + }. + +Intuitively, the definition of ``O_NRCPA_real`` can be interpreted as +follows: Given any scheme ``S`` that implements the expected procedures +(or minimal syntax) of a symmetric nonce-based encryption scheme, we can +construct a NRCPA oracle by implementing the expected procedures (or +minimal syntax) in the following way, using (the expected procedures of) +``S``. Certainly, this means that the procedures of ``O_NRCPA_real`` can +formally only be given a meaning (and, hence, be referred/called from +other code) if the module parameter is instantiated. In other words, +``O_NRCPA_real.init`` and ``O_NRCPA_real.enc`` are not well-defined +procedures, but ``O_NRCPA_real(M).init`` and ``O_NRCPA_real(M).enc`` are +(where ``M`` is a module of type ``NBEncScheme``). Contrarily, the +module variables of ``O_NRCPA_real`` (i.e., ``k`` and ``log``) are +independent of the instantiation of its module parameter: there is only +ever one ``O_NRCPA_real.k`` and one ``O_NRCPA_real.log``, even if +``O_NRCPA_real`` is instantiated multiple times with different modules. +Therefore, it is possible to refer to ``O_NRCPA_real.k`` and +``O_NRCPA_real.log``, but not to ``O_NRCPA_real(M).k`` and +``O_NRCPA_real(M).log`` (again, where ``M`` is a module of type +``NBEncScheme``). + +:::note From pen-and-paper to computer Looking at the actual code of +``O_NRCPA_real``, we can see that it is a relatively straightforward +translation from the pen-and-paper definition of which the novel +concepts may seem rather self-explanatory. Regardless, we briefly go +over these concepts for clarity and completeness. + ``list`` is a type +constructor (defined in ``List.ec``) that can be used to construct the +type of lists over a certain type. In other words, for any type ``t``, +``t list`` is the type of lists containing elements of type ``t``. + +``[]`` is a value (defined in ``List.ec``) that denotes the empty list. ++ ``\in`` is an abbreviation (defined in ``List.ec``) that can be used +an infix operator, and checks whether the left-hand side operand (of +some type, say ``t``) is an element of the right-hand side operand (of +type ``t list``). + ``::`` is an infix operator (defined in ``List.ec``) +that prepends the left-hand side operand (of some type, say ``t``) to +the right-hand side operand (of type ``t list``). + In EasyCrypt, +procedures can only have a single return statement. The main reason for +this is to keep the complexity of the program logics (used for proofs) +somewhat in check. For this reason, to formalize procedures that contain +multiple return statements, we accordingly replace all return statements +by assignments to a return variable and a single return statement at the +end. ::: + +Ideal NRCPA Oracle +~~~~~~~~~~~~~~~~~~ + +Having dealt with the formalization of + +.. math:: \mathcal{O}^{CPA\textrm{-}real}_{\Sigma} + +, we continue with the formalization of + +.. math:: \mathcal{O}^{CPA\textrm{-}ideal} + +. Certainly, as one would expect from the pen-and-paper definitions, the +latter essentially only differs from the former in that it samples +ciphertexts uniformly at random instead of legitimately generating them +(i.e., via an actual encryption scheme). As a result, the module +formalizing the ideal oracle does not need to be parameterized on +another module (representing an actual encryption scheme), nor does it +need to maintain a secret key. However, it does require a uniform +distribution over the complete ciphertext space to sample from. So, +before formalizing the oracle, we need to define this distribution; we +do so as follows. + +:: + + op [lossless full uniform] dctxt : ctxt distr. + +In this code, we define a (sub)distribution ``dctxt`` over the ``ctxt`` +type, similar to how we defined the (sub)distribution ``dkey`` over the +``key`` type `before `__. +However, in contrast to ``dkey``, ``dctxt`` is assumed to have several +properties, each of which is denoted by one of the keywords in the +square brackets. First, we assume ``dctxt`` to be ``lossless``; that is, +we assume ``dctxt`` is proper distribution (the sum of its probabilities +exactly equals 1). Second, we assume ``dctxt`` to be ``full``; that is, +we assume ``dctxt`` assigns a non-zero probability to each value of type +``ctxt``. Lastly, we assume ``dctxt`` to be ``uniform``; that is, we +assume ``dctxt`` assigns either a probability of 0 or a constant +probability to each value of type ``ctxt`` (this constant probability is +the same for all values). Note that the combination of the ``full`` and +``uniform`` properties mean that ``dctxt`` assigns the same non-zero +probability to each value of type ``ctxt``. Adding the ``lossless`` +property on top of this results in ``dctxt`` assigning each value of +type ``ctxt`` a probability of + +.. math:: 1 / \left| \mathcal{C} \right| + +(where + +.. math:: \left| \mathcal{C} \right| + +denotes the cardinality of the ciphertext space). In other words, +combining the ``lossless``, ``full``, and ``uniform`` properties results +in the distribution that is usually referred to as the “uniform +distribution”. For more information about distributions in EasyCrypt, +`click here `__. + +Having the required ciphertext distribution at our disposal, we can go +ahead and formalize the ideal oracle. As mentioned before, this +formalization is essentially identical to the formalization of the real +oracle, merely replacing the legitimate generation of ciphertexts by the +appropriate sampling operation (and, of course, removing anything +related to the legitimate generation of ciphertext, as this is +redundant). More precisely, we formalize + +.. math:: \mathcal{O}^{CPA\textrm{-}ideal} + +\ as the module given below. + +:: + + module O_NRCPA_ideal : NRCPA_Oraclei = { + var log : nonce list + + proc init() : unit = { + log <- []; + } + + proc enc(n : nonce, m : ptxt) : ctxt option = { + var c : ctxt; + var r : ctxt option; + + if (! (n \in log)) { + log <- n :: log; + + c <$ dctxt; + + r <- Some c; + } else { + r <- None; + } + + return r; + } + }. + +IND$-NRCPA Experiment and Security +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +At this point, it remains to formalize the considered class of +adversaries and security experiment before finally being able to +formalize the security property of a (symmetric nonce-based) encryption +scheme :math:`\Sigma`. + +Starting off, recall that a class of adversaries contains any (possibly +probabilistic) algorithm that implements a certain interface, +potentially requiring access to a number of oracles. Notice that if we +would be able to specify access to modules of other types in a module +type, adversary classes (with potential oracle access) could easily be +formalized using module types. Namely, the only requirement for a module +``A`` to be of a certain module type ``AT`` is that ``A`` implements the +procedures defined by ``AT``; otherwise, there are no restrictions on +``A``. Indeed, this precisely matches our concept of (a class of) +adversaries: All algorithms that satisfy the expected interface +constitute valid adversaries and, hence, belong to the considered class +of adversaries. So, to formalize a class of adversaries that do not +expect access to any oracle, it suffices to use module types as we have +already gone over before. However, to formalize a class of adversaries +that does expect access to an oracle(s), we require some additional +functionality. Fortunately, EasyCrypt allows for module types that, in +addition to specifying a set of procedures that is to be implemented, +also indicate a sequence of module parameter(s), so-called `functor +types or higher-order module +types `__. + +Applying the above to our currently case, we first create a module type +formalizing the interface of the NRCPA oracles provided *to the +adversaries*. This is necessary because ``NRCPA_Oraclei``, the module +type formalizing the interface of the NRCPA oracles given *to the +experiment*, include the ``init`` procedure, which we do not want to +expose to the adversaries. Therefore, we create a separate module type +for the oracles actually given to the adversary; indeed, this type +should only specify the ``enc`` procedure of the ``NRCPA_Oraclei`` type. +Luckily, EasyCrypt allows for the direct inclusion of procedure +signatures from other module types, so we do not have to copy-paste; see +the snippet below. + +:: + + module type NRCPA_Oracle = { + include NRCPA_Oraclei [enc] + }. + +Using this newly defined module type, we can formalize the class of +adversaries with a module type as follows. + +:: + + module type Adv_IND_NRCPA (O : NRCPA_Oracle) = { + proc distinguish() : bool + }. + +Intuitively, the ``Adv_IND_NRCPA`` module type encompasses all modules +that expect a module of type ``NRCPA_Oracle`` and, *after* being given +such a module, implement ``distinguish`` procedure that takes no input +and outputs a value of type ``bool`` (i.e., a boolean). + +Based on the above, we can formalize the IND$-NRCPA experiment/game, +which is nothing more than a (probabilistic) program that is defined +with respect to a NRCPA oracle and an IND$-NRCPA adversary. In EasyCrypt +terms, the IND$-NRCPA experiment/game is a module that takes two module +parameters: one of type ``NRCPA_Oraclei`` and one of type +``Adv_IND_NRCPA``. Here, a technicality is that—because EasyCrypt allows +code to be written exclusively inside of procedures—we must encapsulate +the actual code of the experiment/game in a procedure (which we +arbitrarily name ``run``), even though there is no corresponding +(explicit) procedure/algorithm signature in the pen-and-paper +definition. Otherwise, the formalization, provided in the following +snippet, is a verbatim translation of the pen-and-paper definition. + +:: + + module Exp_IND_NRCPA (O : NRCPA_Oraclei) (D : Adv_IND_NRCPA) = { + proc run() : bool = { + var b : bool; + + O.init(); + + b <@ D(O).distinguish(); + + return b; + } + }. + +At last, we can express the advantage of an (IND$-NRCPA) adversary +:math:`\mathcal{D}` against IND$-NRCPA of a symmetric nonce-based +encryption scheme :math:`\Sigma`. Recall that the pen-and-paper +definition of this advantage is the following. + +.. math:: + + + \mathsf{Adv}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\Sigma}(\mathcal{D}) + = \left|\mathsf{Pr}\left[\mathsf{Exp}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\mathcal{D}, \mathcal{O}^{CPA\textrm{-}real}_{\Sigma}} = 1\right] + - \mathsf{Pr}\left[\mathsf{Exp}^{\mathrm{IND\$\textrm{-}NRCPA}}_{\mathcal{D}, \mathcal{O}^{CPA\textrm{-}ideal}} = 1\right]\right| + +Formally, these probability expressions are not fully defined unless the +initial memory/context is fixed. More precisely, the experiment only +defines a distribution over its (state and) output value—which allows us +to talk about things such as the probability of the output of the +experiment being 1—if the initial memory is fixed; otherwise, it would +define a set of distributions (one distribution for each possible +initial memory). To keep flexibility in reasoning, EasyCrypt makes the +choice of letting programs run in arbitrary initial memories, and those +need to be specified as part of the probability statements/advantages. +At present, it is impossible to define operators that are parameterized +by memories in EasyCrypt, and we must always explicitly write out the +advantage expressions when they are present. This means that the +advantage expressions will only be formalized within the formalization +of the corresponding security statements. For this reason, we postpone +the discussion concerning the formalization of the advantage expressions +to when we start formalizing the relevant security statements. + +“Nonce-Respecting” Pseudo-Random Function Family Property, Pen-and-Paper +------------------------------------------------------------------------ + +In cryptography, it is common to base security of a scheme on +computational hardness assumptions that can somehow be linked to (parts +of) the scheme; we also do this here. Particularly, we base the +IND$-NRCPA security of + +.. math:: \mathcal{E} + +\ on the (assumed) “Nonce-Respecting” Pseudo-Random Function family +(NRPRF) property [1]_ of the function family used to map nonces to +plaintexts (i.e., + +.. math:: \left(f_{k} : \mathcal{N} \rightarrow \mathcal{P}\right)_{k \in \mathcal{K}} + +). Intuitively, this property captures the extent to which an (unknown) +random function from the function family is indistinguishable from a +truly random function of the same type (i.e., from nonces to plaintexts) +by observing the outputs corresponding to unique/non-repeating inputs. + +More formally, consider the two oracles given below, +:math:`\mathcal{O}^{PRF\textrm{-}real}` and +:math:`\mathcal{O}^{PRF\textrm{-}ideal}`. [2]_ + +.. math:: + + + \begin{align*} + \begin{align*} + & \underline{\smash{\mathcal{O}^{PRF\textrm{-}real}}}\\ + & \begin{align*} + & \underline{\smash{\mathsf{init}()}}\\ + & \left\lfloor~ + \begin{align*} + & k \operatorname{\smash{\overset{\$}{\leftarrow}}} \mathcal{D}_{\mathcal{K}}\\ + & \mathrm{log} \leftarrow [\ ] + \end{align*} + \right. + \end{align*} + \\ + & \begin{align*} + & \underline{\smash{\mathsf{get}(n)}}\\ + & \left\lfloor~ + \begin{align*} + & \textsf{if}\ n \notin \mathrm{log}\\ + & \left\lfloor~ + \begin{align*} + & \mathrm{log} \leftarrow n\ ||\ \mathrm{log}\\ + & m \leftarrow f_k(n)\\ + & \textsf{return}\ m + \end{align*} + \right.\\ + & \textsf{else}\\ + & \left\lfloor~ + \begin{align*} + & \textsf{return}\ \bot + \end{align*} + \right. + \end{align*} + \right. + \end{align*} + \end{align*} + &&&&&&&& + \begin{align*} + & \underline{\smash{\mathcal{O}^{PRF\textrm{-}ideal}}}\\ + & \begin{align*} + & \underline{\smash{\mathsf{init}()}}\\ + & \left\lfloor~ + \begin{align*} + & \\ + & \mathrm{log} \leftarrow [\ ] + \end{align*} + \right. + \end{align*} + \\ + & \begin{align*} + & \underline{\smash{\mathsf{get}(n)}}\\ + & \left\lfloor~ + \begin{align*} + & \textsf{if}\ n \notin \mathrm{log}\\ + & \left\lfloor~ + \begin{align*} + & \mathrm{log} \leftarrow n\ ||\ \mathrm{log}\\ + & m \operatorname{\smash{\overset{\$}{\leftarrow}}} \mathcal{U}_{\mathcal{P}}\\ + & \textsf{return}\ m + \end{align*} + \right.\\ + & \textsf{else}\\ + & \left\lfloor~ + \begin{align*} + & \textsf{return}\ \bot + \end{align*} + \right. + \end{align*} + \right. + \end{align*} + \end{align*} + \end{align*} + +As we can see, :math:`\mathcal{O}^{PRF\textrm{-}real}` and +:math:`\mathcal{O}^{PRF\textrm{-}ideal}` effectively only differ in the +way they create plaintexts: The former creates plaintexts by mapping the +provided nonces with a random function (that is fixed during +initialization) from +:math:`\left(f_{k} : \mathcal{N} \rightarrow \mathcal{P}\right)_{k \in \mathcal{K}}`; +the latter creates plaintexts by sampling them uniformly at random, +independent of the provided nonces. Then, akin to what we did for +IND$-NRCPA security, we define the advantage of a nonce-respecting +pseudo-random function distinguisher :math:`\mathcal{D}` against +:math:`\left(f_{k} : \mathcal{N} \rightarrow \mathcal{P}\right)_{k \in \mathcal{K}}` +as the following (absolute) difference. + +.. math:: + + + \mathsf{Adv}^{\mathrm{NRPRF}}(\mathcal{D}) + = \left|\mathsf{Pr}\left[\mathsf{Exp}^{\mathrm{NRPRF}}_{\mathcal{D}, \mathcal{O}^{PRF\textrm{-}real}} = 1\right] + - \mathsf{Pr}\left[\mathsf{Exp}^{\mathrm{NRPRF}}_{\mathcal{D}, \mathcal{O}^{PRF\textrm{-}ideal}} = 1\right]\right| + +In this equation, +:math:`\mathsf{Exp}^{\mathrm{NRPRF}}_{\mathcal{D}, \mathcal{O}}` refers +to the experiment defined below. + +.. math:: + + + \begin{align*} + & \underline{\smash{\mathsf{Exp}^{\mathrm{NRPRF}}_{\mathcal{O}}(\mathcal{D})}}\\ + & \left\lfloor + \begin{align*} + & \mathcal{O}.\mathsf{init}()\\ + & b \operatorname{\smash{\overset{\$}{\leftarrow}}} \mathcal{D}^{\mathcal{O}.\mathsf{get}}.\mathsf{distinguish}()\\ + & \textsf{return}\ b + \end{align*} + \right. + \end{align*} + +Notice that this experiment takes the exact same approach as the one we +defined for IND$-NRCPA security: The only difference between these +experiments concerns the class of adversaries and the class of oracles +they consider. + +Lastly, we say that +:math:`\left(f_{k} : \mathcal{N} \rightarrow \mathcal{P}\right)_{k \in \mathcal{K}}` +is a NRPRF if, for any nonce-respecting pseudo-random function family +adversary :math:`\mathcal{D}`, +:math:`\mathsf{Adv}^{\mathrm{NRPRF}}(\mathcal{D}`) is “small”. Again, +because we only consider exact security, “small” basically means +“bounded by other *concrete values/probabilities* that we believe are +small in practice”. + +Again, if you are interested in seeing the paper-based security proof +before diving into the EasyCrypt formalization, you can read further on +the `proving security part `__. + +“Nonce-Respecting” Pseudo-Random Function Family Property, EasyCrypt +-------------------------------------------------------------------- + +Evidently, on a conceptual level, the definitions for IND$-NRCPA and +NRPRF experiment and oracles are almost identical. Accordingly, the +corresponding EasyCrypt formalization are also going to be almost +identical. As such, we go over the formalization of NRPRF at a faster +pace, primarily highlighting the differences with the formalization of +IND$-NRCPA and reiterating important aspects. The preceding material +discussing IND$-NRCPA most likely contains explanations of +subjects/concepts left untouched here. + +NRPRF Oracle Type +~~~~~~~~~~~~~~~~~ + +Once again, we start by defining the type for the oracles; as before, we +do so using a module type that specifies a procedure signature for each +algorithm defined expected to be implemented by NRPRF oracles. Looking +at the definitions of :math:`\mathcal{O}^{PRF\textrm{-}real}` and +:math:`\mathcal{O}^{PRF\textrm{-}ideal}`, we can see what (type of) +algorithms these are. The following snippet presents the corresponding +formalization. + +:: + + module type NRPRF_Oraclei = { + proc init() : unit + proc get(n : nonce) : ptxt option + }. + +Real NRPRF Oracle +~~~~~~~~~~~~~~~~~ + +Using the newly defined module type, we formalize the real NRPRF oracle +using a (by now) straightforward translation from the pen-and-paper +definition; see the snippet below. Recall that an EasyCrypt procedure +can only have one ``return`` statement, which is why we employ a return +variable instead of having multiple ``return`` statements. Furthermore, +remember that, since we are using an ``option`` type to represent +successes and failures, the outputs are of the form ``Some p`` (where +``p`` is of type ``ptxt``; this represents a success) or ``None`` (this +represents a failure). + +:: + + module O_NRPRF_real : NRPRF_Oraclei = { + var k : key + var log : nonce list + + proc init() : unit = { + k <$ dkey; + + log <- []; + } + + proc get(n : nonce) : ptxt option = { + var r : ptxt option; + + if (! (n \in log)) { + log <- n :: log; + + r <- Some (f k n); + } else { + r <- None; + } + + return r; + } + }. + +Ideal NRPRF Oracle +~~~~~~~~~~~~~~~~~~ + +For the ideal NRPRF oracle, the formalization is similar to that of the +real NRPRF oracle, only differing in (analogous) ways the pen-and-paper +definitions also differ. + +The only novelty here is that we define and use an alias for the +``dctxt`` distribution, called ``dptxt``. In its definition, this alias +is explicitly indicated to be a distribution over the type of +plaintexts. Naturally, this is only possible because ``ptxt`` and +``ctxt`` are actually the same type. Semantically, this makes no +difference at all; the only reason we do this is to increase readability +by matching the notation with the conceptual meaning. (Recall that NRPRF +oracles conceptually produce plaintexts, not ciphertexts.) The specific +alias definition is provided in the snippet below. + +:: + + op dptxt : ptxt distr = dctxt. + +Then, we formalize the ideal NRPRF oracle as follows. + +:: + + module O_NRPRF_ideal : NRPRF_Oraclei = { + var log : nonce list + + proc init() : unit = { + log <- []; + } + + proc get(n : nonce) : ptxt option= { + var y : ptxt; + var r : ptxt option; + + if (! (n \in log)) { + log <- n :: log; + + y <$ dptxt; + + r <- Some y; + } else { + r <- None; + } + + return r; + } + }. + +NRPRF Experiment and Security +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Having formalized the relevant oracles, we continue by formalizing the +(NRPRF) adversary class. Once again, we formalize this adversary class +using a module type with a single module parameter modeling the expected +NRPRF oracle. Notice that, akin to before, the current module type we +have for NRPRF oracles—``NRPRF_Oraclei``—specifies (the signature of) an +initialization procedure, which we do not want to expose to adversaries. +As such, we create a separate module type for NRPRF oracles given to +adversaries, which only expose the ``get`` procedure. + +:: + + module type NRPRF_Oracle = { + include NRPRF_Oraclei [get] + }. + + module type Adv_NRPRF (O : NRPRF_Oracle) = { + proc distinguish() : bool + }. + +At this point, we have everything required to formalize the NRPRF +experiment, shown. Recall that, even though the adversary is given an +oracle of type ``NRPRF_Oraclei``, the ``init`` procedure of this module +is not actually exposed to the adversary due to the way we specified its +module type. + +:: + + module Exp_NRPRF (O : NRPRF_Oraclei) (D : Adv_NRPRF) = { + proc run() : bool = { + var b : bool; + + O.init(); + + b <@ D(O).distinguish(); + + return b; + } + }. + +.. [1] + NRPRF is not a conventional property; rather, it is a variant of the + more customary Pseudo-Random Function family (PRF) property. For + educational purposes, we have specifically devised this variant to + simplify the current proof. + +.. [2] + Typically, the NRPRF experiment and oracles would first be defined + with respect to an abstract function family of the correct type + before being instantiated with the actual relevant function family + for the proof. This is analogous to how we first defined IND$-NRCPA + with respect to an abstract (symmetric) nonce-respecting encryption + scheme before instantiating it with the actual relevant encryption + scheme for the proof. However, for educational purposes, we decide to + keep it simple and stick with the description that matches the + EasyCrypt formalization the best; for this reason, we immediately + consider the concrete NRPRF property of + :math:`\left(f_{k} : \mathcal{N} \rightarrow \mathcal{P}\right)_{k \in \mathcal{K}}`. diff --git a/doc/tutorials/introduction-itp-program-logics.rst b/doc/tutorials/introduction-itp-program-logics.rst new file mode 100644 index 000000000..be5b10bae --- /dev/null +++ b/doc/tutorials/introduction-itp-program-logics.rst @@ -0,0 +1,51 @@ +Introduction to Computer-Aided Cryptographic Proofs +=================================================== + +.. note:: + + This guide is reproduced and updated, with permission, from `Tejas + Shah `__\ ’s `Joy of + EasyCrypt `__. + + We are grateful to Tejas and Dominique Unruh for developing it and + allowing us to use it here. + +This repo consists of learning material for EasyCrypt, a toolset for +reasoning about cryptographic proofs. It inspired by and written in the +style of `Software +Foundations `__, a series of +electronic textbooks that explain the mathematical underpinnings of +reliable software. For concepts related to cryptography we aim to track +`The Joy of Cryptography `__ (JoC), an +open-source undergrad textbook for cryptography. + +Target audience +--------------- + +Anyone curious about cryptography and who wants to understand formal +verification and computer-aided cryptography in the computational +approach to design-level security [1]_. In line with that, we assume +that the reader is completely new to the field of cryptography, and for +some concepts, the reader will be referred to JoC when needed. We will +offer simplified explanations of concepts required for formal +verification as we go. We expect familiarity with discrete mathematics, +data structures and algorithms, a basic familiarity with the command +line and the ability to work with the Emacs text editor. Essentially, if +you have a little programming experience, then you should be able to +work your way through the ideas presented in this work. + +Although Emacs is pretty complex, we only expect the reader to know how +to open files and navigate them to begin with. These skills can be +learnt quickly with the tutorial that is presented upon a fresh install +of Emacs. Additionally, the `guided tour of +Emacs `__ is helpful for those +who want to know more about what Emacs is capable of and don’t want to +go through the entire tutorial. + +As with the original text, joy is not guaranteed. Formal verification +can be challenging, so we ask you to be patient and keep working with +the material. A tip that we can provide is to start and learn as you go. + +.. [1] + If you do not understand what that means, it is alright, we develop + the required background. diff --git a/doc/tutorials/introduction-itp-program-logics/abstract-ind-ror.ec b/doc/tutorials/introduction-itp-program-logics/abstract-ind-ror.ec new file mode 100644 index 000000000..02ea38e7f --- /dev/null +++ b/doc/tutorials/introduction-itp-program-logics/abstract-ind-ror.ec @@ -0,0 +1,115 @@ +(* +Welcome to ProofGeneral, the front-end that we use to +work with EasyCrypt. ProofGeneral runs on top of Emacs, +so most of keybindings of Emacs work as expected. + +In this file, we go through an illustrative example of +modelling an IND-RoR game with EasyCrypt. + +To interactively evaluate the script, you can either use the +toolbar at the top or use the following keybindings: +1. ctrl + c and then ctrl + n to evaluate one line/block of code (Next) +2. ctrl + c and then ctrl + u to undo evaluation of one line/block of code (Undo) +3. ctrl + x ctrl + s to save the file +4. ctrl + x ctrl + c to exit Emacs + +We will look at more keybindings in the next file. +Evaluting the first line will split the interface to show three panes. + +1. EasyCrypt script pane (left pane) +2. Goals pane (top right) +3. Response pane (bottom right) + +Keep evaluating until the end of the file +and see how things change. +*) + +(* We first import some core theory files *) +require import Real Bool DBool. + +(* We define abstract data-types and operations *) +type msg. +type cip. + +(* Encrypt and decrypt operations. *) +op enc: msg -> cip. +op dec: cip -> msg. + +(* Compute operations for the adversary. *) +op comp: cip -> bool. + +(* +Next we define the module types. +These are blueprints for concrete types +that we instantiate right after we define them. +*) + +module type Challenger = { + proc encrypt(m:msg): cip + proc decrypt(c:cip): msg +}. + +module C:Challenger = { + + proc encrypt(m:msg): cip = { + return enc(m); + } + + proc decrypt(c:cip): msg = { + return dec(c); + } +}. + +(* Similarly we define an adversary. *) +module type Adversary = { + proc guess(c:cip): bool +}. +(* and an instance of the same. *) +module Adv:Adversary = { + + proc guess(c:cip): bool = { + return comp(c); + } +}. + +(* The game module and the claims related to it. *) +module Game(C:Challenger, Adv:Adversary) = { + + proc ind_ror(): bool = { + var m:msg; + var c:cip; + var b,b_adv:bool; + b <$ {0,1}; (* Pick b uniformly at random. *) + if(b=true){ + (* Set m to be an authentic message. *) + } else { + (* Set m to be a random string. *) + } + c <@ C.encrypt(m); + b_adv <@ Adv.guess(c); + return (b_adv=b); + } +}. + +(* +At this point EasyCrypt will throw a warning +complaining about how there may be an uninitialized +variable. This happens because in our current +program definition, we haven't initialized +"m" to anything. +We skim past this warning, since this example +is only to illustrate the structure of EasyCrypt scripts. +Go ahead and keep evaluating the script. +Make sure to undo some evaluations as well, +just to get the keystrokes into your muscle memory. +*) + +axiom ind_ror_pr_le1: +phoare [Game(C,Adv).ind_ror: true ==> res] <= 1%r. + +lemma ind_ror_secure: +phoare [Game(C,Adv).ind_ror: true ==> res] <= (1%r/2%r). +(* Notice the changes in the goals pane *) +proof. + admit. +qed. diff --git a/doc/tutorials/introduction-itp-program-logics/abstract-ind-ror.png b/doc/tutorials/introduction-itp-program-logics/abstract-ind-ror.png new file mode 100644 index 000000000..99e9faee9 Binary files /dev/null and b/doc/tutorials/introduction-itp-program-logics/abstract-ind-ror.png differ diff --git a/doc/tutorials/introduction-itp-program-logics/ambient-logic.ec b/doc/tutorials/introduction-itp-program-logics/ambient-logic.ec new file mode 100644 index 000000000..e59a556c8 --- /dev/null +++ b/doc/tutorials/introduction-itp-program-logics/ambient-logic.ec @@ -0,0 +1,428 @@ +(* +As we saw earlier in the abstract-ind-ror.ec file, +we use Emacs, and ProofGeneral to work with EasyCrypt. +We will need various commands/keybindings to work with Emacs. +All the keybindings begin either with the CONTROL key, denoted by "C", +or the META or ALT key denoted by "M". +So if you see "C-c C-n" it simply means: CONTROL + c and then CONTROL + n. +Go ahead, try it. This will evaluate the current comment, highlight it +to indicate that it has been evaluated and will place a small black dot on the +left margin at the beginning of the next block to be evaluated. +*) + +(* +Most formal proofs are written interactively. +The proof-assistant, EC in our case, will keep track of the goals +(context, and conclusions) for us. +The front-end, Proof-General + Emacs in our case, will show us the +goals and messages from the assistant, in the "goals" pane, and "response" pane +on the right. +Our objective is to use different tactics to prove or "discharge" the goal. +Since we only have comments so far there are no goals for EC to work with. +We will change that in a short while. +*) + +(* +Here is a short list of keystrokes that will come in handy for this file: +1. C-c C-n : Evaluate next line or block of code +2. C-c C-u : Go back one line or block of code +3. C-c C-ENTER: Evaluate until the cursor position +4. C-c C-l: To reset the Proof-General layout +5. C-x C-s: Save file +6. C-x C-c: Exit Emacs (read the prompt at the bottom of the screen) +*) + +(* +EC has a typed expression language, so everything we declare +should either explicitly have a type or it should be inferable +from the operators that are used. +To begin with let us import the built-in Integer theory file. +*) + +require import Int. + +(* The pragma line simply tells EC to print all goals *) +pragma Goals: printall. + +(* +Now, let us start with something trivial to prove. +Let us start with the reflexivity of integers. +Reflexivity is simply the property that an integer is equal to itself. +Mathematically, we would write it like so: +For every integer x, x=x. +*) + +(* +Here is how we declare something like that in EC. +C-c C-n multiple times to get EC to evaluate the lemma. +Or alternatively, move the cursor to the line with the lemma, +and hit C-c C-ENTER. +*) + +lemma int_refl: forall (x: int), x = x. +(* +Notice how EC populates the goals pane on the right +with the context and the conclusion. +Keep stepping through the proof with C-c C-n. +*) +proof. + trivial. +qed. + +(* +We begin a formal proof with the tactic called "proof", +although it is optional to begin a proof with the "proof" keyword/tactic, +it is considered good style to use it. + +Then we use a set of tactics which transform the goal into zero or more subgoals. +In this case, we used the tactic "trivial", to prove our int_refl lemma. +Once there are no more goals, we can end the proof with "qed", +and EC saves the lemma for further use. +*) + +(* +"trivial" tries to solve the goal using a mixture of other tactics. +So it can be hard to understand when to apply it, but the good news +is that trivial never fails. It either solves the goals or leaves the goal +unchanged. So you can always try it without harm. +*) + +print int_refl. + +(* +The "print" command prints out the request in the response pane. +We can print types, modules, operations, lemmas etc using the print keyword. +Here are some examples: +*) + +print op (+). +print op min. +print axiom Int.fold0. + +(* +The keywords simply act as qualifiers and filters. +You can print even without those. +Like so: +*) +print (+). +print min. + +(* +Now EC knows the lemma int_refl, and allows us to use it to prove other lemmas. +Although the next lemma is trivial, it illustrates the idea of this applying +known results. +*) + +print Int. + +lemma forty_two_equal: 42 = 42. +proof. + apply int_refl. +qed. + +(* +"apply" tries to match the conclusion of what we are applying (the proof term), +with the goal's conclusion. If there is a match, it replaces the goal +with the subgoals of the proof term. +In our case, EC matches int_refl to the goal's conclusion, sees that it +matches, and replaces the goal with what needs to be proven for int_relf which is +nothing, and it concludes the proof. +*) + +(* +EC comes with a lot of predefined lemmas and axioms that we can use. +Let us now look at axioms about commutativity and associativity for integers. +They are by the names addzC, and addzA. Print them out as an exercise. +*) + + +(* Simplifying goals *) + +(* +In the proofs, sometimes tactics yield us something that can be simplified +We use the tactic "simplify", in order to carry out the simplification. + +The simplify tactic reduces the goal to a normal form using lambda calculus. +We don't need to worry about the specifics of how, but it is important to +understand that EC can simplify the goals given it knows how to. +It will leave the goal unchanged if the goal is already in the normal form. + +For instance, here is a contrived example that illustrates the idea. +We will get to more meaningful examples later, but going through these +simple examples will make writing complex proofs easier. +*) + +(* Commutativity *) +lemma x_plus_comm (x: int): x + 2*3 = 6 + x. +proof. + simplify. + (* EC does the mathematical computation for us and simplifies the goal *) + simplify. + (* simplify doesn't fail, and leaves the goal unchanged *) + trivial. + (* trivial doesn't fail either, and leaves the goal unchanged *) + apply addzC. +qed. + +(* ---- Exercise ---- *) +(* +"admit" is a tactic that closes the current goal by admitting it. +Replace admit in the following lemma and prove it using the earlier tactics. +*) +lemma x_minus_equal (x: int): x - 10 = x - 9 - 1. +proof. +admit. +qed. + +(* +The goal list in EC is an ordered one, and you have to prove them +in the same order as EC lists it. "admit" can be used to bypass a certain +goal and focus on something else in the goal list. +*) + +(* +Use the tactic "split" to split the disjunction into two +and apply the previous axioms to discharge the goals. +Experiment with admiting the first goal after splitting +*) +lemma int_assoc_comm (x y z: int): x + (y + z) = (x + y) + z /\ x + y = y + x. +proof. +admit. +qed. + +(* +To deal with disjunctions in EC, you can use the tactics "left" or "right" +to step into a proof of the left proof term, or the right proof term respectively. +*) + +(* Searching in EC *) + +(* +Since, there is a lot that is already done in EC, +we need a way to look for things. +We do that using the "search" command. It prints out all axioms and lemmas +involving the list of operators that give it. +*) + +search [-]. +(* [] - Square braces for unary operators *) + +search (+). + +(* +As you can see the list can be quite overwhelming and difficult to navigate. +So we can limit the results using a list of operators, or patterns. +*) + +search ( * ). +(* +() - Parentheses for binary operators. +Notice the extra space for the "*" operator. +We need that since (* *) also indicates comments. +*) + +search (+) (=) (=>). +(* List of operators "=>" is the implication symbol *) + +search min. +(* By just the name of the operators. *) + +(*---- Exercises ----*) + +(* Distributivity *) +(* Search for the appropriate axiom and apply it to discharge this goal. *) +lemma int_distr (x y z: int): (x + y) * z = x * z + y * z. +proof. + admit. +qed. + +(* +So far, we saw lemmas without any assumptions +except for that of the type of the variable in question. +More often than not we will have assumptions regarding variables. +We need to treat these assumptions as a given and introduce them into the context. +This is done by using "move => ..." followed by the name you want to give +the assumption. +*) + +lemma x_pos (x: int): 0 < x => 0 < x+1. +proof. + move => x_ge0. + simplify. + trivial. + (* Both of those tactics don't work. We need something else here *) + (* Let us see if EC has something that we can use. *) + search (<) (+) (0) (=>). + rewrite addz_gt0. + (* + "rewrite" simply rewrites the pattern provided, so in our case it + rewrites our goal here (0 < x + 1), with the pattern that we provided + which is addz_gt0, and then requires us to prove the assumptions of + the pattern which are 0 < x and 0 < 1. + *) + (* Goal 1: 0 < x *) + + (* + When we have a goal matches an assumption, we + can use the tactic assumption to discharge it. + *) + assumption. + + (* Goal 2: 0 < 1 *) + trivial. +qed. + +(* Let us see some variations *) + +lemma int_assoc_rev (x y z: int): x + y + z = x + (y + z). +proof. + print addzA. + (* + We might have a lemma or an axiom that we can apply to the goal, + but the LHS and RHS might be flipped, and EC will complain that + they don't match to apply them. + To rewrite a lemma or axiom in reverse, we simply add the "-" infront + of the lemma to switch the sides like so. + *) + rewrite -addzA. + trivial. +qed. + +(* +Note that here "apply addzA." or "apply -addzA" do not work +We encourage you to try them. +*) + +(* +Recap: +So far we have seen the following tactics: +trivial, simplify, apply, rewrite, +move, split, left, right, admit, and assumption. +We also saw how to print and search for patterns. +These are at the foundation of how we work with EC. +*) + +(* +Intro to smt and external provers: +An important point to understand, however, is that EC +was built to work with cryptographic properties and more complex things. +So although other mathematical theorems and claims can be proven in EC, +it will be quite painful to do so. We will employ powerful automated tools +to take care of some of these low-level tactics and logic. +EC offers this in the form of the "smt" tactic. +When we run smt, EC sends the conclusion and the context to external smt solvers. +If they are able to solve the goal, then EC completes the proof. +If not smt fails and the burden of the proof is still on us. +*) + +lemma x_pos_smt (x: int): 0 < x => 0 < x+1. +proof. +smt. +qed. + +(* +As you can see, smt can make our lives much easier. +Now, here are some properties about logarithms that are mentioned in +The Joy of Cryptography. We leave them to be completed as exercises, +without using the smt tactic. Most of them are straightforward and +serve the purpose of exercising the use of basic tactics. +*) + +require import AllCore. + + +(* print AllCore to see what it includes *) + +(* Logs and exponents: *) + +lemma exp_product (x: real) (a b: int): x^(a*b) = x ^ a ^ b. +proof. + search (^) (=). + by apply RField.exprM. +qed. + +lemma exp_product2 (x: real) (a b: int): x <> 0%r => x^a * x^b = x^(a + b). +proof. + move => x_pos. + search (^) (=). + print RField.exprD. + rewrite -RField.exprD. + assumption. + trivial. +qed. + +(* Logarithm exercises *) +require import RealExp. + +(* +Print and search for "ln" to see how it is defined and +the results we have available already +*) +lemma ln_product (x y: real) : 0%r < x => 0%r < y => ln (x*y) = ln x + ln y. +proof. + search (ln) (+). + move => H1 H2. + by apply lnM. +qed. + +print log. +(* +Notice how log is defined. It is defined as an operator that expects two inputs +Since most of ECs axioms are written for natural logs (ln), inorder to reason with +log and inorder to work with the next lemma, you will need to rewrite log. +To do so the syntax is + +rewrite /log. + +The "/" will rewrite the pattern that follows. +*) + +(* +This helper can come in handy in the next proof. +Sometimes it can be cumbersome to reason with a goal. +In cases like those, it is useful to reduce the complexity of the proof by using +helper lemmas like these. +*) + +lemma helper (x y z: real): (x + y) / z = x/z + y/z. +proof. +smt. +qed. + +lemma log_product (x y a : real): + 0%r < x => 0%r < y => log a (x*y) = log a x + log a y. +proof. + move => H1 H2. + rewrite /log. + rewrite lnM. + assumption. + assumption. + by apply helper. +qed. + +(* Or we can simply let smt do the heavy lifting for us *) +lemma log_product_smt (x y a : real): + 0%r < x => 0%r < y => log a (x*y) = log a x + log a y. +proof. + smt. +qed. + +(* +Modulo arithmatic exercises: +This is one of the properties that is mentioned in the + *) +require import IntDiv. + +lemma mod_add (x y z: int): (x %% z + y %% z) %% z = (x + y) %% z. +proof. + by apply modzDm. +qed. + +(* +A couple of more keystrokes that might be useful. + +1. C-c C-r: Begin evaluating from the start +2. C-c C-b: Evaluate until the end of the file. + +Go ahead and give these a try. +*) diff --git a/doc/tutorials/introduction-itp-program-logics/ambient-logic.png b/doc/tutorials/introduction-itp-program-logics/ambient-logic.png new file mode 100644 index 000000000..97299e230 Binary files /dev/null and b/doc/tutorials/introduction-itp-program-logics/ambient-logic.png differ diff --git a/doc/tutorials/introduction-itp-program-logics/ambient-logic.rst b/doc/tutorials/introduction-itp-program-logics/ambient-logic.rst new file mode 100644 index 000000000..c66dd1d2a --- /dev/null +++ b/doc/tutorials/introduction-itp-program-logics/ambient-logic.rst @@ -0,0 +1,384 @@ +The ambient logic of EasyCrypt is what drives all proof scripts. To get +a grasp of how to work with ambient logic, we will work through the +``ambient-logic.ec`` file. As we saw in the motivating example earlier, +formal proofs are a sequence of proof tactics, and so far, we’ve only +seen the ``admit`` tactic. In this chapter, we will learn some more +basic tactics and work with simple mathematical properties of integers. + +It is highly recommended to work through `the +file `__ +using EasyCrypt in the Proof General + Emacs environment. However, +simply reading through this chapter will also provide you with a working +knowledge of ambient logic and the tactics that we use in this chapter. + +Navigation +---------- + +As noted earlier, the official Emacs tutorial covers the basics of +working with Emacs. The tutorial is presented as an option on the splash +screen on fresh installs of Emacs. It can also be accessed by starting +Emacs and then pressing (Ctrl + h), followed by t. + +All the keybindings begin either with Ctrl key, denoted by “C”, or the +META or Alt key, denoted by “M”. + +So, “C-c C-n” simply means: Ctrl + c and then Ctrl + n. + +Apart from all the basic keybindings of Emacs, we have a few more +bindings that are used specifically for interactive theorem proving in +EasyCrypt. We list some of the most common commands here: + ++----+--------------+--------------------------------------------------+ +| # | Keystroke | Command | ++====+==============+==================================================+ +| 1. | C-c C-n | Evaluate next line or block of code | ++----+--------------+--------------------------------------------------+ +| 2. | C-c C-u | Go back one line or block of code | ++----+--------------+--------------------------------------------------+ +| 3. | C-c C-ENTER | Evaluate until the cursor position | ++----+--------------+--------------------------------------------------+ +| 4. | C-c C-l | To reset the Proof-General layout | ++----+--------------+--------------------------------------------------+ +| 5. | C-c C-r | Begin evaluating from the start (Reset) | ++----+--------------+--------------------------------------------------+ +| 6. | C-c C-b | Evaluate until the end of the file | ++----+--------------+--------------------------------------------------+ +| 7. | C-x C-s | Save file | ++----+--------------+--------------------------------------------------+ +| 8. | C-x C-c | Exit Emacs (Pay attention to the prompts) | ++----+--------------+--------------------------------------------------+ + +Most formal proofs are written interactively, and the proof-assistant, +EasyCrypt in our case, will keep track of the goals (context and +conclusions) for us. The front-end, Proof-General + Emacs in our case, +will show us the goals and messages from the assistant in the goals pane +and response pane, respectively. Our objective is to use different +tactics to prove or “discharge” the goal. + +.. figure:: ambient-logic.png + :alt: The different panes in EasyCrypt + + The different panes in EasyCrypt + +Basic tactics and theorem proving +--------------------------------- + +EasyCrypt has a typed expression language, so everything we declare +should either explicitly have a type or be inferable from the context. +As we saw earlier, EasyCrypt comes with basic built-in data types. These +can be accessed by importing them into the current environment. In this +file, we will be working with the ``Int`` theory file, and we also want +EasyCrypt to print out all the goals. For this, we provide a directive +to EasyCrypt using a ``pragma``. + +:: + + require import Int. + pragma Goals: printall. + +Generally, the first steps in our files will be importing theories and +setting the pragma. + +Before we dive into cryptography, we need to understand how to direct +EasyCrypt to modify the goals and make progress. As we mentioned, this +is achieved by using tactics. In general, the proofs for lemmas take the +following form: + +:: + + lemma name ... : ... . + proof. + tactic_1. + ... + tactic_n. + qed. + +Tactic: ``trivial`` +~~~~~~~~~~~~~~~~~~~ + +To begin with, we will look at a few properties of integers and +introduce how some of the tactics work. + +Reflexivity is simply the property that an integer is equal to itself. +Mathematically, we would write it like so: + +.. math:: \forall x \in \mathbb{Z}, x=x + +We can express this in EasyCrypt with a lemma and prove it like so: + +:: + + lemma int_refl: forall (x: int), x = x. + proof. + trivial. + qed. + +Once we state our lemma and evaluate it, EasyCrypt populates the goal +pane with what needs to be proved. In our case, it presents the +following in the goal. + +:: + + Current goal + + Type variables: + ------------------------------------------ + forall (x : int), x = x + +We start the proof script with the ``proof``, and then EasyCrypt expects +tactics to close the goal. In this case, we use ``trivial``, to prove +our ``int_refl`` lemma. Upon evaluating ``trivial``, the goal pane is +cleared since using this tactic closes the goal. Once there are no more +goals, we can end the proof with ``qed``, and EasyCrypt saves the lemma +for further use and sends us this message in the response pane. Like so: + +:: + + + added lemma: `int_refl' + +``trivial`` tries to solve the goal using various tactics. So it can be +hard to understand when to apply it, but the good news is that +``trivial`` never fails. It either solves the goals or leaves the goal +unchanged. So you can always try it without harm. + +Tactic: ``apply`` +~~~~~~~~~~~~~~~~~ + +Now EasyCrypt knows the lemma ``int_refl`` and allows us to use it to +prove other lemmas. This can be done using the ``apply`` tactic. For +instance: + +:: + + lemma forty_two_equal: 42 = 42. + proof. + apply int_refl. + qed. + +``apply`` tries to match the conclusion of what we are applying (the +proof term) with the goal’s conclusion. If there is a match, it replaces +the goal with the subgoals of the proof term. + +In our case, EasyCrypt matches ``int_refl`` to the goal’s conclusion, +sees that it matches, and replaces the goal with what needs to be proven +for ``int_refl``, which is nothing, and it concludes the proof. + +EasyCrypt comes with many predefined lemmas and axioms that we can use. +For instance, it has axioms related to commutativity and associativity +for integers. They are by the names ``addzC``, and ``addzA``. + +We can ask EasyCrypt to print using: ``print addzC.`` + +EasyCrypt responds with: +``axiom nosmt addzC: forall (x y : int), x + y = y + x.`` + +Tactic: ``simplify`` +~~~~~~~~~~~~~~~~~~~~ + +In the proofs, sometimes tactics yield something that can be simplified. +We use the tactic ``simplify`` to carry out the simplification. +``simplify`` reduces the goal to a normal form using lambda calculus. We +don’t need to worry about the specifics of how, but it is important to +understand that EasyCrypt can simplify the goals given it knows how to. +It will leave the goal unchanged if the goal is already in a normal +form. + +For instance, here is an example that illustrates the idea. + +:: + + lemma x_plus_comm (x: int): x + 2*3 = 6 + x. + proof. + simplify. + (* Simplifies the goal to x + 6 = 6 + x. *) + + simplify. + trivial. + (* These make no progress, but don't fail either. *) + + apply addzC. + (* Discharges the goal *) + qed. + +Tactics: ``move``, ``rewrite``, ``assumption`` +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +So far, we saw lemmas without any assumptions except for specifying the +type of a variable. More often than not, we will have assumptions +regarding variables. We need to treat these assumptions as a given and +introduce them into the context. This is done by using ``move =>`` +followed by the name you want to give the assumption. Additionally, when +these assumptions show up as goals, instead of applying the assumptions, +we can call the tactic ``assumption`` to discharge the goal directly. +EasyCrypt will automatically look for assumptions that match the goal +when we use ``assumption``. + +In the following example, we use ``addz_gt0``, which is this result: + +``axiom nosmt addz_gt0: forall (x y : int), 0 < x => 0 < y => 0 < x + y.`` + +:: + + lemma x_pos (x: int): 0 < x => 0 < x+1. + proof. + move => x_ge0. + (* + Moves the assumption 0 < x into the + context, and names it x_ge0. + *) + + rewrite addz_gt0. + (* Splits into two goals. *) + + (* Goal 1: 0 < x *) + assumption. + + (* Goal 2: 0 < 1 *) + trivial. + qed. + +The tactics ``rewrite`` and ``apply`` are very similar, they try to +pattern match the goal with the term that is supplied to them. However, +there can be some subtle differences which aren’t exactly clear. For +instance, with the simple example: + +:: + + lemma forty_two_equal: 42 = 42. + proof. + apply int_refl. + qed. + +``apply int_refl.`` discharges the goal, but ``rewrite int_refl.`` +doesn’t make any progress. So sometimes, trial and error are required to +make progress. + +We might have a lemma or an axiom that we can rewrite to the goal, but +the LHS and RHS might be flipped, and EasyCrypt will complain that they +don’t match to apply them. To rewrite a lemma or axiom in reverse, we +simply add the “-” in front of the lemma to switch the sides like so: + +:: + + lemma int_assoc_rev (x y z: int): x + y + z = x + (y + z). + proof. + rewrite -addzA. + trivial. + qed. + +These tactics form the basics of theorem proving and working with +EasyCrypt at the level of ambient logic. + +A point to note here is that there are many more options and intricacies +even within these simple tactics. For instance, there are many +introduction patterns with the ``move =>`` tactic, and the keyword +``move`` can be replaced by other tactics as well. Presenting these +introduction patterns with good examples could be an important addition +to this chapter on the basic tactics. + +Commands: ``search`` and ``print`` +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Often when it comes to working with theorems, we need the ability to +search through results that are already in the environment. We saw a few +examples of printing in the content that we have covered so far. Let us +take a slightly more detailed look at this part of EasyCrypt that we use +from time to time. + +The ``print`` command prints out the request in the response pane. We +can print types, modules, operations, lemmas etc., using the print +keyword. Here are some examples: + +:: + + print op (+). + (* Response: abbrev (+) : + int -> int -> int = CoreInt.add. *) + print op min. + (* Response: op min (a b : int) : int + = if a < b then a else b. *) + print axiom Int.fold0. + (* Response: lemma fold0 ['a]: + forall (f : 'a -> 'a) (a : 'a), fold f a 0 = a. *) + +The keywords simply act as qualifiers and filters. You can print even +without those. The qualifiers simply help us to narrow the results. + +The ``search`` command allows us to search for axioms and lemmas +involving a list of operators. It accepts arguments enclosed in the +following braces: 1. ``[ ]`` - Square brackets for unary operators 2. +``( )`` - Rounded brackets for binary operators 3. Combination of these +separated by a space + +:: + + search [-]. + search (+). + (* Shows lemmas and axioms that + include the specified operators. *) + search ( * ). + (* Notice the extra space for the "*" operator. + We need that since (* *) also indicates comments. *) + + search (+) (=) (=>). + (* Shows lemmas and axioms which have + all the listed operators *) + +In the file, we have peppered some exercises that require the reader to +search for specific results to make progress. + +External SMT solvers: ``smt`` +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +An important point to understand is that EC was built to work with +cryptographic properties and more complex things. So although general +mathematical theorems and claims can be proven in EC, it will be quite +painful to do so. We will employ powerful automated tools to take care +of some of these low-level tactics and logic. EC offers this in the form +of the ``smt`` tactic. When we run ``smt``, EC sends the conclusion and +the context to external smt solvers like ``Z3``, ``Alt-Ergo`` etc., that +have been configured to be used by EasyCrypt. If they can solve the +goal, then ``smt`` will discharge the specific sub-goal that it was +invoked on. If not, ``smt`` fails, and the burden of the proof is still +on us. + +For example, if we wish to prove the result: + +.. math:: \forall x \in \mathbb{R}, \forall a, b \in \mathbb{Z}, \text{ and } x \neq 0 \implies x^a * x^b = x^{a+b} + +We would do it like so: + +:: + + lemma exp_product (x: real) (a b: int): + x <> 0%r + => x^a * x^b = x^(a + b). + proof. + move => x_pos. + rewrite -RField.exprD. + assumption. + trivial. + qed. + +However, it can be simplified to: + +:: + + lemma exp_product_smt (x: real) (a b: int): + x <> 0%r + => x^a * x^b = x^(a + b). + proof. + smt(). + qed. + +The key takeaway is that we will rely on external solvers to do a fair +amount of heavy lifting when it comes to results related to low-level +math. + +That concludes this chapter on ambient logic. In this chapter we covered +the basic tactics like ``apply``, ``simplify``, ``move``, ``rewrite`` +etc, we also saw how to use the ``search`` and ``print`` commands and +learnt to work with external solvers. We have also provided exercises +that help the reader practice using these tactics. We will introduce +more tactics and other techniques as we progress in the subsequent +chapters. diff --git a/doc/tutorials/introduction-itp-program-logics/conclusion.rst b/doc/tutorials/introduction-itp-program-logics/conclusion.rst new file mode 100644 index 000000000..f6e44abd4 --- /dev/null +++ b/doc/tutorials/introduction-itp-program-logics/conclusion.rst @@ -0,0 +1,16 @@ +Working through the material should give you a basic grasp of how +EasyCrypt works, and the ability to work with some of the tactics. +Admittedly, this work is by no means complete since we barely scratched +the surface of what EasyCrypt is capable of doing and the current state +of the art when it comes to cryptography. + +A good next step if you are interested in learning more about +formalising game-based cryptographic security proofs in EasyCrypt is to +simply follow our main tutorial—referring to this one for concepts or +ideas that may not have been cemented. + +If you already know what you want to formalize, you may also be +interested in the `Crypto Proof +Ladders `__ project created under the +umbrella of the High-Assurance Cryptographic Software (HACS) +`community `__. diff --git a/doc/tutorials/introduction-itp-program-logics/easycrypt.rst b/doc/tutorials/introduction-itp-program-logics/easycrypt.rst new file mode 100644 index 000000000..cd3ff86a0 --- /dev/null +++ b/doc/tutorials/introduction-itp-program-logics/easycrypt.rst @@ -0,0 +1,362 @@ +As we saw earlier, the security properties of cryptosystems can be +modelled as games being played by challengers (Alice, Bob) and +adversaries (Eve). EasyCrypt is a proof assistant that allows us to +model and verify these game-based cryptographic proofs. + +EasyCrypt environment +--------------------- + +EasyCrypt is written in OCaml and uses many external tools and +libraries. However, the components that we will be interacting with the +most are the following: 1. **Emacs and Proof General**: Emacs is an +open-source text editor, and Proof General is a generic interface for +proof assistants based on Emacs. Together these form the front-end for +working with EasyCrypt. When working with EasyCrypt, we generally prove +statements interactively using the Emacs + Proof General environment. + +:: + + *Note*: EasyCrypt also has a batch processing mode which doesn't need the + Emacs + Proof General front-end and only requires a terminal. However, this + mode is used to check multiple files and not to write proofs. + +2. **External Provers and Why3**: Often called SMT (Satisfiability + Modulo Theory) provers or SMT solvers are powerful tools that try to + solve the problem of satisfiability of a formula given a set of + conditions. With EasyCrypt, there is a possibility to use multiple + external provers like `Alt-Ergo `__, + `Z3 `__ and + `CVC4 `__, and + `Why3 `__ is used as the platform for all the + provers. + + These provers can take care of a lot of the low-level and often + gruelling work of proving some mathematical results, as we will see. + +.. note:: + + Since there are a lot of external dependencies setting up the + environment can be quite time-consuming, and doing it right might + involve quite a bit of choice. If you don’t want to have to make + choices, we offer an opinionated `installation + guide `__. + +Now without delving too much into the theory, let us start with a quick +motivating example. + +Abstract example: IND-RoR game +------------------------------ + +Let us model a game to prove that a cryptographic protocol possesses the +property of ciphertexts being indistinguishable from random. It is often +abbreviated as IND-RoR (Indistinguishability - Real or Random). The +notion of indistinguishability is considered to be one of the most basic +security assurances that are expected from cryptosystems. + +Intuitively, the idea is that if an adversary cannot tell apart an +encrypted message from encrypted randomness, then they can’t obtain any +information from intercepted ciphertexts that they wouldn’t be able to +obtain purely by chance. Hence, the system can be thought to be secure. + +To model it mathematically, let us assume we have a cryptographic +protocol, :math:`CP`, that consists of an encryption function, +:math:`Enc`, and a decryption function, :math:`Dec`, known to the +challengers. The adversary gets access to the output of :math:`Enc`. In +this simplified example, we don’t worry about the specifics of these +functions. + +So the game for IND-RoR under the protocol, :math:`CP`, would proceed as +follows: 1. Pick :math:`b \in \{0,1\}`, uniformly at random. 2. If +:math:`b = 0`, the challengers encrypt a real message using :math:`Enc`. +Let us call it :math:`c_0 = Enc(m_{\textit{real}})` 3. If :math:`b = 1`, +the challengers encrypt a random bitstring using :math:`Enc`. Let us +call it :math:`c_1 = Enc(m_{\textit{random}})` 4. If :math:`b=0`, send +:math:`c_0` to the adversary, else send :math:`c_1` 5. Adversary is +allowed to perform its computations on the provided ciphertext and is +expected to output :math:`b_{\textit{adv}}` 6. Now, the adversary is +said to win the game if they have a non-negligible advantage in +correctly guessing which ciphertext (real or random) they were supplied +with. Mathematically, the adversary wins the game if: + +.. math:: + + \mathbb{P}[b_{adv}==b] + = \dfrac{1}{2} + \epsilon, \text{ where } \epsilon \text{ is non-negligible} + +Now, if we come up with a proof that +:math:`P[b_{adv}==b] = \frac{1}{2} + \epsilon`, where :math:`\epsilon` +is negligible, regardless of what the adversary does, then we can claim +that the protocol is secure under the IND-RoR paradigm. + +Most cryptographic protocols rely on game-based proofs like these to +prove the protocol’s security properties. Our game, although simplified +to a large extent, can already be modelled in EasyCrypt. + +Modelling the IND-RoR game with EasyCrypt +----------------------------------------- + +Let us develop an EasyCrypt `proof +sketch `__ +for the game that we defined above. + +Every EasyCrypt proof consists of the following major steps: + +Defining the objects +~~~~~~~~~~~~~~~~~~~~ + +We first need to establish the context we would like to work in. +EasyCrypt comes with several predefined types, operators and functions, +such as integers, real numbers, etc. Hence we begin by loading +(``require``) and importing (``import``) the theories into the current +environment (files that contain these definitions are called theory +files or just theories) that we need. + +In this example, we will only need the ``Real Bool DBool`` theory files. +``Real`` and ``Bool`` are needed to work with real and boolean types, +and we need the ``DBool`` (boolean distribution) to pick a boolean value +at random. Importing these theories works like so: + +:: + + require import Real Bool DBool. + +Notice how the statement ends with a “.”; this is how statements are +terminated in EasyCrypt. + +In addition to the built-in types, we might need custom data types and +operations. EasyCrypt allows us to do so using the keywords ``type`` and +``op``. + +Let us define a ``msg`` type for messages, and ``cip`` type for +ciphertexts. Then let us define the operation ``enc: msg -> cip`` which +defines a function called ``enc`` mapping ``msg`` to ``cip``, and a +function called ``dec`` to go back from ``cip`` to ``msg``. +Additionally, let us also define a function called ``comp`` to model the +adversary performing some computation upon receiving a ``cip`` and +returning a ``bool``. + +:: + + type msg. + type cip. + + (* Encrypt and decrypt operations. *) + op enc: msg -> cip. + op dec: cip -> msg. + + (* Compute operations for the adversary. *) + op comp: cip -> bool. + +Note that these are only abstract definitions, and we haven’t specified +the details of these types or functions. The interesting thing about +EasyCrypt is that we can already go pretty far with the abstract types +and operations. + +Let us keep going and define custom module types and modules. Module +types can be thought of as blueprints, while modules can be thought of +as concrete instances of module types. For those familiar with +object-oriented programming, this is similar to interfaces for classes +and the classes that implement those interfaces. + +In our example, the challengers have the ability to encrypt and decrypt +messages. We can model this by creating a module type called +``Challenger``, which needs to have two procedures called ``encrypt`` +and ``decrypt``. As we said, a module type is simply a blueprint. To +work with the module types, we could create a concrete instance of the +``Challenger`` type and fill out the procedures. In our example, we +create a module, ``C``, of type ``Challenger``. ``C`` has to implement +the procedures ``encrypt`` and ``decrypt``. This can be achieved like +so. + +:: + + module type Challenger = { + proc encrypt(m:msg): cip + proc decrypt(c:cip): msg + }. + + module C:Challenger = { + proc encrypt(m:msg): cip = { + return enc(m); + } + proc decrypt(c:cip): msg = { + return dec(c); + } + }. + + (* Similarly, we define an adversary *) + module type Adversary = { + proc guess(c:cip): bool + }. + (* and a concrete instance of an adversary *) + module Adv:Adversary = { + proc guess(c:cip): bool = { + return comp(c); + } + }. + +.. note:: + + Module types and modules need to begin with a capital letter. + +We now have all the ingredients required to model the IND-RoR game +outlined above. A game can be defined as a module in EasyCrypt like so: + +:: + + module Game(C:Challenger, Adv:Adversary) = { + proc ind_ror(): bool = { + var m:msg; + var c:cip; + var b,b_adv:bool; + b <$ {0,1}; (* Sample b uniformly at random *) + if(b){ + (* Set m to be an authentic message *) + } else { + (* Set m to be a random string *) + } + c <@ C.encrypt(m); + b_adv <@ Adv.guess(c); + return (b_adv = b); + } + }. + +Here, we leave the ``if`` and ``else`` blocks empty since we don’t want +to introduce too much complexity in this motivating example. + +Making claims +~~~~~~~~~~~~~ + +Once we have the objects defined, we can make claims related to these +objects. We can either state these claims as axioms with the ``axiom`` +keyword, in which case EasyCrypt will not expect a proof or a lemma with +the ``lemma`` keyword, and EasyCrypt will expect a proof for the +statement. For our running example, a claim that we can state is that +the probability of ``(b_adv=b)`` or the result, ``res``, holding is +certainly less than or equal to 1. This statement about the probability +of an event is universally true. Hence we can state it as an axiom like +so: + +``{Stating an axiom}{list:axiom} axiom ind_ror_pr_le1: phoare [Game(C,Adv).ind_ror: true ==> res] <= 1%r.`` + +This code can be read in the following way: We state the axiom, +``ind_ror_pr_le1``, which says that the probability (``phoare``) of the +result (``res``) holding upon running the ``ind_ror`` game with ``C`` +and ``Adv`` is less than or equal to 1. (The trailing ``\%r`` after +``1`` is how we cast an integer to a real number.) + +We will look at the components in more detail as we go along. However, +the key takeaway here is that axioms don’t require proofs. + +Next, let us claim that the cryptosystem is indeed IND-RoR secure. +Statements like these are what we intend to prove and are the main +reason we go through the whole setup. + +.. note:: + + We skip the detail about the negligible advantage and + :math:`\epsilon` since this is only an illustrative example. We’d pay + more attention to the details when we work with an actual protocol. + +:: + + lemma ind_ror_secure: + phoare [Game(C,Adv).ind_ror: true ==> res]<=(1%r/2%r). + +Proofs +~~~~~~ + +Once we state a lemma, EasyCrypt expects a proof for the same. It is +good practice to start a proof script with the ``proof`` keyword, but it +is not strictly necessary. A proof script is a sequence of tactics that +transform the goal into zero or more sub-goals. A proof is said to be +complete or discharged once we get to zero sub-goals. Upon completing a +proof, we end the script with ``qed``, and EasyCrypt adds the lemma to +the environment. + +Since we haven’t filled out the details in our running example, we can’t +really make progress with the proof of ``lemma ind_ror_secure``, so for +this example, we will ``admit`` it. Admitting a result is akin to +axiomatizing it. Ideally, we wouldn’t want to axiomatize a lemma. +However, we use this example to illustrate the structure of EasyCrypt +proofs in general. + +:: + + lemma ind_ror_secure: + phoare [Game(C,Adv).ind_ror: true ==> res]<=(1%r/2%r). + proof. + admit. + qed. + +The complete code of the example can be found in ``abstract-ind-ror.ec`` +file. Most proof scripts are developed interactively. To get a taste of +how this works, you can open ``abstract-ind-ror.ec`` in Emacs. This +should happen automatically if you open any ``.ec`` file. Once you open +the file, you can step through the proof line by line using the +following keystrokes. + +1. Ctrl + c and then Ctrl + n to evaluate one line/block of code +2. Ctrl + c and then Ctrl + u to go back one line/block of code +3. Ctrl + x Ctrl + s to save the file +4. Ctrl + x Ctrl + c to exit Emacs.\* + +.. note:: + + Emacs will prompt you to save the file if you modified it and remind + you that there is an active easycrypt process running. So please pay + attention to the prompts. You need to respond with a “yes” to the + prompt about killing the easycrypt process to exit Emacs. + +These four keybindings should be enough to get you through this file. We +will return to more navigation and other important keybindings in the +next chapter. We include these instructions in the file as well, so you +don’t have to keep switching back and forth. Upon evaluating the first +instructions, the screen should look like so: + +.. figure:: abstract-ind-ror.png + :alt: Working with ``abstract-ind-ror.ec`` + + Working with ``abstract-ind-ror.ec`` + +We will develop the concepts required to work with it in the following +chapters. However, we encourage you to get started working with the tool +and try it out right away. + +Different logics in EasyCrypt +----------------------------- + +Now that we understand that overarching structure of what we can achieve +with EasyCrypt let us get down to the details. + +EasyCrypt allows us to work with mathematical objects and results of +different types. To work with these different results, EasyCrypt has the +following logics: + +1. **Ambient logic**: This is the higher-order logic that allows us to + reason with the proof objects and terms. +2. **Hoare logic and its variants**: + + 1. **Hoare Logic (HL)**: Allows us to reason about a set of + instructions or a single program. + 2. **Relational Hoare Logic (RHL)**: Allows us to reason about a pair + of programs. + 3. **Probabilistic Hoare Logic (pHL)**: When we have a program with + elements of probabilistic behaviour, we need to modify Hoare Logic + to work with the elements of probability. EasyCrypt supports + working with these kinds of programs as well. + 4. **Probabilistic Relational Hoare Logic (pRHL)**: Similarly, pRHL + allows us to reason with pairs of programs with probabilistic + behaviour. + +With these logics, EasyCrypt allows us to verify the security properties +of cryptographic protocols. Most cryptographic proofs are game-based, +implying that we need the ability to work with pairs of programs, as we +saw earlier in the IND-RoR example. This is essentially why we need RHL +and pRHL. + +Apart from these logics, EasyCrypt relies on external SMT solvers to +provide a fair degree of automation. SMT solvers are tools that help to +determine whether a mathematical formula is satisfiable or not. We will +learn to work with these logics and also how to use the external solvers +in the following chapters. diff --git a/doc/tutorials/introduction-itp-program-logics/hoare-logic.ec b/doc/tutorials/introduction-itp-program-logics/hoare-logic.ec new file mode 100644 index 000000000..d7fbec32d --- /dev/null +++ b/doc/tutorials/introduction-itp-program-logics/hoare-logic.ec @@ -0,0 +1,644 @@ +pragma Goals: printall. + +require import AllCore. + +(* +Let us start small and first work with some examples that we saw in the text. +Please pay attention to the syntax of the modules, and capitalization of names. +EasyCrypt (EC) expects the first letters of module names, +and module type names to be capitalized. +*) + +module Func1 = { + proc add_1 (x:int) : int = { return x+1; } + + (* + proc stands for procedure. + Since EC is typed, we are required to mention the + return type of procedures in the definition. + *) + + proc add_2 (x: int) : int = { x<- x + 2; return x; } +}. + +(* +EC allows us to define concretely defined procedures like we did above. +But since we want to model adversaries about whom we know nothing, +we can also define abstract procedures like an eavesdrop procedure. +of an adversary. Like so: +*) +module type Adv = { + proc eavesdrop () : bool +}. + +(* +We don't know what the procedure does, but we do know its return type. +Also notice that now we have a module type and not just a module. +This is because Adv is a type that we will need to instantiate. +We had similar ideas in the abstract-ind-ror.ec +Where the Adversary module type had a "guess" procedure. +We will return to this later when we start working with cryptographic protocols. +But this is an important fact that we need to keep in mind. +*) + +(* +Let us return to hoare triples and take a look at some triples and +try to prove them in EC. +A triple denoted by {P} C {Q} in theory is expressed as +hoare [C : P ==> Q ] in EC, with the usual definitions. +Additionally, the return value of the program C, is stored in a special +keyword called res. +*) + +lemma triple1: hoare [ Func1.add_1 : x = 1 ==> res = 2]. +proof. +(* +When working with hoare logic, or its variants, the goal will be different from +what a goal in ambient logic looks like. We need to start stepping through +the procedure or program that is being reasoned about and change the +preconditions and postconditions according to the axioms and lemmas that we have. +To make progress here, we first need to tell EC what Func1.add_1 is. +The way to do that is by using the "proc" tactic. +It simply fills in the definitions of the procedures that we define. +*) + proc. + +(* +When the goal’s conclusion is a statement judgement whose program is empty, +like we have now the "skip" tactic reduces it to the goal whose conclusion +is the ambient logic formula P => Q, +where P is the original conclusion’s precondition, +and Q is its postcondition. + +Visually, skip works in the following way: + + P => Q + ----------------- skip + {P} skip; {Q} + +skip; denotes an empty program. +While skip next to the line is the tactic itself. +*) + skip. + +(* +Now we are back in familiar territory, except the fact that +we have an interesting "&hr" lurking in the goal. +This refers to the memory in which the program acts. +When we deal with multiple programs, there is a possibility +that the variables come from different memories. So EC provides us +different namespaces to deal with them. +To introduce memory into the context we need to prepend "&" to a variable name. +Like so: +*) + move => &m H1. + + subst. +(* The "subst" tactic simply substitutes variables *) + trivial. +qed. + + +lemma triple2: hoare [ Func1.add_2 : x = 1 ==> res = 3 ]. +proof. + proc. + +(* +Now we have a program which is not empty, +so we can't use the "skip" tactic directly. +Thankfully we learnt about the different axioms in hoare logic. + +When we are faced with +{P} S1; S2; S3; {Q} (with the usual definitions) +applying the "wp" tactic consumes as many ordinary statements as possible from +the end. Then it replaces the postcondition Q, with the weakest precondition R. +R is such that R in conjunction with the consumed statements and the original +post condition hold. It is easier to visualize this in a proof-tree. +For instance, when we have +{P} S1; S2; S3; {Q} and +S2; S3 are statements that can be dealt with some axioms or logical deductions, +then wp does the following: + + -----------------(Other rules) + {P} S1; {R} {R} S2; S3; {Q} + --------------------------------------seq + {P} S1; S2; S3 {Q} + +The triple {R} S2; S3; {Q} is guaranteed to hold, and +hence the goal transforms to +just {P} S1; {R} +*) + +(* +Let us see what happens in our context. +The "wp" tactic consumes the only statement in the program. +In this case an assignment, and replaces the variable like we'd expect. +When we have an empty program, we can simply use the "skip" tactic +and continue with our proof. + + x = 1 => x+2=3 + -------------------------------skip + {x = 1} skip; {x+2=3} + -------------------------------wp + {x = 1} x:= x+2 {x=3} +*) + + wp. + skip. + move => &m x. + subst. + trivial. +qed. + +(* +Let us define some more simple functions and hoare triples to work with. +*) +module Func2 = { + proc x_sq (x:int) : int = { return x*x; } + proc x_0 (x:int) : int = { x <- x*x; x<- x-x; return x; } + proc x_15 (x:int) : int = { x <- 15; return x; } +}. + +(* +Exercises: +Define a few triples relating the behaviour of these functions. +For instance try to define the following triples and prove them: +1. {x = 2} Func2.x_sq {res = 4} +2. {x = 10} Func2.x_0 {res = 0} +3. {true} Func2.x_15 {res = 15} +*) + +(* Using some automation *) + +(* +We generally don't want to be dealing with the low-level proofs, +so we will be combining Hoare logic with the external solvers +that we saw earlier. One thing to remember is that the external +solvers work only with ambient logic goals. +So we need to get the goals state to something that the smt solvers +can work with. +*) + +lemma triple3: hoare [ Func2.x_sq : 4 <= x ==> 16 <= res ]. +proof. +proc. +skip. +move => &m H1. +(* +Here this conclusion is trivial for us to understand and prove on paper +however it can be quite hard to do with EC, so we will simply outsource it to smt. +The external provers are quite powerful, and can make our life easier. +*) +smt. +qed. + +(* +Now let us look at the special cases that we had in the text. +Namely: {true} C {Q}, and {false} C {Q}. +*) +lemma triple4: hoare [ Func2.x_0 : true ==> res=0 ]. +proof. +proc. +wp. +skip. +move => &m T x. +by simplify. +(* Prepending the "by" keyword to a tactic +tries to close the goals by applying trivial +to the result of the tactic, and fails if the goal can't be closed *) +qed. + +(* +"by" is called a tactical. Tacticals are commands that can work with +other tactics. We will see more later. +*) + +(* +So far so good, that was pretty much what we expected. +However let us take a look at the next lemma. Now we are looking at the triple: +{false} x:=15 {x = 0}. +This shouldn't hold, but watch what happens. +*) + +lemma triple5: hoare [ Func2.x_15 : false ==> res=0 ]. +proof. +proc. +wp. +skip. +move => _ f. + +(* +The underscore essentially is a pattern for introduction +which tells EC to ignore whatever is in that position. +Here since we have a "forall _" in the goal already, we tell EC to ignore it. +You could also use a "?", to let EC decide what to call the variable being moved +to the assumptions. +*) + +(* +Pause here for a moment and ponder about what the goal currently says. +It says that assuming that "false" holds, we want to prove that 15 = 0. +As absurd as it is, we know that "false" is the strongest statement there is. +And we have arrived at a state where "false" holds. +This would imply that anything and everything can be derived from false. +Hence we can actually "prove" that 15 = 0. +*) +trivial. +qed. + +(* +The point to understand here is that we could only do this +because we moved "false" into the context manually when we used the "move" tactic. +So our math is still consistent and the world hasn't exploded yet. +The way to think about this triple is assuming "false" holds implies that 15 = 0. +*) + + +(* +Let us now work with some more interesting functions and triples. +The flipper function simply returns the opposite of the boolean +value that it gets. +*) + +module Flip = { + +proc flipper (x: bool) : bool = + { + var r: bool; + if (x = true) + { r <- false; } + else + { r <- true; } + return r; + } +}. + +lemma flipper_correct_t: hoare [ Flip.flipper : x = true ==> res = false ]. +proof. + proc. + (* + When the first statement of the program is an if condition, we can use the + "if" tactic to branch into two different goals with appropriate truth values for + the if condition. + In our case, the goal branches into x = true, and x <> true based, and these + conditions are added to the preconditions. + *) + if. + (*Goal 1: x = true *) + auto. + + (* + If the current goal is a HL, pHL, pRHL statement the "auto" tactic + uses various program logic tactics in an attempt to reduce the goal + to a simpler one. It never fails, but may fail to make any progress. + In this usage, it replaces "wp. skip. and trivial." + *) + + (* Goal 2: x <> true. + Yields a contradiction in the assumptions. + Since our precondition states that x = true /\ x <> true + We will use some automation to deal with it. + *) + auto. + smt. +qed. + +(* +Notice the repetition of proof steps in the branches. +This can be reduced by using tacticals. +In order to tell EC to repeatedly use certain tactics on all +resulting goals, we use the ";" tactical. +So, we can simplify the above proof like so: +*) + +lemma flipper_correct_f: hoare [ Flip.flipper : x = false ==> res = true ]. +proof. + proc. + if; auto; smt. +qed. + +(* +However, since this program is quite simple we can actually make the proof +shorter. We can also make the logic more abstract like so. Please note how we do this, +since we will use it again. +*) + +lemma flipper_correct (x0:bool): + hoare [ Flip.flipper : x = x0 ==> res <> x0 ]. +proof. + proc. + auto. + smt. +qed. + +(* +This is how proofs are polished and made shorter. We first write a verbose proof, +then keep experimenting to find shorter and more elegant proofs. +*) + +(* +Let us define the exponentiation function that we saw in the text. +*) + +module Exp = { + proc exp (x n: int) : int = + { + var r, i; + r <- 1; + i <- 0; + while (i < n){ + r <- r*x; + i <- i+1; + } + return r; + } +}. + + +(* +Let us formulate a hoare triple that says that exp(10, 2) = 100. +The triple would be: +{x = 10 /\ n=2} Exp.exp {res=100} +and in EC, we would write it like so. +*) + +lemma ten_to_two: hoare [ Exp.exp : x = 10 /\ n = 2 ==> res = 100 ]. +proof. + proc. + +(* +When working with tuples EC has the syntax of using backticks (`) to address the tuple. +So (x,n).`1 refers to x. +Often the output from EC can be quite hard to read, simplifying it can sometimes help. +*) + simplify. + +(* +Now we want to reason with a while loop in the program. +Thankfully, we can see that the loop only runs twice, since n=2. +To get a feel of how the program runs we can step through a loop +using the "unroll" tactic. We need to mention the line number of the +program where we want the tactic to apply. Like so: +*) + unroll 3. + unroll 4. + +(* +At this point, we now have two if conditions which we know will hold, +and a while loop for which the condition will not hold. To reason with +loops and conditions like these EC provides two tactics +rcondt, and rcondf. +You can read them as: remove condition with a true/false assignment. +Since here we know that the condition will evaluate to false, we will use the +rcondf version. +*) + + rcondf 5. +(* +Notice how the postcondition now requires the condition for the while loop +to be false. +Since it would evaluate to false, EC gets rid of the loop. +Now we can either use the if tactic that we used earlier to work with the +if conditions here, but wp is generally strong enough to reason with if conditions. +So let us make our lives a little easier and use that instead. +Here, since the program is quite simple, the smt solvers can complete the proof. +However, pay attention to how hard it gets to read the output +after the application of wp, and skip. +*) + wp. + skip. + smt. + +(* +Goal #2: +Again, we have two "if" conditions, that we need to work with. +The proof proceeds the same way as before. wp is strong enough to reason with it. +*) + + wp. + skip. + smt. +qed. + +(* +As usual we could have used some tacticals to shorten the proof. +So let us do that, to clean up the previous proof. +*) + +lemma ten_to_two_clean: hoare [ Exp.exp : x = 10 /\ n = 2 ==> res = 100 ]. +proof. + proc. + unroll 3. + unroll 4. + rcondf 5; auto. +qed. + +(* +For a loop that unrolls twice it is easy to do it manually. +However, this strategy wouldn't work for a different scenario. +For instance in order to prove that the program works correctly we need to prove +the correctness for every number, so we would prefer to work with abstract symbols +and not concrete numbers like 10^2. +In order to work up to it, let us prove that 2^10 works as intended. +But first, we need to understand that EC was not built for computations. +It can handle small calculations like we've seen so far but asking EC to do 2^10 +doesn't work as we'd like it to. +For instance, take a look at the following lemma, and our attempt to prove it. +*) + +lemma twototen: 2^10 = 1024. +proof. + trivial. + simplify. + auto. +(* +None of those tactics do anything +Even smt doesn't work. +You can try it as well. +Again, the point here is that, these kinds of tasks aren't what EC was +built for. +For the time being we will admit this lemma, since we know that +2^10 is in fact 1024. +We need this to prove the next few lemmas relating to hoare triples. +*) + admit. +qed. + +lemma two_to_ten: hoare [ Exp.exp : x = 2 /\ n = 10 ==> res = 1024 ]. +proof. + proc. + simplify. +(* +To get rid of the loop, we need to understand the behavior of the program, and +figure out a loop invariant. This is because we have the tactic: +"while I" +Where "I" is the loop invariant, that holds before and after the loop. +This essentially means thinking about what the loop actually does, +and the conditions that hold before and after the execution of the loop. +We want the invariant to help us prove the goal that we have. +Which is r = 1024. Let us try to see how we can get there. +Let us start small and say that we know that (x = 2) holds before +and after the execution of the loop. +*) + while ( x = 2 ). +(* +Observe how the goals have changed. +In Goal #1, the invariant that we propose is in both the pre and post conditions. +The burden of the proof still lies on us however. Of course, since we don't +change x, this should hold quite naturally. And we can discharge Goal #1 quite +easily. +*) + wp. + auto. + +(* +Now let us pay attention to what we have left. +The second part of the postcondition says +forall (i0, r0 : int), +given that i0 is greater than or equal to n, and x = 2 +then r0 = 1024. +That is clearly incorrect, since r0 isn't bound or related to x or i0. +You are welcome to experiment and try to see how far you can get in +the proof. However in our attempt, the goal simply becomes harder to read. +Using wp, and skip introduces memory into the context making it quite difficult to +read. We will "abort" this attempt here, and try to think of a stronger invariant. +*) +abort. + +lemma two_to_ten: hoare [ Exp.exp : x = 2 /\ n = 10 ==> res = 1024 ]. +proof. + proc. + +(* +As an additional invariant, we know that the loop runs until our +loop variable i goes from 0, to n. So as an invariant, we have +0 <= i <= n, and the control exits the loop when ! (i < n). +Let us try to see what happens if we add this in. +*) + while ( x = 2 /\ 0 <= i <= n). + wp. + auto. + smt. + +(* +Let us read what the goal says now. +Again it says something about r0 without bounding what r0 can be. +This attempt will also fail. +So we need to understand what happens to the variable r0, at the end of every +iteration of the loop. +*) +abort. + + +lemma two_to_ten: hoare [ Exp.exp : x = 2 /\ n = 10 ==> res = 1024 ]. +proof. + proc. +(* +We know that after every iteration, the variable r is multiplied by x. +So in this case, since we have x = 2, essentially at the end of +i iterations of the loop we have the fact that r = 2^i. +This is an invariant, and it binds r to the variables that are passed to the +loop. Let us see if this attempt works. +*) + while (x = 2 /\ 0 <= i <= n /\ r = 2^i). + +(* +Again, Goal #1 will go through quite easily. +*) + wp. + skip. + smt. + +(* Goal #2 *) + wp. + simplify. + auto. +(* +When the goal is too complicated to read, we can apply the tactic "progress". +"progress" breaks the goals into simpler ones by repeatedly applying the +"split", "subst" and "move =>" tactics and trying to solve trivial goals automatically. +*) + progress. + +(* 2 ^ 0 = 1 *) + smt. + +(* 2^10 = 1024 *) + smt. +qed. + +(* +A point to note here: +Had we not admitted the lemma twototen the proof would get stuck +You are welcome to comment it out and try the proof again. +*) + +(* +So finally, we have an invariant that works. +Let us clean up the proof, and also if we think about it, +the condition (x=2) isn't really needed, since the program never +modifies the value of x. So let us get rid of that condition as well. +*) + +lemma two_to_ten_clean: hoare [ Exp.exp : x = 2 /\ n = 10 ==> res = 1024 ]. +proof. + proc. + simplify. + while ( r = x^i /\ 0 <= i <= n); auto; smt. +qed. + +(* +Now the proof seems so innocuous and straightforward. +However, it is important to understand that these proofs and +figuring out the loop invariants always take a few tries, and +sometimes crafting the right invariant can be an art by itself. +This also gets quite hard when there are a lot of variables +to keep track of. So it is good practice to work with smaller examples first. +*) + + +(* +Now let us try to work with abstract symbols, the stuff that EC +was actually built for. Here we mentioned in the text, in order to claim +that the exp function is correct, we need to have the condition that +the exponent that we provide is greater than zero. +We use x0, and n0, in order to differentiate from the program variables. +*) +lemma x0_to_n0_correct (x0 n0: int): + 0 <= n0 => + hoare [ Exp.exp : x = x0 /\ n = n0 ==> res = x0 ^ n0 ]. +proof. + move => Hn0. + proc. + while (r=x^i /\ 0 <= i <= n). + wp. + skip. + smt. + + wp. + skip. + progress. + smt. + smt. +qed. + + +(* +Again, we can clean up the proof like so: +Notice that we omit the type declaration of x0 and n0, +since EasyCrypt can figure it out by itself. +*) +lemma x0_to_n0_correct_clean x0 n0: + 0 <= n0 => + hoare [ Exp.exp : x = x0 /\ n = n0 ==> res = x0 ^ n0 ]. +proof. + move => Hn0. + proc. + while (r=x^i /\ 0 <= i <= n); auto; smt. +qed. + +(* +As an exercise, you can do similar proofs for the following mathematical functions: +1. A program to decide if a given number is even or odd. +2. A program to compute the factorial of a given number. +*) diff --git a/doc/tutorials/introduction-itp-program-logics/hoare-logic.rst b/doc/tutorials/introduction-itp-program-logics/hoare-logic.rst new file mode 100644 index 000000000..2434c8897 --- /dev/null +++ b/doc/tutorials/introduction-itp-program-logics/hoare-logic.rst @@ -0,0 +1,806 @@ +Working through the chapter on ambient logic should give you a good +grasp of the ambient logic and tactics for reasoning with simple math. +Up until now, we were working with mathematical proofs that only used +logical reasoning. However, when working with programs and procedures we +need a way to reason with what the programs do. + +For instance, let us think about an exponentiation program for integers +like so: + +:: + + exp(x, n): + r = 1 + i = 0 + while (i < n): + r = r * x + i = i + 1 + return r + +When presented with a program like this, our objective is to figure out +if the program behaves correctly. At first glance, this program seems +correct. However, a glaring mistake here is that the program will always +return :math:`1` as a result if we pass any negative integer as the +second argument. That isn’t the behaviour we expect from an +exponentiation function. So saying that the program is correct would be +a false claim. So to make claims about the behaviour of the program, +mathematically, we would say something like: + +.. math:: \text{Given } \underbrace{x \in \mathbb{Z}, n \in \mathbb{Z} \text{ and } n \ge 0 }_a \ \ \ \underbrace{exp(x, n)}_b \text{ returns } \underbrace{r = x ^{n}}_c + +.. math:: \text{Where } a \text{ is the precondition}, b \text{ is the program}, c \text{ is the postcondition} + +The Hoare triple +---------------- + +As marked in the statement above, claims that we make generally have +three distinct parts: preconditions, the program and postconditions. +Hoare logic formalises these three parts and introduces them as a +**Hoare triple**. + +A Hoare triple is denoted like so: + +.. math:: \{ P \} \ C \ \{ Q \} + +Here :math:`P,Q`, are conditions on the program variables used in +:math:`C`. Conditions on program variables are written using standard +mathematical notations together with logical operators like +:math:`\wedge` (‘and’), :math:`\vee` (‘or’), :math:`\neg` (‘not’) and +:math:`\implies` (‘implies’). Additionally, we have special conditions +:math:`true` or :math:`T` which always holds, and :math:`false` or +:math:`F` which never holds. + +:math:`C` is a program in some specified language. + +We say that a Hoare triple, :math:`\{P\} \ C \ \{Q\}`, holds if whenever +:math:`C` is executed from a state satisfying :math:`P` and if the +execution of :math:`C` terminates, then the state in which :math:`C`\ ’s +execution terminates satisfies :math:`Q`. We will limit our discussion +to programs which terminate. + +Examples +~~~~~~~~ + +1. :math:`\{ x = n \} \ x:= x+1 \ \{ x = n+1 \}` holds. ( :math:`:=` is + the assignment operator) +2. :math:`\{ x = n \} \ x:= x+1 \ \{ x = n+ 2 \}` doesn’t hold. +3. :math:`\{ true \} \ C \ \{ Q \}` is a triple in which the + precondition always holds. So we’d say that this triple holds for + every :math:`C` that satisfies the postcondition :math:`Q`. +4. :math:`\{ P \} \ C \ \{ true \}`, similarly, this triple holds for + every precondition :math:`P` that is satisfied, and every program + :math:`C`. +5. :math:`\{ false \} \ C \ \{ Q \}`, is an interesting triple which, + according to our definitions, doesn’t hold since false is a statement + that never holds. However, this is a slightly special case, as we + will see in EasyCrypt. + +Exercises +~~~~~~~~~ + +1. Does :math:`\{ x=1 \} \ x:=x+2 \ \{ x=3 \}` hold? +2. How about :math:`\{ true \} \ exp(x,a) \ \{ r=x^a \}`? Why? +3. What about :math:`\{ 2=3 \} \ x:=1 \ \{ x=1 \}`? + +Strength of statements +---------------------- + +Informally, if a statement can be deduced from another, then the +statement that was deduced is a weaker statement. + +Mathematically if we have :math:`P \implies Q`, we say that :math:`P` is +a stronger statement than :math:`Q`. + +For example, + +.. math:: x = 5 \implies x \ge 5 + +.. math:: x = 5 \text{ is a stronger statement than } x \ge 5 + +As discussed earlier, we have two special statements, :math:`true`, +which always holds, and :math:`false`, which never holds. These are the +weakest and the strongest statements there are, respectively. + +Since any statement that holds can imply that :math:`true` holds. The +reason is that it always holds, :math:`true` is the weakest statement +there is. + +Similarly, :math:`false` never holds. So, no statement can imply +:math:`false`; hence, it is the strongest statement there is. + +Proof trees +----------- + +So far, we looked at Hoare triples for simple statements, these can be +thought of “programs” with a single instruction as well. However, we +need to be able to work with multiple statements and more complex +statements. We achieve this by formalizing a set of axioms that we +believe to be true, and then we combine these axioms to make claims +about complex statements. We often visualize these series of steps in +which we put the axioms together into *schemas* or *proof trees*. + +For example: For a statement :math:`S`, we say it is or provable by +denoting it with a turnstile (:math:`\vdash`) symbol like so +:math:`\vdash S`, and its proof can be denoted by: + +.. math:: \dfrac{\vdash S_1, \vdash S_2, \dots ,\vdash S_n}{\vdash S} + +This says the conclusion :math:`S` may be deduced from the +:math:`S_1, \dots, S_n` which are the hypotheses of the rule. The +hypotheses can either all be theorems or axioms of Hoare Logic or +mathematics. + +Now, we will take a look at some of the axioms of Hoare logic with +examples to give you a flavour of how they work. One of the reasons we +cover these is because these axioms form the basis for the tactics we +use in Hoare logic in EasyCrypt. Of course, the main idea is to +familiarize the reader with the basics since the main goal is for the +machine to take care of the specifics. + +Axioms of Hoare logic +--------------------- + +1. **Assignment**: + + .. math:: \vdash \{P[E/V ]\} \ V :=E \ \{P\} + + Where :math:`V` is any variable, :math:`E` is any expression, + :math:`P` is any statement, and the notation :math:`P[E/V]` denotes + the result of substituting the term :math:`E` for all occurrences of + the variable :math:`V` in the statement :math:`P`. + + Example: :math:`\vdash \{ y = 5 \} \, x := 5 \,\{ y = x \}` + +2. **Precondition strengthening**: When we have a Hoare triple + :math:`\{ P ' \}\ C \ \{ Q \}`, where :math:`P'` is a statement that + follows from a stronger statement, :math:`P`. Then we can say, + + .. math:: \dfrac{\vdash P \implies P', \vdash \{P'\}\ C \ \{Q\}} {\vdash \{P\} \ C \ \{Q\}} + + Example: Let + + .. math:: C = [x:=x+2] + + .. math:: P = \{x = 5\} + + .. math:: P' = \{x \ge 5\} \text{ , and} + + .. math:: Q = \{x \ge 7\} + + Using the precondition strengthening axiom we have, + + .. math:: \dfrac{\vdash \{x = 5\} \implies \{x \ge 5\} ,\ \vdash \{x \ge 5\} \ x:=x+2 \ \{x \ge 7\} } {\vdash \{x=5\} \ x:= x + 2 \ \{x \ge 7\}} + +3. **Postcondition weakening**: Similarly, when we have a Hoare triple + :math:`\{P\}\, + C \,\{Q'\}`, where :math:`Q'` is a strong statement, and if :math:`Q` + follows from :math:`Q'`. Then we can say, + + .. math:: \dfrac{\vdash \{P\}\ C \ \{Q'\}, \ \vdash Q' \implies Q}{ \vdash \{P\} \ C \ \{Q\}} + + Example: Let + + .. math:: C = [x:=x+2] + + .. math:: P = \{x = 5\} + + .. math:: Q' = \{x = 7\} \text{ , and} + + .. math:: Q = \{x \ge 7\} + + With the postcondition weakening axiom, we have, + + .. math:: \dfrac{\vdash \{x = 5\}\ x:=x+2 \ \{x =7\}, \ \vdash x = 7 \implies x \ge 7 } {\vdash \{x=5\} \ x:= x + 2 \ \{x \ge 7\}} + + Together the precondition strengthening and postcondition weakening + axioms are known as the + + .. math:: \textbf{consequence rules} + + . + +4. **Sequencing**: For two programs :math:`C_1, C_2`, we have + + .. math:: \dfrac{ \vdash \{P\}\ C_1 \ \{Q'\}, \ \vdash \{Q'\}\ C_2 \ \{Q\}, }{ \vdash \{P\}\ C_1;C_2 \ \{Q\} } + + Example: Let + + .. math:: C_1 = [x:=x+2] + + .. math:: C_2 = [x:=x*2] + + .. math:: P = \{x = 5\} + + .. math:: Q' = \{x = 7\} \text{ , and} + + .. math:: Q = \{x = 14\} + + Using the sequencing axiom, we have, + + .. math:: \dfrac{ \vdash \{x = 5\} \ x:=x+2 \ \{x =7\}, \ \vdash \{x = 7\}\ x:=x * 2 ,\{x =14\} } {\vdash \{x=5\} \ x:= x + 2, x:= x * 2 \ \{x =14\}} + +We go through these examples to get a sense of what formal proof trees +look like and the theory that formal verification is based on. The proof +trees that we’ve used are already simplified to exclude the assignment +axiom and steps that we as humans can easily understand and gloss over. +Proof trees get quite large and unwieldy as soon as we do anything +non-trivial. This is exactly where formal verification tools come into +the picture. So, let us now switch to EasyCrypt and work with Hoare +triples. + +Hoare logic has been studied quite extensively, and there are plenty of +good textbooks (`Textbook 1 `__, +`Texbook +2 `__) +that one can refer to for mathematical rigour and completeness. The +objective here is to give the reader an intuitive understanding of the +math, and enough working knowledge required to work with EasyCrypt. + +HL in EasyCrypt +--------------- + +With a basic understanding of HL, we can now proceed to work with it in +EasyCrypt. We will work through the file +```hoare-logic.ec`` `__. +As before, it is recommended to work with the file in the Proof General ++ Emacs environment. However, reading through this section provides the +basic ideas developed in the practice file. + +Basic Hoare triples +~~~~~~~~~~~~~~~~~~~ + +Let us start small and first work with some examples that we saw +earlier. We first define a module to define two procedures for the +programs. + +:: + + module Func1 = { + proc add_1 (x:int) : int = { return x+1; } + proc add_2 (x: int) : int = { x <- x + 2; return x; } + }. + +A Hoare triple denoted by :math:`\{P\} \ C\ \{Q\}` in theory is +expressed as ``hoare [C : P ==> Q ]`` in EasyCrypt, with the usual +definitions. Additionally, the return value of the program, :math:`C`, +is stored in a special keyword called ``res``. + +So the triple, :math:`\{x=1 \} \ \text{Func1.add}\_\text{1} +\ \{x=2\}`, would be expressed in EasyCrypt like so: + +:: + + lemma triple1: hoare [ Func1.add_1 : x = 1 ==> res = 2]. + +When working with Hoare logic or its variants, the goal will be +different from what a goal in ambient logic looks like. For instance, +evaluating the ``lemma triple1`` produces the following goal. + +:: + + Current goal + Type variables: + --------------------------------------------- + pre = x = 1 + + Func1.add_1 + + post = res = 2 + +We need to start stepping through the procedure or program that is being +reasoned about and change the preconditions and postconditions according +to axioms and lemmas that we have. + +To make progress here, we first need to tell EasyCrypt what +``Func1.add_1`` is. The way to do that is by using the ``proc`` tactic. +It simply fills in the definitions of the procedures that we define. +Since ``Func1.add_1`` is made up of only a return statement, ``proc`` +replaces ``res`` with the return value. This leaves us with an empty +program. This is what we want to work towards; using different tactics +we would like to change the preconditions and postconditions depending +on what the programs that we are reasoning with do. Once we have +consumed all the program statements, we can transform the goal from a HL +goal to a goal in ambient logic using the ``skip`` tactic. ``skip`` does +the following: + +.. math:: \dfrac{ P \implies Q}{\{P\} \text{ skip; } \{Q\}}\texttt{skip} + +.. math:: \text{skip;} + +\ signifies an empty program, while + +.. math:: \texttt{skip} + +is the tactic itself. + +This puts us back in the familiar territory of ambient logic, and we can +use all the tactics that we learnt in ``ambient-logic.ec``. The only +difference is that transitioning a goal from Hoare logic to ambient +logic introduces some qualifiers about the memory that the program works +on. Hence, we need to handle those as well. In this example, the goal +after evaluating ``skip`` will simply read: +``forall &hr, x{hr} = 1 => x{hr} + 1 = 2``. The proof for which follows +pretty trivially. The only difference is that we need to move the memory +into the assumption by prepending the & character in the ``move =>`` +tactic. + +So the full proof for this simple example looks like so: + +:: + + lemma triple1: hoare [ Func1.add_1 : x = 1 ==> res = 2]. + proof. + proc. + skip. + move => &m H1. (* &m moves memory to the assumption *) + subst. (* Substitutes variables from the assumptions *) + trivial. + qed. + +Now let us work with a program where the body is not empty. + +:: + + lemma triple2: hoare [ Func1.add_2 : x = 1 ==> res = 3 ]. + +Using ``proc`` produces the following goal. + +:: + + Current goal + Type variables: + --------------------------------------------- + Context : Func1.add_2 + + pre = x = 1 + + (1) x <- x + 2 + + post = x = 3 + +When we are faced with :math:`\\{P\\} S1; S2; S3; \\{Q\\}` with the +usual definitions, applying the ``wp`` tactic consumes as many ordinary +statements as possible from the end. Then it replaces the postcondition +:math:`Q`, with a precondition :math:`R`. :math:`R` is chosen such that +it holds in conjunction with the consumed statements and the original +postcondition and it is as weak as possible (*w*\ eakest +*p*\ recondition). It is easier to visualize this in a proof tree. + +For instance, when we have :math:`\{P\} S1; S2; S3; \{Q\}` and +:math:`S2; S3;` are statements that can be dealt with some axioms or +logical deductions, then ``wp`` does the following: + +.. math:: \dfrac{\{P\} S1; \{R\} \ \ \dfrac{...}{\{R\} S2; S3; \{Q\}}\text{\tiny{(Other rules)}}}{\{P\} S1; S2; S3; \{Q\}}\texttt{seq} + +The judgement :math:`\{R\} S2; S3; \{Q\}` is guaranteed to hold, and +hence the goal transforms to just :math:`\{P\} S1; \{R\}`. + +In our context, ``wp`` consumes the only instruction that we have in the +program and produces the judgement +:math:`\{x = 1\} \ \text{skip;} \ \{x+2=3\}` to which we apply ``skip``. +This gives us the following proof-tree: + +.. math:: \dfrac{x = 1 \implies x+2=3}{ \dfrac{ \{x = 1\} \ \text{skip;} \ \{x+2=3\} }{ \{x = 1\} \ x:= x+2 \ \{x=3\} }\texttt{wp}}\texttt{skip} + +Putting us back in familiar territory, and the proof follows quite +easily. + +:: + + lemma triple2: hoare [ Func1.add_2 : x = 1 ==> res = 3 ]. + proof. + proc. + wp. + skip. + move => &m x. + subst. + trivial. + qed. + +Automation, and special cases +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Now that we have an understanding of how we can make progress, let us +take a look at how we can use automation since we still have powerful +external solvers at our disposal and we would like to use them whenever +we can. We will be working with the following procedures in this +section. + +:: + + module Func2 = { + proc x_sq (x:int) : int = { return x*x; } + proc x_0 (x:int) : int = { x <- x*x; x <- x-x; return x; } + proc x_15 (x:int) : int = { x <- 15; return x; } + }. + +For instance, let us take a look at a triple, which states that if you +square any integer greater than or equal to 4, the result is greater +than or equal to 16. Pretty trivial and straightforward when you think +about it. However, the proof for something simple like this becomes +quite tiresome, hence we will simply ask ``smt`` to handle it. The only +issue however is that smt solvers can only work on goals in ambient +logic. So it is up to us to bring the goal to a state that doesn’t +involve Hoare logic. In this example, since ``x_sq`` consists of a +single ``return`` statement, ``proc`` and ``skip`` are enough. + +:: + + lemma triple3: hoare [ Func2.x_sq : 4 <= x ==> 16 <= res ]. + proof. + proc. + skip. + smt(). + qed. + +Let us now look at the triple +:math:`\{\text{false}\} \ x:=15 \ \{x = 0\}.` + +Theoretically, we know that this triple doesn’t hold, since ``false`` +never holds. We have the ``proc x_15`` in the ``module Func2`` that we +can use to express that triple in EasyCrypt. The interesting thing is +that we can actually write proof for the triple in question. + +:: + + lemma triple4: hoare [ Func2.x_15 : false ==> res=0 ]. + proof. + proc. + wp. + skip. + move => _ f. + trivial. + qed. + +The reason we can do this is that we essentially force the assumption +that ``false`` holds and we want to prove the postcondition +:math:`15 = 0`. As absurd as it is, we know that ``false`` is the +strongest statement there is. By getting EasyCrypt to the state where +``false`` holds would imply that anything and everything can be derived +from it. Hence we can actually “prove” that :math:`15 = 0`. + +The point to understand here is that we could only do this because we +moved ``false`` into the context manually when we used the ``move =>``. +So our math is still consistent and the world hasn’t exploded yet. The +way to think about this triple is assuming ``false`` holds implies that +:math:`15 = 0`. + +Conditionals and loops +~~~~~~~~~~~~~~~~~~~~~~ + +Let us now work with some more interesting functions and triples. We +define a flipper function which simply returns the opposite of the +boolean value that it gets. + +:: + + module Flip = { + + proc flipper (x: bool) : bool = + { + var r: bool; + if (x) + { r <- false; } + else + { r <- true; } + return r; + } + }. + +Let us say that we would like to prove the fact related to this program, +that if the input is :math:`\{\text{true}\}`, +:math:`\texttt{Flip.flipper}` returns :math:`\{\text{false}\}`. + +We use a slightly verbose proof here to demonstrate how to open up an +``if`` block. Using the ``if`` tactic in the proof script gives us two +goals, one in which the ``if`` condition holds, and another in which it +doesn’t. In our case, it splits into one goal with ``x = true``, and +another with ``x <> true``. Additionally, when the current goal is a HL, +pHL, pRHL statement the ``auto`` tactic uses various tactics in an +attempt to reduce the goal to a simpler one automatically. It never +fails, but it may fail to make any progress. For instance, in this first +usage of the tactic, it does the job of the ``wp, skip, and trivial`` +tactics. + +:: + + lemma flipper_correct_t: + hoare [ Flip.flipper : x = true ==> res = false ]. + proof. + proc. + if. + (* Goal 1: x = true *) + auto. + + (* Goal 2: x <> true. *) + auto. + smt. + qed. + +Notice the repetition of proof steps in the branches. This can be +reduced by using tacticals. In order to tell EasyCrypt to repeatedly use +certain tactics on all resulting goals, we use the “;” tactical. So, we +can simplify the above proof like so + +:: + + lemma flipper_correct_f: + hoare [ Flip.flipper : x = false ==> res = true ]. + proof. + proc. + if; auto; smt. + qed. + +However, since this program is quite simple we can actually make the +proof shorter. We can also make the logic more abstract like so: + +:: + + lemma flipper_correct (x0: bool): + hoare [ Flip.flipper : x = x0 ==> res <> x0 ]. + proof. + proc. + auto. + smt. + qed. + +This is how proofs are polished and made shorter. We first write a +verbose proof, then keep experimenting to find shorter and more elegant +proofs. + +Let us now increase the difficulty and work with a slightly more +involved example. We define the exponentiation function that we saw +earlier in EasyCrypt. + +:: + + module Exp = { + proc exp (x n: int) : int = + { + var r, i; + r <- 1; + i <- 0; + while (i < n){ + r <- r*x; + i <- i+1; + } + return r; + } + }. + +Let us formulate a Hoare triple that says that ``exp(10, 2) = 100``, +since of course :math:`10^2 = 100`. + +We would have the triple + +.. math:: \{x = 10 \wedge n=2 \}\ \text{Exp.exp}\ \{\text{res}=100\} + +. In EasyCrypt we would state the lemma like we have done earlier. For +the proof, we will employ loop unrolling. We adopt this method since we +know that the while loop will be executed twice, and we can work through +those manually. To unroll a loop with ``unroll n``, where ``n`` is the +line of code with the loop statement, a ``while`` loop in our case. With +the loops unrolled, we get two if conditions which we know will hold, +and a while loop for which the condition will not hold. To reason with +loops and conditions like these EasyCrypt provides two tactics +``rcondt``, and ``rcondf``. They can be read as “remove the condition +with a true/false assignment”. We will use the ``rcondf`` version. This +forces us to prove that the boolean in the ``while`` block, ``(i res = 100 ]. + proof. + proc. + simplify. (* Makes the goal more readable *) + unroll 3. + unroll 4. + rcondf 5. + (* post = !(i res = 100 ]. + proof. + proc. + unroll 3. + unroll 4. + rcondf 5; auto. + qed. + +For a loop that unrolls twice, it is easy to do it manually. However, +this strategy wouldn’t work for a different scenario. For instance, in +order to prove that the program works correctly, we need to prove the +correctness for every number, so we would prefer to work with abstract +symbols and not concrete numbers like :math:`10^2`. In order to work up +to it, let us try to prove that :math:`2^{10}` works as intended. But +first, we need to understand that EasyCrypt was not built for +computations. It can handle small calculations like we’ve seen so far +but asking EasyCrypt to do :math:`2^{10}` doesn’t work as we’d like it +to. For instance, take a look at the following lemma, and our attempt to +prove it. + +:: + + lemma twototen: 2^10 = 1024. + proof. + (* We can't make any progress with these. *) + trivial. + simplify. + auto. + (* + smt fails as well, we will admit this result, + since we know it is true. + *) + admit. + qed. + +Again, the point here is that EasyCrypt wasn’t built for tasks like +these. For the time being, we will admit this lemma, since we know that +:math:`2^{10}` is in fact 1024. We need this to prove the next few +lemmas relating to Hoare triples. + +At this point, we’d like to prove that ``exp(2,10)`` works as expected, +however, we can’t do so with direct computation since it would be +painful and also not the purpose of using EasyCrypt, so to reason with +loops, we need to be able to think of loop invariants and think about +the program variables which change. For instance, we know that the +variable ``x`` remains the same throughout the computation. So let us +try to get rid of the ``while`` loop stating that this is the only +invariant. We know that this is obviously not enough, since doing this +will in a sense forget about what happens to the other variables. +However, examples that get stuck are instructive as well as they allow +us to understand what we did wrong. The following proof reaches a point +in which the postcondition states: + +``post = ... forall (i0 r0 : int), ! i0 < n => x = 2 => r0 = 1024}`` + +This can’t hold since it states that the result ``r0`` is 1024 for every +``r0``, hence we abort this attempt. + +:: + + lemma two_to_ten: + hoare [ Exp.exp : x = 2 /\ n = 10 ==> res = 1024 ]. + proof. + proc. + simplify. + while ( x = 2 ). + wp. + auto. + abort. + +Similarly, we try another invariant which helps, but still gets stuck +since it doesn’t account for how the variable ``r`` changes after every +iteration of the loop. We abort this attempt as well. + +:: + + lemma two_to_ten: + hoare [ Exp.exp : x = 2 /\ n = 10 ==> res = 1024 ]. + proof. + proc. + while ( x = 2 /\ 0 <= i <= n). + wp. + auto. + smt. + abort. + +We know that after every iteration, the variable ``r`` is multiplied by +``x``. So in this case, since we have ``x = 2``, essentially at the end +of ``i`` iterations of the loop we have the fact that +:math:`\text{r} = 2^\text{i}`. This is an invariant, and it binds r to +the variables that are passed to the loop. With this, we finally have +all the ingredients for the invariant and we complete the proof, like +so: + +:: + + lemma two_to_ten: + hoare [ Exp.exp : x = 2 /\ n = 10 ==> res = 1024 ]. + proof. + proc. + while (x = 2 /\ 0 <= i <= n /\ r = 2^i). + + wp. + skip. + smt. + + wp. + simplify. + auto. + + (* + Sometimes, the goal can be quite complicated, and we + can use "progress" to break it down into smaller goals + *) + progress. + + (* 2 ^ 0 = 1 *) + smt. + + (* 2^10 = 1024 *) + smt. + qed. + +Finally, we have an invariant that works. Let us clean up the proof, and +also if we think about it, the condition ``x=2`` isn’t really needed, +since the program never modifies the value of ``x``. Let us get rid of +that condition while we are at it. + +:: + + lemma two_to_ten_clean: hoare [ Exp.exp : x = 2 /\ n = 10 ==> res = 1024 ]. + proof. + proc. + simplify. + while ( r = x^i /\ 0 <= i <= n); auto; smt. + qed. + +Now the proof seems so innocuous and straightforward. However, it is +important to understand that these proofs and figuring out the loop +invariants always takes a few tries, and sometimes crafting the right +invariant can be an art by itself. This also gets quite hard when there +are a lot of variables to keep track of. So it is good practice to work +with smaller examples first. + +Now let us try to work with abstract symbols, the stuff that EC was +actually built for. In order to claim that the ``exp`` function is +correct, we need to have the condition that the exponent that we provide +is greater than zero. We use ``x0``, and ``n0``, in order to +differentiate from the program variables. + +:: + + lemma x0_to_n0_correct (x0 n0: int): + 0 <= n0 => + hoare [ Exp.exp : x = x0 /\ n = n0 ==> res = x0 ^ n0 ]. + proof. + move => Hn0. + proc. + while (r=x^i /\ 0 <= i <= n). + wp. + skip. + smt. + + wp. + skip. + progress. + smt. + smt. + qed. + +Again, we can clean up the proof like so: + +:: + + lemma x0_to_n0_correct_clean x0 n0: + 0 <= n0 => + hoare [ Exp.exp : x = x0 /\ n = n0 ==> res = x0 ^ n0 ]. + proof. + move => Hn0. + proc. + while (r=x^i /\ 0 <= i <= n); auto; smt. + qed. + +With that we conclude this chapter on Hoare logic. In this chapter we +first presented the theory of Hoare logic, and we saw how to work with +HL in EasyCrypt. Starting with simple Hoare triples we worked our way up +to reasoning with more advanced Hoare triples, and along the way we +learnt some new tactics that allowed us to work with the HL goals. diff --git a/doc/tutorials/introduction-itp-program-logics/preface.rst b/doc/tutorials/introduction-itp-program-logics/preface.rst new file mode 100644 index 000000000..3cf3f807c --- /dev/null +++ b/doc/tutorials/introduction-itp-program-logics/preface.rst @@ -0,0 +1,208 @@ + .. rubric:: “Program testing can be used to show the presence of + bugs, but never to show their absence!” + :name: program-testing-can-be-used-to-show-the-presence-of-bugs-but-never-to-show-their-absence + + .. rubric:: - Edsger W. Dijkstra + :name: edsger-w.-dijkstra + +Building reliable software is extremely tough. In order to guarantee the +reliability of software, there are plenty of different approaches that +can be employed, ranging from testing to various software building +methodologies. However, these are among the weakest guarantees we can +provide or are simply best practices that can ensure some level of +reliability. + +With the explosion of software applications being used, bad software has +also been the source of literal explosions. For instance, NASA lost its +`Mars Climate +Orbiter `__ +in 1998 due to a bug in converting units from the Imperial system to the +SI system. More recently, bad software led to the death of 346 people +onboard `two Boeing 737 MAX airplanes that crashed in 2018 and +2019 `__. +Bad software has proven to be extremely costly. + +On the opposite end of the spectrum of software reliability guarantees +lies the field of formal verification. The core idea behind formal +verification of software is to provide mathematical guarantees of +program behaviour based on specifications. It grew out of the field of +formal methods in mathematics and later computer-aided mathematical +proofs. So, formal verification rests on the firm foundations of formal +logic and reasoning. + +Cryptography also follows the same pattern when it comes to reliability +guarantees. Testing and following best practices are still the go-to +methods to ensure the reliability of most cryptographic protocols; these +methods provide the weakest guarantees, as we discussed above. To +provide stronger guarantees, the ideas of formal verification have been +applied to cryptography, giving rise to the field of formally verified +cryptography. As these fields advanced and became more and more complex, +software tools that could aid us in this process were built. There are +several approaches to formal verification of cryptography, as we will +see. We will focus on one approach to the field (design-level security) +and work with EasyCrypt, a toolset that allows us to verify game-based +cryptographic proofs. + +Formal verification: A brief history +------------------------------------ + +The ideas of formal verification can be traced back to Leibniz’s ideas +about *characteristica universalis* back in the 17th century. He +imagined it to be a universal conceptual language that could be used to +solve logical problems. However, we do not need to go that far back; for +our intents and purposes, formal methods and later computer-aided math +came into the limelight with the famous four-colour theorem being proven +with the help of computers by Appel and Haken (`Part +I `__, +`Part +II `__) +in 1977. + +The hypothesis of the four-colour theorem is quite simple and elegant. +It says, “Any planar map can be coloured with only four colours”. The +computer-aided proof by Appel and Haken attracted plenty of criticism +since it was done by performing an exhaustive case analysis of a billion +cases. An exhaustive case analysis means that the computer went through +every single case that could arise when trying to colour a map and came +back saying that four colours are all it takes. For an elegant problem, +the proposed computer-aided proof felt like using a sledgehammer to +crack a seemingly innocent nut, and this style of theorem proving +polarised the research community. + +Nevertheless, the computer-aided proof of the four-colour theorem is a +significant milestone, and it set off more work and efforts in the field +of computer-aided mathematics. The field has grown considerably since +then, and there are a multitude of tools available for use. For +instance, one can use theorem provers like Coq or Isabelle to formally +prove general mathematical statements with the help of a computer. Or, +one can use specialised tools like EasyCrypt or Tamarin to work with +specific domains of formal verification, like cryptography in this case. +As for the four-colour theorem, a fully computer-free proof is yet to be +discovered. + +Formal verification in cryptography +----------------------------------- + +As the field of formal verification in math took off and got established +over the years, there was a problem brewing in the academic circles +dealing with cryptography. At its core, modern cryptography is based on +math, and to demonstrate different security properties of protocols, we +come up with mathematical proofs and guarantees about them. As the field +advanced, these proofs started getting fairly complex and often too +complicated for humans to go through. This problem can be best +illustrated with this excerpt from a `paper by Shai +Halevi `__: + +“The problem is that as a community, we generate more proofs than we +carefully verify (and as a consequence some of our published proofs are +incorrect). I became acutely aware of this when I wrote my `EME\* +paper `__. After spending a +considerable effort trying to simplify the proof, I ended up with a +23-page proof of security for a — err — marginally useful +mode-of-operation for block ciphers. Needless to say, I do not expect +anyone in his right mind to even read the proof, let alone carefully +verify it.” + +In the paper, Halevi highlights that cryptography as a field has +advanced to the point where the proofs are so complex that the field +could benefit from automation or, at the very least, some help from +machines. In a way, automated and computer-assisted are the two +approaches that are possible in the field of formal verification of +cryptography. + +What is computer-aided cryptography? +------------------------------------ + +At this point, it is a good idea to read `Sec 1.1 of +JoC `__ to understand what +cryptography is and is not. To summarise and add to the ideas from JoC, +modern cryptography deals with three main problems related to the +security of communication. They are the following: + +1. **Privacy**: Protecting information from being accessed by + unauthorised parties +2. **Integrity**: Protecting information from being tampered with or + altered +3. **Authenticity**: Making sure the information is from an authentic + source + +Each of these properties can be defined as a mathematical property of +information, and claiming that a cryptographic protocol protects a +certain property is equivalent to proving that the information possesses +that mathematical property. Given that the proofs can be complicated and +hard to follow, the idea of using computers to verify the proofs comes +in here. + +To illustrate this idea better, let us first meet Alice, Bob and Eve. We +assume that Alice wants to send a message to Bob and wants the +communication to be private. While Eve wants to eavesdrop on their +communication. One way to prove that a system of communication is secure +is to think of Alice, Bob and Eve playing a game where the objective of +the game for Alice and Bob is to communicate in a way that Eve can’t +differentiate between the messages and a random string of characters. +This would mean that Eve can extract just as much information from an +intercepted message as they can extract from random noise, implying that +the communication is private. This game can be modelled mathematically, +and we can prove that the communication was private. Proofs written in +this style are called game-based cryptographic proofs. + +These ideas of representing information security properties as +mathematical properties and the games that Alice, Bob and Eve play +(game-based cryptographic proofs) are essentially the cornerstones of +provable and verifiable security. Depending on the definition of the +games and conditions related to them, the proofs can turn out to be +fairly intricate, as we established earlier. In the worst case, +handwritten proofs could even be wrong. Incorrect proofs translate to +significant security risks and reaffirm the need for the field of +formally verified cryptography. The complexity and difficulty of +verifying these proofs translate to a need for more automation and +computer-aided verification – tools like EasyCrypt are built to do just +that. + +Criticism of computer-aided cryptography +---------------------------------------- + +Although the need for the field has been well established, it faces many +challenges and has its own shortcomings. + +Only a few important protocols, such as Bluetooth, and TLS, are formally +verified, and it is less likely that verifying these protocols uncovers +serious flaws. This is because they are subject to extensive testing and +attacks. Whereas the protocols that aren’t used to support major +industrial applications generally aren’t subject to the same level of +scrutiny. They only receive limited manual testing, which leaves them +prone to errors. This is where formal verification can actually be used +to improve them significantly. The complexity of using the tools poses a +significant hurdle, and these protocols are left unverified. + +Additionally, a high barrier to entry to the field compounds the problem +of protocols being left unverified. This is because teams developing +protocols can’t spend the time and effort required to go through the +process of formally verifying them. + +In the end, the benefits of formal verification can seem marginal as the +tools themselves can have flaws, leading to the philosophical conundrum +of “Who will guard the guards themselves?” + +As a response to these challenges, the field offers the following +rebuttals: 1. The field is still new, and the tooling is undergoing +active development. Once the tools mature and are easier to use, we can +expect the industry to move in the direction of requiring formal +verification for protocols to be put into use. For instance, the +development of the 5G protocol happened in close `collaboration with the +formal verification community `__ +and is an encouraging move in the right direction 2. Even though the +tools might have flaws, the point to note here is that it would be +exceptionally hard for a mathematical proof to be wrong and also getting +past a formal verification check. So a flawed tool already provides +better security compared to a human-verified proof. The standard to beat +remains a highly specialised set of human eyes verifying a mathematical +proof. The argument of who guards the guards themselves already applies +to the current situation, and formal verification is, in fact, a +significant improvement. 3. The high barrier to entry remains a problem +with no simple solutions. However, this argument is akin to saying that +nuclear physics has a high barrier to entry. Although true, this +situation arises from the fact that these fields are highly specialised +and require years of training to reach a certain level of competence. + +All in all there is plenty of work left to do in the field. diff --git a/doc/tutorials/introduction-itp-program-logics/relational-hoare-logic.ec b/doc/tutorials/introduction-itp-program-logics/relational-hoare-logic.ec new file mode 100644 index 000000000..c28c94d2e --- /dev/null +++ b/doc/tutorials/introduction-itp-program-logics/relational-hoare-logic.ec @@ -0,0 +1,478 @@ +pragma Goals: printall. + +require import AllCore. + +(* +Let us work with Relational Hoare Logic and see how +to handle it in EasyCryt. As usual let us start simple and +define two functions that swap variables. +*) + +module Jumbled = { + proc swap1 (x y: int) : int*int = { + var z; + z <- x; + x <- y; + y <- z; + return (x,y); + } + + proc swap2 (x y: int) : int*int = { + var z; + z <- y; + y <- x; + x <- z; + return (x,y); + } +}. + +(* +A couple of things to observe in the definitions. +Firstly, they infact swap variables, however the order in which +they swap them is different. +Secondly, the return type of the functions is a tuple. +Notice the syntax of how it is done. (int*int) + +On paper we define hoare quadruples like so: +{P} C1 ~ C2 {Q} +While in EC, we use the following syntax to say the same: +equiv [C1 ~ C2 : P ==> Q] +As with Hoare triples in EC, we access the results of +both the programs using the "res" keyword. +Let us first prove that swap1 is equivalent to itself. +*) + +lemma swap1_equiv_swap1: +equiv [Jumbled.swap1 ~ Jumbled.swap1 : + x{1}=x{2} /\ y{1}=y{2} ==> res{1} = res{2}]. +(* +The numbers in the curly braces are identifiers +for programs. So res{1} should be read as result +from program 1, and res{2} is the result from program 2. +*) +proof. + proc. + simplify. + auto. +qed. + +(* +Let us now prove that both the swap functions are equivalent. +Notice the shorthand that we use for the conditions. +The eagle-eyed readers would've noticed this +shorthand in the goals pane in the previous exercise. +*) + +lemma swaps_equivalent: +equiv [Jumbled.swap1 ~ Jumbled.swap2 : ={x, y} ==> ={res} ]. +proof. +proc. + simplify. +(* +Now we have different programs, and the way we work with them is by +using similar tactics that we used for HL. +The only difference now is that we have to add identifiers +to the tactics for them to target specific sides and lines of code. +For instance, for the sake of a demonstration let us use the wp tactic +in an asymmetric way. +*) + wp 2 3. +(* +The tactic "wp n1 n2" will try to consume code +up to the n1-th line from the left program, +up to the n2-th line from the right program. +As you can see here, using "wp 2 3" +knocks off the 3rd line from the left program, +and leaves the right program untouched. +Try C-c C-u to undo and then C-c C-n +to redo and notice how things change. +*) + wp 2 2. + wp 0 1. + wp 0 0. + skip. + trivial. +qed. + +(* +Let us clean up the proof since we will never use +wp in the way we did above. In general we will rely +on EC to automatically work with whatever it can. +*) + +lemma swaps_equivalent2: +equiv [Jumbled.swap1 ~ Jumbled.swap2 : ={x, y} ==> ={res} ]. +proof. + proc. + wp. + skip. + simplify. + trivial. +qed. + +(* +Now that we see the complete proof relies only on +"wp, skip, and trivial" tactics, we can replace them with "auto". +Let us clean up the proof further with auto. +*) + +lemma swaps_equivalent_clean: +equiv [Jumbled.swap1 ~ Jumbled.swap2 : ={x, y} ==> ={res} ]. +proof. + proc. + auto. +qed. + +(* +Now let us take a small detour here and build on the the module types +that we briefly introduced in the exercise file of HL. +When working with cryptography, we generally don't know about the +inner workings of an adversary or an oracle. +In order to model these in EC we have the module types. +*) + +module type Adv = { + proc eavesdrop_one(): bool + proc eavesdrop_two(): bool +}. + +(* +By defining the module type Adv, we are instructing EC that any +concrete module which is of the Adv type has to, at the very least, +implement eavesdrop_one, and eavesdrop_two procedures. +What is interesting is that EC allows us to reason with the +abstract module types as well. For example let us define a module +which expects an Adv as input, and has a procedure +*) + +module Abstract_game(A:Adv) = { + proc one(): bool = { + var x; + x <@ A.eavesdrop_one(); + return x; + } +}. + +(* +At this stage, we don't know what A.eavesdrop_one does. +Neither does EC. However, we can still prove certain facts +related to it. Let us take a look at a simple reflexivity +example to understand how that works. +Notice that we have a new term glob A, in the precondition. +It stands for the global variable of the module A. +So in this next lemma we claim that, if the global state of the A +which is of type Adv is equal at the beginning of the program +then running the same program yields us the same result. +Quite a simple lemma, however the point to note here is +that we haven't defined what the function is. +*) + +lemma eavesdrop_reflex(A<:Adv): +equiv [Abstract_game(A).one ~ Abstract_game(A).one : + ={glob A} ==> res{1} = res{2} ]. +proof. + proc. + call (_: true). +(* +the call tactic does a few complicated things under the hood, +but at this point of time, what we can take away is that +if there is a call to the same abstract function on both +sides, call (_: true), knocks them both off. +*) + auto. +qed. + +(* +However, let us also define a concrete instantiation of Adv, +and work with it. A is quite basic, and either always returns +true or always returns false. +*) + +module A : Adv = { + proc eavesdrop_one() = { + return true; + } + + proc eavesdrop_two() = { + return false; + } +}. + +module Games = { + proc t(): bool = { var x; x <@ A.eavesdrop_one(); return x; } + proc f(): bool = { var x; x <@ A.eavesdrop_two(); return x; } +}. + +lemma games_quadruple (A<:Adv): + equiv [Games.t ~ Games.f : ={glob A} ==> res{1} <> res{2}]. +proof. + proc. + inline *. + wp. + simplify. + trivial. +(* auto can replace wp. simplify. trivial *) +qed. + +(* +The point of this detour is that, +when we work with cryptographic proofs we will +be dealing with adversaries both concrete and abstract ones. +With these exercises are warming up and building up those concepts. +*) + +(* +Before we move on to other things, let us take a look at +something non-trivial in RHL. +As we discussed earlier, one of the use cases of RHL +is to ensure that compiler optimisations preserve program behaviour. +Let us take a look at an example of this with a simple compiler +optimisation called "invariant hoisting". +Take a look at the programs defined below. +*) + +module Compiler = { + proc unoptimised (x y z: int) : int*int = { + while (y < z){ + y <- y + 1; + x <- z + 1; + } + return (x,y); + } + + (* + As you can observe, if the condition of the while loops holds + for even one iteration the variable x is set to z+1. + However every subsequent iteration of the loop doesn't change x, + since z is also constant. Hence to save on computation, + the compiler hoists that line out of the scope of the while loop. + Like so: + *) + + proc optimised (x y z: int) : int*int = { + if(y < z){ + x <- z + 1; + } + while (y < z){ + y <- y + 1; + } + return (x,y); + } +}. + +(* +Now let us try to prove the fact that +the behaviour of both the programs is equivalent. +At this point there can be two possibilities: +1. !(y < z) => (y = z) \/ (z < y): +In this case neither the while loop, nor the if condition are satisfied. +So both the programs effectively do nothing to the variables. + +or + +2. (y < z): +The while loop and the if condition executed at least once. +In this case the variables are modified. + +So in order to prove that the optimisation is indeed correct, we can +break our proof into these two cases, prove them independently +and then put them back together. + +An important point to note here is that, this proof took multiple attempts +and a fair amount of time to polish. It is important to understand +that this is a normal process, and takes practice to be able +to work with logic. Anyway, let us trudge on. + +Let us work with the first part in which the loops are never executed. +*) +lemma optimisation_correct_a: +equiv [Compiler.unoptimised ~ Compiler.optimised: + ={x, y ,z} /\ !(y{1} < z{1}) ==> ={res} ]. +proof. + proc. + simplify. +(* +At this point we introduce the seq tactic. +The seq tactic does the following: + + {P} A1; A2; A3 ~ B1; B2; B3 {Q} + ----------------------------------------------- seq 1 2: (R) + {P} A1; ~ B1; B2; {R} /\ {R} A2; A3; ~ B3; {Q} + +In general, the idea behind using the seq tactic is to +break the programs into manageable chunks, and deal with them +separately. +In our program, we have an if condition, that +we can effectively deal with and then work with the while +conditions. + +In this part of the proof, we know that the code inside the conditions +is not executed. Hence know that +R will simply have the variables unchanged +*) + seq 0 1: ( ={x, y ,z} /\ !(y{1} < z{1}) ). +(* Pause and see how the goal changed and now we have two goals to prove *) + auto. +(* +Now we know that neither of the while conditions +hold. So like we did earlier, we will use the rcondf to work with them. +rcondf breaks the goal into two, first part keeps everything before the while +intact. In our case, there is nothing so it adds a "skip", and a post-condition +which is the negation of the boolean expression of the while. +So in our case !(y < z). +When working with RHL, we have to use program identifiers, so that +EC can target the correct side and lines of code. +*) + rcondf {1} 1. + auto. + + (* Similarly, we work with the right program. *) + rcondf {2} 1. + auto. + + auto. +qed. + +(* +Now let us work with the second part of the proof which deals with +the part where the loops are executed. +The only complex part of this proof is the while loop. +So please pause before and after to ponder about the invariant. +*) + +lemma optimisation_correct_b: +equiv [Compiler.unoptimised ~ Compiler.optimised: + ={x, y ,z} /\ y{1} ={res} ]. +proof. + proc. +(* +As we did earlier, we will get rid of the if, +but this time we know that it will be executed, +hence we have x{2} = z{2} + 1 in the condition. +*) + seq 0 1: (={y,z} /\ y{1} ={res} ]. +proof. + proc*. +(* +Here we introduce "proc*", +proc* modifies the goal in a way similar to "proc", but +without losing the fact that the code is infact a procedure call. +With proc, we usually lose this connection to the procedures. +*) + +(* +Now we split on the boolean expression of the while loop. +Although we can't see it in the goal explicitly, we know this +is what we need to do since we put together two parts earlier. +*) + case (y{1} ={res} ]. +proof. +admit. +qed. + +(* +Now we define two more code blocks with similar deadcode, +except this time the variables y,z are not fixed like in +the previous code. +Prove that both these code blocks acheive the same result. +You could make progress by breaking the proof into +two parts, one in which the while loop is never +executed, and another in which it is executed at least once. +After that you could put them together. +*) +module Compiler3 = { + proc unoptimised (x y z: int) : int = { + while(z`__. +As usual, we start with some simple exercises. + +Basic Hoare quadruples +~~~~~~~~~~~~~~~~~~~~~~ + +We begin with two functions, ``swap1`` and ``swap2``, which swap +variables. However, the way they swap variables is slightly different, +and we’d like to establish the fact that they accomplish the same task. +We define ``swap1`` and ``swap2`` like so: + +:: + + module Jumbled = { + proc swap1 (x y: int) : int*int = { + var z; + z <- x; + x <- y; + y <- z; + return (x,y); + } + + proc swap2 (x y: int) : int*int = { + var z; + z <- y; + y <- x; + x <- z; + return (x,y); + } + }. + +In both functions, ``z`` is the temporary variable. In ``swap1``, ``x`` +is first stored in ``z``, while in ``swap2`` ``y`` is stored first. +However, both the functions accomplish the task of swapping variables. + +A Hoare quadruple, :math:`\{P\} \ C_1 \sim C_2 \ \{Q\}`, is expressed +in EasyCrypt with the statement ``equiv [C1 ~ C2 : P ==> Q].`` As with +Hoare triples, we access the results of both the programs using the +``res`` keyword. However, since we now have two programs, we need to add +identifiers to the variables that we use and also to the results to +convey the program that we are speaking about. For instance, to prove +that ``swap1`` is equivalent to itself, we would have the following +lemma. + +:: + + lemma swap1_equiv_swap1: + equiv [Jumbled.swap1 ~ Jumbled.swap1 : x{1}=x{2} /\ y{1}=y{2} ==> res{1} = res{2}]. + proof. + proc. + simplify. + auto. + qed. + +The proof for this lemma is quite straightforward and since there isn’t +much to reason ``auto`` is strong enough to complete the proof. Next we +prove that ``swap1`` is equivalent to ``swap2``. Now we have different +programs, and the way we work with them is by using similar tactics that +we used for HL. The only difference now is that we have to add +identifiers to the tactics for them to target specific sides and lines +of code. For instance, for the sake of a demonstration, we use the +``wp`` in an asymmetric way. + +``wp n1 n2`` will try to consume code up to the +``n1``\ :math:`^\textsf{th}` line from the left program, up to the +``n2``\ :math:`^{\textsf{th}}` line from the right program and will +modify the postconditions depending on the instructions that have been +consumed. The logic is similar to what we saw in HL. + +:: + + lemma swaps_equivalent: + equiv [Jumbled.swap1 ~ Jumbled.swap2 : ={x, y} ==> ={res}]. + proof. + proc. + simplify. + wp 2 3. + wp 2 2. + wp 0 1. + wp 0 0. + skip. + trivial. + qed. + +Since we will never really use ``wp`` the way we did above, we can +replace the large block of different calls to ``wp n1 n2.`` with just +``wp`` and EasyCrypt accomplishes the same automatically. Further, we +also notice that the proof only uses ``wp, skip`` and ``trivial`` +tactics, so we can use ``auto`` instead. This gives us a fairly trivial +proof for the lemma of the swap functions being equivalent. + +:: + + lemma swaps_equivalent_clean: + equiv [Jumbled.swap1 ~ Jumbled.swap2 : ={x, y} ==> ={res}]. + proof. + proc. + auto. + qed. + +Abstract modules and adversaries +-------------------------------- + +Now let us take a small detour here and build on the module types that +we saw earlier when modelling the abstract IND-RoR game. When working +with cryptography, we generally don’t know about the inner workings of +an adversary or an oracle. In order to model these in EasyCrypt, we have +the module types. + +:: + + module type Adv = { + proc eavesdrop_one(): bool + proc eavesdrop_two(): bool + }. + +By defining the module type Adv, we are instructing EasyCrypt that any +concrete module which is of the ``Adv`` type has to, at the very least, +implement ``eavesdrop_one`` and ``eavesdrop_two`` procedures. What is +interesting is that EasyCrypt allows us to reason with the abstract +module types as well. For example, let us define a module which expects +an Adv as input. + +:: + + module Abstract_game(A:Adv) = { + proc one(): bool = { + var x; + x <@ A.eavesdrop_one(); + return x; + } + }. + +At this stage, we don’t know what ``A.eavesdrop_one`` does and neither +does EasyCrypt. However, we can still prove certain facts related to it. +Just for a demonstration, we provide a reflexivity example. + +Notice that we have a new term ``glob A`` in the precondition. It stands +for the global variables of the module ``A``. So in this following +lemma, we claim that if the global state of the ``A`` which is of type +``Adv`` is equal at the beginning of the program, then running the same +program yields us the same result. Quite a simple lemma, however the +point to note here is that we haven’t defined what the procedure is. + +:: + + lemma eavesdrop_reflex(A<:Adv): + equiv [Abstract_game(A).one ~ Abstract_game(A).one : + ={glob A} ==> res{1} = res{2} ]. + proof. + proc. + call (_: true). + auto. + qed. + +``call`` does a few complicated things under the hood, but at this point +of time, we can think that ``call (_: true)``, knocks off a call to the +same abstract function on both sides. + +Let us also define a concrete instantiation of ``Adv`` called ``A`` and +work with it. Module ``A`` is quite basic, and either always returns +true or always returns false. + +:: + + module A : Adv = { + proc eavesdrop_one() = { + return true; + } + + proc eavesdrop_two() = { + return false; + } + }. + + module Games = { + proc t(): bool = + { var x; x <- A.eavesdrop_one(); return x; } + proc f(): bool = + { var x; x <- A.eavesdrop_two(); return x; } + }. + +Now we can reason with these concrete instances with the tactics that +we’ve seen so far. For instance, since we know that ``Games.t`` and +``Games.f`` return different values, we can make a claim like the +following and prove it. In this proof, we use ``inline *``, which simply +fills in (or “inlines”) the concrete code of ``Games.t`` and +``Games.f``. The ``*`` in the tactic is a selector to select everything +that can be inlined. + +:: + + lemma games_quadruple (A<:Adv): equiv [Games.t ~ Games.f : + ={glob A} ==> res{1} <> res{2} ]. + proof. + proc. + inline *. + wp. + simplify. + trivial. + qed. + +The key takeaway of this detour is that when we work with cryptographic +proofs, we will be dealing with both concrete and abstract adversaries. +We can now go back to working with some more challenging Hoare +quadruples. + +Advanced Hoare quadruples +~~~~~~~~~~~~~~~~~~~~~~~~~ + +As we discussed earlier, one of the use cases of RHL is to ensure that +compiler optimisations preserve program behaviour. Let us take a look at +an example of this with a simple compiler optimisation called *invariant +hoisting*. Take a look at the programs defined below. + +:: + + module Compiler = { + proc unoptimised (x y z: int) : int*int = { + while (y < z){ + y <- y + 1; + x <- z + 1; + } + return (x,y); + } + proc optimised (x y z: int) : int*int = { + if(y < z){ + x <- z + 1; + } + while (y < z){ + y <- y + 1; + } + return (x,y); + } + }. + +As you can observe, if the condition of the ``while`` loop in +``unoptimised`` holds for even one iteration the ``x`` is set to +``z+1``. However, the subsequent iterations of the loop don’t change +``x``. Hence to save on computation, the compiler hoists that line out +of the scope of the ``while`` loop, giving us ``optimised``. + +Now let us try to prove the fact that the behaviour of both the programs +is equivalent. At this point, there can be two possibilities: 1. +``!(y < z)``: In this case, neither the ``while`` loop nor the ``if`` +condition is satisfied. So, both the programs effectively do nothing to +the variables. 2. ``(y < z)}``: The ``while`` loop and the ``if`` +condition are executed at least once. In this case, the variables are +modified. + +So to prove that the optimisation is correct, we can break our proof +into these two cases, work on them independently and then put them back +together. + +Let us work with the first part in which the loops are never executed. +In this proof, we will use the ``seq`` tactic. It does the following: + +.. math:: \dfrac{\{P\} A1; \sim B1; B2; \{R\} \ \ \{R\} A2; A3; \sim B3; \{Q\}}{\{P\} A1; A2; A3 \sim B1; B2; B3 \{Q\}}\ seq \ 1 \ 2:(R) + +The idea behind using the ``seq`` is to break the programs into +manageable chunks and deal with them separately. In our program, we have +an ``if`` condition in ``optimised`` that we can deal with and then work +with the ``while`` conditions. In this part of the proof, we know that +the code inside the conditions is not executed. Hence, we know that we +can pass the precondition itself as :math:`R`. With this we can knock +off the ``if`` from ``optimised`` using ``seq``. Then we use ``rcondf`` +to deal with the ``while`` loops since we know that they won’t be +executed. + +:: + + lemma optimisation_correct_a: + equiv [Compiler.unoptimised ~ Compiler.optimised: + ={x, y ,z} /\ (z{1}=y{1} \/ z{1} ={res} ]. + proof. + proc. + simplify. + + (* Dealing with the if on the right *) + seq 0 1: ( ={x, y ,z} /\ (z{1}=y{1} \/ z{1} ={res} ]. + proof. + proc. + (* Dealing with the if condition in optimised *) + seq 0 1: (={y,z} /\ y{1} ={res} ]. + proof. + + proc*. + + (* Branching on the boolean *) + case (y{1}