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 noncebased 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 NonceBased Encryption Schemes, PenandPaper
For the security property, we consider INDistinguishability from RANDOM ciphertexts under NonceRespecting ChosenPlaintext Attacks (IND$NRCPA): An adversary with access to a chosenplaintext 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 noncebased) 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, $\mathcal{O}^{CPA\textrm{}real}_{\Sigma}$ (which is defined with respect to an abstract symmetric noncebased encryption scheme $\Sigma$, instantiable by any concrete such scheme) and $\mathcal{O}^{CPA\textrm{}ideal}$.
$\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 noncebased) encryption scheme $\Sigma$ against a noncerespecting chosenplaintext distinguisher $\mathcal{D}$—i.e., a (potentially probabilistic) algorithm $\mathcal{D}$ with the appropriate interface—as the (absolute) difference between the likelihood of (1) $\mathcal{D}$ outputting $\texttt{true}$ when given access to (the $\mathsf{enc}$ procedure of) $\mathcal{O}^{CPA\textrm{}real}_{\Sigma}$ and (2) $\mathcal{D}$ outputting $\texttt{true}$ when given access to (the $\mathsf{enc}$ procedure of) $\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 $\mathcal{D}$ in distinguishing $\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 $\mathcal{D}$ against IND$NRCPA of $\Sigma$. Mathematically, this advantage is expressed as follows.
$\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 $\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 $\mathsf{enc}$ function of the oracle, and directly outputs the return value received from the distinguisher.
$\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, $\mathsf{Adv}^{\mathrm{IND\$\textrm{}NRCPA}}_{\Sigma}(\mathcal{D})$ matches the intuitive description of insecurity we gave earlier. Namely, because $\mathsf{Exp}^{\mathrm{IND\$\textrm{}NRCPA}}_{\mathcal{D}, \mathcal{O}^{CPA\textrm{}real}_{\Sigma}}$ and $\mathsf{Exp}^{\mathrm{IND\$\textrm{}NRCPA}}_{\mathcal{D}, \mathcal{O}^{CPA\textrm{}ideal}}$ merely differ in the oracle they provide to $\mathcal{D}$, a difference in probability of $\mathcal{D}$ outputting a certain truth value (arbitrarily chosen to be 1, or $\texttt{true}$, here) between the experiments must be a consequence of distinguishing the oracles somehow. Certainly, this is precisely what $\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 noncebased encryption) scheme $\Sigma$ is IND$NRCPA secure if, for any noncerespecting chosenplaintext adversary $\mathcal{D}$, $\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.
IND$NRCPA Security for Symmetric NonceBased Encryption Schemes, EasyCrypt
To formalize the abovediscussed 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 penandpaper definition of the oracles, we can see that they implement two algorithms: $\mathsf{init()}$ and $\mathsf{enc}(n, m)$, where $n$ is a nonce, $m$ is a plaintext, and $\mathsf{enc}(n, m)$ outputs either a valid ciphertext or an indication of failure ($\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
builtin 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 alreadyexisting 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 $\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,
$\mathcal{O}^{CPA\textrm{}real}_{\Sigma}$ is defined with respect to some other entity $\Sigma$ from a certain
class; in this case, this is the class of symmetric noncebased encryption schemes.
In EasyCrypt, we formalize this using a socalled functor or higherorder 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 previouslydefined NBEncScheme
module type. So, we can formalize $\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 noncebased 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 welldefined 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
).
Looking at the actual code of O_NRCPA_real
, we can see that it is a relatively straightforward
translation from the penandpaper definition of which the novel concepts may seem rather
selfexplanatory. Regardless, we briefly go over these concepts for clarity and completeness.
list
is a type constructor (defined inList.ec
) that can be used to construct the type of lists over a certain type. In other words, for any typet
,t list
is the type of lists containing elements of typet
.[]
is a value (defined inList.ec
) that denotes the empty list.\in
is an abbreviation (defined inList.ec
) that can be used an infix operator, and checks whether the lefthand side operand (of some type, sayt
) is an element of the righthand side operand (of typet list
).::
is an infix operator (defined inList.ec
) that prepends the lefthand side operand (of some type, sayt
) to the righthand side operand (of typet 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 $\mathcal{O}^{CPA\textrm{}real}_{\Sigma}$, we continue with the formalization of $\mathcal{O}^{CPA\textrm{}ideal}$. Certainly, as one would expect from the penandpaper 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 nonzero 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 nonzero 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 $1 / \left \mathcal{C} \right$
(where $\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 $\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 noncebased) encryption scheme $\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), socalled functor types or higherorder 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 copypaste;
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 penandpaper definition. Otherwise, the formalization, provided in the
following snippet, is a verbatim translation of the penandpaper 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 $\mathcal{D}$ against IND$NRCPA of a symmetric noncebased encryption scheme $\Sigma$. Recall that the penandpaper definition of this advantage is the following.
$\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.
"NonceRespecting" PseudoRandom Function Family Property, PenandPaper
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 $\mathcal{E}$ on the (assumed) "NonceRespecting" PseudoRandom Function family (NRPRF) property^{1} of the function family used to map nonces to plaintexts (i.e., $\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/nonrepeating inputs.
More formally, consider the two oracles given below, $\mathcal{O}^{PRF\textrm{}real}$ and $\mathcal{O}^{PRF\textrm{}ideal}$.^{2}
$\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, $\mathcal{O}^{PRF\textrm{}real}$ and $\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 $\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 noncerespecting pseudorandom function distinguisher $\mathcal{D}$ against $\left(f_{k} : \mathcal{N} \rightarrow \mathcal{P}\right)_{k \in \mathcal{K}}$ as the following (absolute) difference.
$\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, $\mathsf{Exp}^{\mathrm{NRPRF}}_{\mathcal{D}, \mathcal{O}}$ refers to the experiment defined below.
$\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 $\left(f_{k} : \mathcal{N} \rightarrow \mathcal{P}\right)_{k \in \mathcal{K}}$ is a NRPRF if, for any noncerespecting pseudorandom function family adversary $\mathcal{D}$, $\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 paperbased security proof before diving into the EasyCrypt formalization, you can read further on the proving security part.
"NonceRespecting" PseudoRandom 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 $\mathcal{O}^{PRF\textrm{}real}$ and $\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 penandpaper 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 penandpaper 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;
}
}.
Footnotes

NRPRF is not a conventional property; rather, it is a variant of the more customary PseudoRandom Function family (PRF) property. For educational purposes, we have specifically devised this variant to simplify the current proof. ↩

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) noncerespecting 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 $\left(f_{k} : \mathcal{N} \rightarrow \mathcal{P}\right)_{k \in \mathcal{K}}$. ↩