Formalizing the Hidden Number Problem in Isabelle/HOL

The closest vector problem is the problem of finding a vector $v_{\text{min}}$ in a given lattice $L$ that is closest to a target vector $u$ – that is, finding $v_{\text{min}}$ witnessing $D≔\min \{\Vert v-u\Vert :v\in L\}$. Although the task of finding $v_{\text{min}}$ is NP-complete [24], it is possible to find a vector that is not too much further from $u$ than $v_{\text{min}}$ in polynomial time. In particular, Babai’s nearest plane algorithm finds a vector $\widehat{v}\in L\subseteq {ℝ}^n$ where $\Vert \widehat{v}-u\Vert \le \sqrt{n}{(\sqrt{\delta })}^{d}D$, where $\delta \ge 4/3$ is an adjustable approximation factor and $d$ is the dimension of the lattice $L$.

The most general form of Babai’s algorithm allows a target vector $u\in {ℝ}^n$ and a lattice $L\subseteq {ℝ}^n$ spanned by $d$ vectors (with $d\le n$). However, the algorithm requires obtaining a “nearly orthogonal” basis of $L$ by applying the LLL basis reduction algorithm [28], which in Isabelle/HOL has been formalized for lattices $L\subseteq {\mathbb{Z}}^n$ [12, 43, 18]. Since we build on this existing LLL formalization, our formalization of Babai’s algorithm also only accepts lattices in ${\mathbb{Z}}^n$. We can apply our algorithm to a lattice ${\mathbb{Q}}^n$ by first scaling it to a lattice in ${\mathbb{Z}}^n$ (a technique we apply later on), but this workaround is not available for lattices in ${ℝ}^n$. The target vector $u$ may be drawn from ${\mathbb{Q}}^n$. We also focus on the $n=d$ case, so our formal algorithm only accepts lattices where $n=d$ (which is sufficient for our purposes in the hidden number problem).

We follow a set of lecture notes by Stephens-Davidowitz [42] which addresses the relevant $n=d$ case. The informal proof, worded geometrically, references the hyperplanes defined by integer multiples of the lattice basis vectors. Reformulated algebraically, this is an argument about the coefficients of lattice vectors as linear combinations of the basis vectors. In the formal proof, we obtain these coefficients by inverting the matrix corresponding to the lattice basis vectors, which is only possible if said matrix is square, i.e., when $n=d$. While we explored ways of lifting the $n=d$ special case to a more general result for $n\le d$, we did not succeed;³³3We considered embedding a lattice with into ${ℝ}^d$, or padding out such a lattice with additional but superfluous basis vectors, but neither workaround succeeded. as the matrix and its inverse are involved in many of the proof details, we expect that generalizing the result may require changes to large portions of the proof. Hence, specializing to the $n=d$ case appears to present a non-trivial limitation. We discuss the details of our proof strategy and the formalized result in Section 4.1.

Let $p$ be a large prime. Intuitively, the HNP, introduced by Boneh and Venkatesan [11], is concerned with designing an adversary capable of finding a fixed “hidden number” $\alpha \in {(\mathbb{Z}/p\mathbb{Z})}^{\times }$ with high probability (where ${(\mathbb{Z}/p\mathbb{Z})}^{\times }$ is the set $\{1,\mathrm{\dots },p-1\}$ viewed as a group under multiplication modulo $p$), given access to an oracle which (roughly speaking) leaks the first $k$ bits of $(\alpha \cdot t)modp$ for randomly sampled values of $t$ (and a fixed choice of $k$).

To make this precise, Boneh and Venkatesan introduce the ${\mathrm{MSB}}_k$ operator, where they initially present ${\mathrm{MSB}}_k(x)$ as “the integer $t$ such that ” [11]. This can be thought of as giving approximately $k$ bits of information about $x$. However, this is not quite the ${\mathrm{MSB}}_k$ function they ultimately use – they assume that ${\mathrm{MSB}}_k$ is slightly modified from the previous description to satisfy (though they do not concretely describe the modification). The rest of the theorem statement and proof relies only on this bound and not on the precise definition of ${\mathrm{MSB}}_k$. In fact, the proof turns out to only require a bound of $p/2^k$. In our formalization, we let the ${\mathrm{MSB}}_k$ function be arbitrary, subject to this assumption, but we do subsequently define two concrete ${\mathrm{MSB}}_k$ functions (a non-computational definition modeled on the original (incomplete) description given by Boneh and Venkatesan, and a more intuitive computational definition) and prove that they satisfy this assumption (see Section 4.2).

With ${\mathrm{MSB}}_k$ fixed, the adversary receives a sequence of tuples $((t_1,𝒪(t_1)),\mathrm{\dots },(t_d,𝒪(t_d)))$, where $𝒪$ is an oracle defined by $𝒪(x)={\mathrm{MSB}}_k((x\cdot \alpha )modp)$ and the $t_i$’s are uniformly and independently sampled from ${(\mathbb{Z}/p\mathbb{Z})}^{\times }$. Given this input, the adversary then tries to produce the original hidden number $\alpha$. A successful adversary implies that the problem of finding $\alpha$ can be reduced to the problem of computing the oracle. In the context of Diffie–Hellman, a successful adversary means that if the secret key is difficult to recover, then so is partial information about the secret key.

The original proof by Boneh and Venkatesan additionally assumes that $n$ (and hence $p$) is “sufficiently large” – for our formalization, we explicitly assume $n>961$, which we derive from both our particular bound for Babai’s algorithm (discussed later in Section 4.1) and the inequalities used in the proof of Theorem 1. As $n$ (abstractly) represents the number of bits of a secret key, this lower bound does not introduce any practical restrictions – modern encryption schemes use secrets much longer than $961$ bits.

Note that while Theorem 1 establishes that the adversary has polynomial time complexity, we focus on the correctness of the adversary and do not address complexity. As the existing LLL formalization includes a formal complexity analysis [12, 43, 18], we believe that extending their approach to a formal complexity analysis of Babai’s algorithm and the HNP adversary is very doable. This is because Babai’s algorithm is a rather direct application of LLL, and the HNP adversary we will present (Section 3.1) is a direct application of Babai’s algorithm. Nevertheless, we see verifying complexity as interesting future work, as formal verification has historically revealed problems in informal complexity analysis [20].

For the convenience of the reader, we collect some of our frequently-used notation and abbreviations in Table 1 (though this notation will be explained as it is introduced throughout Section 3). We attempt to make our notation consistent with the original paper, though we introduce floor and ceiling operators where appropriate.⁴⁴4The original paper sometimes omits details like floors and ceilings; these details are naturally explicated in the course of formalization, where all type information is explicit.

Boneh and Venkatesan do not explicitly define the adversary, but its definition is inherent in their proof [11]. Our formalization blueprint begins by defining an explicit adversary, $𝒜$. Suppose $t_1,\mathrm{\dots },t_d\in {(\mathbb{Z}/p\mathbb{Z})}^{\times }$ are sampled uniformly and independently. The adversary $𝒜$ receives the list of tuples $((t_1,𝒪(t_1)),\mathrm{\dots },(t_d,𝒪(t_d)))$, defines the vector $u≔(𝒪(t_1),\mathrm{\dots },𝒪(t_d),0)$, and applies Babai’s nearest plane algorithm to $u$ and the $(d+1)$-dimensional lattice $L$ generated by the rows of the matrix

Because the formalized LLL algorithm (and hence our formalization of Babai’s algorithm) operates on lattices of integral vectors, we cannot work directly with the lattice as described above. Instead, we scale this lattice up by $p$, resulting in a lattice $\widehat{L}$ which is a subset of ${\mathbb{Z}}^{d+1}$. This introduces some minor casting nuisances (between rat and int), and also introduces a factor of $p$ in the final distance bound provided by our formal Babai’s algorithm, but does not substantially change the proof approach. In fact, in the proof, the scaling is almost an afterthought – almost the entire proof works with the original lattice $L$, and the scaling only arises in the formal “glue” between the adversary implementation and the final proof steps.

So, from Babai’s algorithm, $𝒜$ now possesses a vector $\widehat{v}\in \widehat{L}$ which is close⁵⁵5We discuss exact bounds in Section 4.1. to $p\cdot u$ (which is $u$ scaled by $p$). Let $\widehat{\beta }\in \mathbb{Z}$ be the last coordinate of $\widehat{v}$. Now, if $\widehat{\beta }\equiv \alpha (modp)$ (the “good” case), then $𝒜$ can extract $\alpha$ from $\widehat{v}$ by computing $\alpha =(\widehat{\beta }modp)$. Foreshadowing, we note that the proof of Theorem 1 ultimately relies on showing that ${\mathrm{Pr}}_{t_i}[\widehat{\beta }\equiv \alpha (modp)]\ge 1/2$, i.e. the good case occurs with probability at least $1/2$.

We use Isabelle’s locale system [2] to fix ambient variables throughout our formalization (so they do not have to be redefined in every lemma statement). To start, we define our adversary within a locale that fixes the ambient variables $p$ and $d$.⁶⁶6It is convenient to use a locale to fix these variables, but since we place no assumptions on $p$ and $d$ within this locale (nor do we prove any lemmas; the assumptions and lemmas appear later in a different locale for the main theorem), we could equivalently pass $p$ and $d$ as arguments into our definition of $𝒜$, and thread them through all helper functions.

This locale contains only what is necessary for the definition of the adversary; in particular, it does not contain $\alpha$. Within this locale, our adversary $𝒜$ is defined as follows:

When the adversary is used in the main theorem, the input variable pairs is assigned to the list of tuples $((t_1,𝒪(t_1)),\mathrm{\dots },(t_d,𝒪(t_d)))$. With this instantiation of pairs, $𝒜$_vec first calls map fst pairs to extract the list $(t_1,\mathrm{\dots },t_d)$. This list is passed to the function int_gen_basis, which constructs a basis for the lattice $\widehat{L}$. Then, $𝒜$_vec computes the vector $p\cdot u$, using the helper function scaled_uvec_from_pairs (note, map_vec rat_of_int is applied merely to convert types from int vec to rat vec by element-wise conversion). Next, $𝒜$_vec applies Babai’s algorithm (with an approximation factor of $c=4/3$) to yield a vector $\widehat{v}$ that is close to $p\cdot u$. Finally, the adversary $𝒜$ returns the last component of $\widehat{v}$ modulo $p$, which is likely $\alpha$. A visualization of the adversary is given in Figure 1.

Having defined the adversary $𝒜$, we must now show that it satisfies the statement of Theorem 1. We discuss the proof here in backwards fashion (starting from the main theorem and subsequently presenting helper lemmas). Let $t_1,\mathrm{\dots },t_d$ be sampled uniformly and independently from ${(\mathbb{Z}/p\mathbb{Z})}^{\times }$, and let $L$ and $u$ be the associated lattice and vector as in the definition of $𝒜$. As noted in Section 3.1, it suffices to show that ${\mathrm{Pr}}_{t_i}[\widehat{\beta }\equiv \alpha (modp)]\ge 1/2$, where $\widehat{\beta }$ is as in the definition of $𝒜$. To show this, Boneh and Venkatesan prove a so-called “uniqueness theorem”, which intuitively says that with probability at least $1/2$, every vector with shape $(\mathrm{\dots },\frac{\beta }{p})\in L$ (with $\beta \in \mathbb{Z}$) that is close to $u$ satisfies $\beta \equiv \alpha (modp)$. This lemma may seem slightly surprising, since it is technically stronger than what we need, but its more general statement is a hammer that allows us to reason only about the shape of $\widehat{v}$ and its closeness to $u$, and not about the details of Babai’s algorithm itself. The uniqueness theorem is stated precisely as follows [11].

Note that the probability in this theorem is considered over the uniformly, independently sampled $t_i$’s (since $u$ and $L$ depend on the $t_i$’s). Also note that it follows directly from the definition of $L$ that every $v\in L$ has last coordinate of the form $\beta /p$ for some $\beta \in \mathbb{Z}$; the non-trivial portion of Theorem 2 is the $\beta \equiv \alpha (modp)$ claim.

Theorem 2 thus reduces the proof of Theorem 1 to simply showing that the $\widehat{v}$ computed by Babai’s algorithm in $𝒜$ satisfies (note the scaling by $p$), a task which amounts to arithmetic manipulation of the bound given by Babai’s algorithm. The bulk of our work is in formalizing Theorem 2, so we now turn to its informal proof blueprint.

We found that the original proof of Theorem 2 given by Boneh and Venkatesan was not very well-suited to formalization. For example, they do not provide many details in the steps involving probabilistic approximations, and they elide many arithmetic details; notably, they do not provide the explicit lower bound on $n$ that is required for the proof (their result is stated for “large enough $n$”; formalization requires an explicit lower bound), and they omit the detailed definition unfolding and manipulation required to derive certain probabilistic inequalities. In light of this, we reformulated Boneh and Venkatesan’s presentation to be more amenable to formalization. We now give the high-level structure of our proof approach, invoking the yet-to-be-stated Lemma 4, a key helper lemma which we subsequently discuss. For some abstraction, we introduce the following definition.

Theorem 2 is thus saying that, with probability at least $1/2$, every $v\in L$ is good. In our development, the lemma sampled_lattice_likely_good is the formalization of Theorem 2.

We state our top-level theorem within a locale. We begin with our hnp_arith locale, which fixes the ambient variables p, $\alpha$, n, k, and d along with the necessary assumptions on each. This locale contains basic technical lemmas about the algebraic relationships between the ambient variables required throughout the rest of the proof.⁹⁹9The lemmas include results like and $\mu +1\le k$.

We then introduce the hnp locale, which inherits from hnp_arith and hnp_adversary, and fixes the msb_k function along with its critical assumption.

Within this locale, we define $𝒪$ in terms of msb_k, as discussed in Section 2.2.

We can now define game, which uses familiar do notation provided by the Isabelle/HOL standard libraries to formally capture the cryptographic “game” that our adversary must win with probability at least $1/2$.

Intuitively, one can think of game as a probabilistic procedure: using the probability mass function (pmf) monad,¹⁰¹⁰10Often called the Giry monad. game takes in an adversary ${𝒜}^{\prime }$, uses the replicate_pmf function¹¹¹¹11All of pmf, replicate_pmf, and return_pmf are defined in the Isabelle/HOL standard libraries; see Section 4.4 for more discussion on pmf and replicate_pmf. to uniformly sample a list $(t_1,\mathrm{\dots },t_d)$ from ${\{1,\mathrm{\dots },p-1\}}^d$, passes $((t_1,𝒪(t_1)),\mathrm{\dots },(t_d,𝒪(t_d)))$ into the adversary ${𝒜}^{\prime }$, and finally returns True if ${𝒜}^{\prime }$ outputs $\alpha$, and False otherwise. More formally, one can understand game as taking in an adversary ${𝒜}^{\prime }$ and returning a probability mass function on the set $\{\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">True</em>},\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">False</em>}\}$, where the probability given to True is the probability that ${𝒜}^{\prime }((t_1,𝒪(t_1)),\mathrm{\dots },(t_d,𝒪(t_d)))=\alpha$. Thus, our top-level theorem is

where $𝒜$ is the adversary defined in Section 3.1. This asserts that our explicit adversary $𝒜$ wins game with probability at least $1/2$ (that is, $𝒜((t_1,𝒪(t_1)),\mathrm{\dots },(t_d,𝒪(t_d)))=\alpha$ for at least half of all lists $(t_1,\mathrm{\dots },t_d)\in {\{1,\mathrm{\dots },p-1\}}^d$).

We first give some details of our proof approach to formalizing Babai’s nearest plane algorithm, followed by some discussion of the bounds we obtain.

We start with some intuition for how our proof of Babai’s nearest plane algorithm proceeds. Let $ℬ=\{b_1,\mathrm{\dots },b_d\}$ be a basis of the lattice $L$ that is LLL-reduced with parameter $\delta \ge 4/3$, let $\widetilde{ℬ}=\{{\tilde{b}}_1,\mathrm{\dots },{\tilde{b}}_d\}$ be the orthogonalization of $ℬ$ computed by the Gram–Schmidt algorithm, and let $\widehat{v}$ be the output of Babai’s Algorithm. As $\widetilde{ℬ}$ is orthogonal, ${\Vert \widehat{v}-u\Vert }^2=\sum _{i=1}^d\frac{{⟨(\widehat{v}-u),{\tilde{b}}_i⟩}^2}{{\Vert {\tilde{b}}_i\Vert }^2}$. Therefore, we may optimize ${\Vert \widehat{v}-u\Vert }^2$ by optimizing each of the terms $\frac{{⟨(\widehat{v}-u),{\tilde{b}}_i⟩}^2}{{\Vert {\tilde{b}}_i\Vert }^2}$.

Babai’s algorithm begins with ${\widehat{v}}_0≔\mathrm{𝟎}$ and, at step $i$, defines ${\widehat{v}}_i≔{\widehat{v}}_{i-1}+z_i{b}_{n-i+1}$, where $z_i\in \mathbb{Z}$ minimizes $⟨({\widehat{v}}_i-u),{\tilde{b}}_{n-i+1}⟩$. In particular, we can show that at step $i$, $⟨({\widehat{v}}_i-u),{\tilde{b}}_{n-i+1}⟩$ can be brought below $\frac{1}{2}{\Vert {\tilde{b}}_{n-i+1}\Vert }^2$ in general and becomes $0$ if (as long as $ℬ$ is LLL-reduced with parameter $\delta$). Moreover, by nature of the Gram–Schmidt orthogonalization, the change-of-basis matrix from $ℬ$ to $\widetilde{ℬ}$ is upper-triangular, so $⟨({\widehat{v}}_i-u),{\tilde{b}}_{n-i+1}⟩=⟨(\widehat{v}-u),{\tilde{b}}_{n-i+1}⟩$, so the bound on each $⟨({\widehat{v}}_i-u),{\tilde{b}}_{n-i+1}⟩$ carries through to the final output. Thus, we obtain

which yields $\Vert \widehat{v}-u\Vert \le \sqrt{d}{\delta }^{d/2}D$ as claimed. Additionally, because the algorithm begins with the lattice vector ${\widehat{v}}_0=\mathrm{𝟎}\in L$, and in each step only adds integer multiples of vectors from $ℬ$ (the original basis of $L$), the final output vector $\widehat{v}$ must be a lattice vector, as needed.

This is an algebraic analog of a geometric proof in lecture notes by Stephens-Davidowitz [42]. In our formalization, we make one modification involving the definition of $D≔\min \{\Vert v-u\Vert :v\in L\}$. It is intuitively clear that this $D$ is well-defined (in particular, since $L\subseteq {\mathbb{Z}}^d$). One may try to formalize the well-definedness of $D$ by picking a ball $B$ centered at $u$ such that $L\cap B\ne \mathrm{\varnothing }$, arguing that $\min \{\Vert v-u\Vert :v\in L\}=\min \{\Vert v-u\Vert :v\in L\cap B\}$ if the RHS exists, and finally showing that the RHS exists by showing that $L\cap B$ is finite. However, this approach involves some geometric argumentation, which tends to be cumbersome to formalize. We instead sought a more algebraic path, starting with the alternative definition $D≔inf\{\parallel v-u\parallel :v\in L\}$, making well-definedness of $D$ immediate. With this new definition of $D$, we cannot obtain a vector $v_{\text{min}}$ witnessing $\Vert v_{\text{min}}-u\Vert =D$ (which is done in the standard proof approach), but we can obtain a vector $v_{ϵ}$ such that $\Vert v_{ϵ}-u\Vert \le (1+ϵ)D$, for arbitrary $ϵ>0$. This $(1+ϵ)$ factor carries through the remainder of the proof, yielding $\Vert \widehat{v}-u\Vert \le (1+ϵ)\sqrt{n}{(\sqrt{\delta })}^{d}D$ for all $ϵ>0$, which implies $\Vert \widehat{v}-u\Vert \le \sqrt{n}{(\sqrt{\delta })}^{d}D$ as needed.

So, a key proof challenge is to obtain the $v_{ϵ}$ for arbitrary $ϵ>0$. If $D\ne 0$, then , meaning $v_{ϵ}$ is yielded immediately by the definition of the infimum. However, if $D=0$, then we must obtain $v_{ϵ}$ where $\Vert v_{ϵ}-u\Vert =0$ (that is, $v_{ϵ}=u$); this is a special case of the fact we had hoped to avoid formalizing, but the condition $D=0$ enables the following argument that is much simpler than in the general case: If $D=0$ but $v_{ϵ}$ does not exist, then we may obtain distinct vectors in $L$ that are arbitrarily close to $u$. This means that they are very close to each other, and hence their difference is a very short nonzero vector in $L$. Applying the lower bound on the sizes of short nonzero vectors in $L$ from the formalized LLL algorithm [18] yields a contradiction, so $v_{ϵ}$ must exist.

Intuitively, the $D=0$ condition implies that if two vectors are both approximately $D$ away from $u$, then those vectors are themselves close together (by the triangle inequality). In the $D>0$ case, one can space out many far-apart vectors approximately on a sphere of radius $D$ centered at $u$; bounding how many such far-apart vectors one can fit is tricky.

As Boneh and Venkatesan note [11], Babai’s algorithm is commonly presented with a final bound of $\Vert \widehat{v}-u\Vert \le 2^{d/2}D$. They further note that with proper adjustment of constants in the LLL algorithm, the bound can be reduced to $2^{d/4.6}D$. Boneh and Venkatesan use a bound of $2^{d/4}D$ in their proof; notably, $2^{d/2}D$ is not strong enough for their proof. Our final bound lies between these two bounds: we prove that $\Vert \widehat{v}-u\Vert \le \sqrt{d}{(4/3)}^{d/2}D$. This is not as strong as the bound of $2^{d/4}D$, but is stronger than $2^{d/2}D$, and (in particular) is strong enough for the proof of Theorem 1.

As our top-level result is stated for an arbitrary ${\mathrm{MSB}}_k$ function satisfying , we formalize two concrete ${\mathrm{MSB}}_k$ functions.

We first formalize the ${\mathrm{MSB}}_k$ function given by Boneh and Venkatesan, namely that ${\mathrm{MSB}}_k(x)$ is the unique $t$ such that . However, this definition is inconsistent with the desired property , and the details of reconciling this are omitted in the source material. To attain this, we set ${\mathrm{MSB}}_k(x)=\lfloor t\cdot p/2^k\rfloor -1$, where $t$ is as before. Note, this modification still does not achieve the bound as presented in the source material [11], but the $p/2^k$ bound suffices for the proof. As this definition is not stated in a computable way (though one could formulate an equivalent computable definition), a literal translation requires Isabelle/HOL’s THE operator, which intuitively represents the unique object satisfying a particular property.¹²¹²12If t $\equiv$ (THE x. P x), then we can prove P t by showing that there exists a unique x satisfying P x. If no such x exists, then the value of t is unspecified, meaning one can only prove things about t that hold for all values of the same type. We provide the following literal translation, named msb_p to emphasize its direct dependence on p.

We prove that msb_p is well-defined by showing that there is indeed a unique $t$ satisfying .

As Boneh and Venkatesan’s definition of ${\mathrm{MSB}}_k$ is non-computational and perhaps slightly esoteric, we formalize the following straightforward (computational) definition, msb_kp1, which literally computes the $k+1$ most significant bits of its input, using the div operation for integer division (note that the $+1$ is required to achieve the desired bound).

This is essentially an arithmetic description of a right-shift of $x$ followed by a left-shift of $x$, both by $n-(k+1)$ bits, where we assume $x$ is expressed in $n$ bits. While the information we desire is captured just by the right shift, the left-shift is necessary to satisfy the desired bound (but adds no information to the oracle).

These two ${\mathrm{MSB}}_k$ functions differ slightly in value, though they express the same intention. The msb_p instantiation can be understood as partitioning $\mathbb{N}$ into intervals of length approximately $p/2^k$, and returning a value in the same interval as $x$. The msb_kp1 instantiation can be understood as instead partitioning $\mathbb{N}$ into intervals of length $2^{n-(k+1)}$, and returning a value in the same interval as $x$. Noting that $p\approx 2^n$, one sees $p/2^k\approx 2^{n-k}$. Hence, msb_kp1 gives around one additional bit of information about $x$.¹³¹³13The additional bit is required because , so taking intervals of length exactly $2^{n-k}$ is not quite good enough to satisfy the msb_p_dist assumption, but taking intervals of length $2^{n-(k+1)}$ is. This means instantiating the hnp locale with ${\mathrm{MSB}}_k=\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">msb\_p</em>}$ yields a slightly stronger result, since the associated oracle gives less information. Instantiating ${\mathrm{MSB}}_k=\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">msb\_kp1</em>}$, on the other hand, gives a computational interpretation.

We verify that both of these ${\mathrm{MSB}}_k$ functions satisfy the msb_k_dist assumption in the hnp locale, which means that a different instantiation of the top-level hnp_adversary_exists theorem can be derived for each choice of ${\mathrm{MSB}}_k$ (though an instantiation using msb_p will not yield an executable oracle).

The computational instantiation ${\mathrm{MSB}}_k=\text{<em class="ltx\_emph ltx\_font\_typewriter ltx\_font\_slanted" style="font-size:90\%;">msb\_kp1</em>}$ is useful for demonstrating an execution of the adversary on a realistic example, since example oracle queries can be directly computed from the definition of msb_kp1 via Isabelle/HOL’s code generator. We include a short example of this in our AFP entry.

In both our formalization of Babai’s algorithm and the HNP, we use Isabelle locales [2] to fix ambient variables. For the HNP, we define the hnp_adversary locale, which fixes $p$ and $d$, and is used to define the adversary $𝒜$ (see Section 3.1). Our main locale, hnp, inherits from this locale, and contains the rest of the proof. Note that if we defined $𝒜$ directly in the hnp locale, we could do the following:

While the “cheating” in this example is obvious, we want to ensure a similar “leak” cannot happen in a subtler way. Our hnp_adversary locale avoids the need to manually inspect the definition of $𝒜$ for such a leak because $\alpha$ is not present in the context in which we define $𝒜$.

Still, as always with formal developments, the truly scrupulous reader must perform some manual inspection of the definitions in the top-level statement to be assured of its correctness. In our case, a skeptic must verify that we do not pass $\alpha$ to the hnp_adversary locale through some other variable name (either the $p$ or $d$), which is easily checked by examining the locale inheritance in the hnp locale (discussed previously in Section 3.3). Moreover, it must be verified that in our definition of game, we do not pass more information about $\alpha$ to $𝒜$ than what is expressed in the statement of Theorem 1, which requires verifying our definition of $𝒪$. However, what is successfully avoided by our locale setup is the need to check our definition of $𝒜$ itself; since the main theorem is an existence proof, the scrupulous reader need only verify that the main theorem is correctly stated, and that $\alpha$ is not passed to $𝒜$ in the definition of game – it is not necessary to manually verify any aspect of the definition of the witness $𝒜$ itself.

The probability mass function (pmf) monad, defined in the Isabelle/HOL standard libraries, allows a user to express procedures involving probabilistic sampling using familiar do notation. For instance, a procedure which samples a value x from probability distribution p and checks if P x holds can be expressed as check_event $\equiv$ do {x $\leftarrow$ p; return_pmf (P x)}, and the probability that check_event returns True (i.e., the probability that P x holds) as pmf check_event True.

As we modeled our formalization on the game-playing style presented in the CryptHOL tutorial [30], we use the language of cryptographic games throughout our formalization (both in proofs and in our top-level statement) and thus frequently use do notation to express the probability of an event. Retrospectively, perhaps an explicitly measure-theoretic style would have been more standard – for instance, measure_pmf.prob p {x. P x} also expresses the probability of P x when x is sampled from p.

Indeed, we found that the existing lemma support for probabilistic reasoning is primarily focused on supporting such measure-theoretic reasoning, and is not as well-developed for working directly with the pmf monad. Consequently, our use of the pmf monad (specifically for expressing games with do notation) made it challenging to find relevant helper lemmas – for instance, we could not find a lemma directly stating that if P x $\to$ Q x, then

Yet, there is a lemma for the measure-theoretic analog, i.e. {x. P x} $\subseteq$ {x. Q x} implies

If we chose to restrict our statements and proofs to such measure-theoretic expressions, or alternatively translated back and forth between measure-theoretic expressions and monadic pmf expressions, then the existing measure-theoretic lemmas could have been sufficient for our purposes. However, we believe that the pmf monad provides a valuable probabilistic language – in general, cryptographic games can be quite complex, which makes the intuitive expressivity of the do notation very valuable – that deserves a suite of specialized helper lemmas analogous to the existing measure-theoretic ones.

We establish helper lemmas which lift some basic measure_pmf.prob lemmas to apply directly to monadic pmf constructs. While most of these helper lemmas are not too challenging to prove (they typically involve translating a monadic pmf expression into an explicitly measure-theoretic form, applying the appropriate lemmas, then translating the result back to the pmf form), they support reasoning directly about cryptographic games expressed with do notation, which is convenient in manual proofs and also supports Sledgehammer’s automation. We believe our lemmas may be of use to future Isabelle/HOL users who wish to work extensively with probabilistic expressions involving do notation and the pmf monad.

We discuss one particularly notable pmf helper lemma here. Throughout our informal proof, we have assumed a sequence of $t_i$’s that are uniformly, independently sampled from a finite set; we formally achieve this using the replicate_pmf function, defined in Isabelle/HOL’s probability library (HOL-Probability) as follows:

Intuitively, if p is a probability distribution over elements of type ’a, then replicate_pmf n p gives a probability distribution over elements of type list ’a of length n. We formally prove that replicate_pmf matches our intuitive notion of repeated independent samples as follows:

Intuitively, this lemma states that the probability of a sequence of events occuring is simply the product of the probabilities of those events. In our formalization, we use this lemma to go from probability $1-A$ (for one event) to probability ${(1-A)}^d$ (for $d$ events) in the proof of Lemma 4. Furthermore, we use this lemma to connect replicate_pmf to the existing indep_events definition provided by the Isabelle/HOL probability library: