[proofplan]
The verification equation is a two-stage modular identity: the inner stage works modulo $p$ in the group $\langle g \rangle \subseteq (\mathbb{Z}/p\mathbb{Z})^\times$ of order $q$, and the outer stage reduces modulo $q$. We invert the signing equation modulo $q$ to express the nonce $k$ as $u_1 + x u_2 \pmod q$. Substituting into $g^{u_1} y^{u_2}$ and using that $g$ has order $q$ — so exponents may be taken modulo $q$ — yields $g^k \bmod p$, whose reduction modulo $q$ is precisely $s_1$.
[/proofplan]
[step:Recover the nonce $k$ modulo $q$ from the signing equation]
By construction, $s_2 \equiv k^{-1}(m + x s_1) \pmod q$, where $k^{-1}$ denotes the multiplicative inverse of $k$ in $(\mathbb{Z}/q\mathbb{Z})^\times$; this exists because $\gcd(k, q) = 1$ by the signer's choice of nonce. Since $s_2 \not\equiv 0 \pmod q$ by the non-triviality assumption, $s_2$ is invertible modulo $q$ (as $q$ is prime, $(\mathbb{Z}/q\mathbb{Z})^\times = (\mathbb{Z}/q\mathbb{Z}) \setminus \{0\}$), and the verifier's quantity $w = s_2^{-1} \bmod q$ is well defined. Multiplying both sides of the signing equation by $k s_2^{-1} \equiv k w \pmod q$:
\begin{align*}
s_2 k w \equiv k^{-1}(m + x s_1) \cdot k w \iff k \equiv w(m + x s_1) \pmod q,
\end{align*}
where the left side simplified via $s_2 \cdot s_2^{-1} = s_2 w \equiv 1$. Hence
\begin{align*}
k \equiv m w + x s_1 w \equiv u_1 + x u_2 \pmod q,
\end{align*}
using $u_1 = m w \bmod q$ and $u_2 = s_1 w \bmod q$.
[guided]
The key algebraic move is inverting $k^{-1}$ on the right. Why does that require $s_2 \ne 0 \pmod q$? The verifier's equation uses $w = s_2^{-1}$, which only exists when $s_2$ is a unit in $\mathbb{Z}/q\mathbb{Z}$. Because $q$ is prime, the units are exactly the non-zero residues, so the condition $s_2 \ne 0 \pmod q$ is exactly the invertibility condition. The DSA spec's requirement that $s_2 \ne 0$ — else draw a new nonce — is thus not a minor edge case but the hypothesis that makes $w$ well defined.
Similarly, the inverse $k^{-1}$ exists because $k$ is drawn from $\{1, \dots, q - 1\}$ and $q$ is prime, so $\gcd(k, q) = 1$ automatically. The identity $k \equiv u_1 + x u_2 \pmod q$ is the crux: it tells us that the verifier's two exponents $u_1, u_2$ encode the signer's nonce $k$ (and private key $x$) in a way that can be recombined multiplicatively in the exponent.
[/guided]
[/step]
[step:Substitute the public key and collect exponents modulo $p$]
The verifier computes $v$ by evaluating $g^{u_1} y^{u_2} \bmod p$. Substituting the public key $y = g^x \bmod p$:
\begin{align*}
g^{u_1} y^{u_2} \equiv g^{u_1} (g^x)^{u_2} \equiv g^{u_1 + x u_2} \pmod p.
\end{align*}
This is just the exponent law in the cyclic group $(\mathbb{Z}/p\mathbb{Z})^\times$, valid because $g, y \in (\mathbb{Z}/p\mathbb{Z})^\times$.
[/step]
[step:Reduce the exponent modulo $q$ using the order of $g$]
We next argue that $g^{u_1 + x u_2} \equiv g^k \pmod p$. By Step 1,
\begin{align*}
u_1 + x u_2 \equiv k \pmod q,
\end{align*}
so $u_1 + x u_2 = k + q \ell$ for some $\ell \in \mathbb{Z}$. Since $g$ has order exactly $q$ in $(\mathbb{Z}/p\mathbb{Z})^\times$, we have $g^q \equiv 1 \pmod p$, and therefore
\begin{align*}
g^{u_1 + x u_2} \equiv g^{k + q \ell} \equiv g^k \cdot (g^q)^\ell \equiv g^k \cdot 1^\ell \equiv g^k \pmod p.
\end{align*}
[guided]
Why is it essential that $g$ have order exactly $q$, not just that $g^q \equiv 1 \pmod p$? The argument needs two things: that $g^q \equiv 1 \pmod p$ (so that adding a multiple of $q$ to the exponent leaves $g^{\cdot}$ unchanged) **and** that $q$ divides $p - 1$ (so that a subgroup of order $q$ exists at all).
DSA arranges this by choosing $q \mid p - 1$ and letting $g := h^{(p-1)/q} \bmod p$ for some $h \in (\mathbb{Z}/p\mathbb{Z})^\times$ with $g \ne 1$. Then $g^q = h^{p-1} \equiv 1 \pmod p$ by Fermat's Little Theorem, and the order of $g$ divides $q$; since it is not $1$ and $q$ is prime, the order equals $q$. This subgroup structure is what allows exponents in $g^{\cdot}$ to be reduced modulo $q$ rather than modulo $p - 1$.
Without this structure — for instance, if $g$ had order $p - 1$ — the exponent $u_1 + x u_2$, computed modulo $q < p - 1$, would generally not agree with $k$ modulo the order of $g$, and the verification would fail.
[/guided]
[/step]
[step:Reduce modulo $q$ and match against $s_1$]
Combining the previous two steps:
\begin{align*}
g^{u_1} y^{u_2} \bmod p = g^{u_1 + x u_2} \bmod p = g^k \bmod p.
\end{align*}
(Each equality is an equality of integers in $\{0, 1, \dots, p - 1\}$ because both sides denote the unique representative of the same residue class modulo $p$.) Reducing once more modulo $q$:
\begin{align*}
v = \bigl( (g^{u_1} y^{u_2}) \bmod p \bigr) \bmod q = (g^k \bmod p) \bmod q = s_1,
\end{align*}
where the last equality is the definition of $s_1$. Hence $v = s_1$, and the verifier accepts.
[/step]
[step:Conclude correctness of the DSA verification procedure]
For any legitimately generated DSA signature $(s_1, s_2)$ on a message hash $m$ under private key $x$ and public key $y = g^x \bmod p$, the verifier's computed quantity $v$ equals $s_1$. Therefore the verifier accepts, which is the statement of correctness.
This completes the proof. The argument used the three structural facts of DSA:
- The invertibility of $s_2$ modulo $q$ (ensured by the spec's $s_2 \ne 0$ check and the primality of $q$).
- The identity $k \equiv u_1 + x u_2 \pmod q$ obtained by inverting the signing equation.
- The reduction of exponents modulo $q$, which holds because $g$ has order $q$ in $(\mathbb{Z}/p\mathbb{Z})^\times$.
[/step]
