\section{ECDSA and Schnorr: Security and Computational Structure}
\label{sec:signatures}

\subsection{ECDSA}

Let $H$ be SHA-256 and $z$ the integer obtained from the leftmost $\lceil\log_2 n\rceil$ bits of $H(m)$ (for \secp{} all
256 bits; $z$ may exceed $n$ and is reduced). With private key $d\in[1,n)$ and public key $P=[d]G$, signing picks a
nonce $k\in[1,n)$, computes
\begin{equation}
  R=[k]G,\qquad r = x(R)\bmod n,\qquad s = k^{-1}(z+rd)\bmod n ,
  \label{eq:ecdsa-sign}
\end{equation}
and outputs $(r,s)$ with $r,s\ne0$. Verification computes $w=s^{-1}$, $u_1=zw$, $u_2=rw$, $X=[u_1]G+[u_2]P$ and
accepts iff $x(X)\bmod n=r$ \citep{nist2023fips186,certicom2009sec1}. Correctness: $X=[s^{-1}(z+rd)]G=[k]G=R$.
Bitcoin additionally requires \emph{low-$s$} ($s\le n/2$, BIP~62/146) because $(r,n-s)$ is also valid: the verification
point becomes $-X$, whose $x$-coordinate is unchanged (check~S5; formalised in Section~\ref{sec:formal}).

\paragraph{Where the security lives.} The nonce $k$ must be uniform and secret: $k$ known gives $d=(sk-z)r^{-1}$;
$k$ reused across two messages gives $k=(z_1-z_2)/(s_1-s_2)$ and then $d$ (our reference implements this textbook
recovery on synthetic keys, \code{recover\_private\_key\_from\_nonce\_reuse}); and a few bits of bias in many nonces
suffice for lattice recovery \citep{howgravegraham2001lattice,breitner2019biased}. RFC~6979 \citep{pornin2013rfc6979}
derives $k$ deterministically by HMAC-DRBG from $(d,H(m))$, which removes the randomness requirement at signing time
(the nonce is still secret because $d$ is). Timing and cache side channels in the scalar multiplication by $k$ are
the practical threat \citep{kocher1996timing,brumley2011remote,aldaya2020ladderleak,jancar2020minerva}; constant-time
scalar multiplication, as in \libsecp{} and the \kk{} crate, is the remedy and costs a measurable constant
(Table~\ref{tab:sig-impl}).

\paragraph{Proof structure.} ECDSA has no reduction to the DLP in the random-oracle model alone: the ``conversion
function'' $R\mapsto x(R)\bmod n$ is not a random oracle and its algebraic structure (it is even, $x(R)=x(-R)$, which is
the source of malleability) obstructs the forking-lemma argument. Known results prove security in the generic
group model \citep{brown2005generic}, under the assumption that the conversion function behaves as a bijective random
oracle \citep{fersch2016provable}, or for weakened unforgeability notions \citep{fersch2017one}; \citet{groth2022security}
give a modern generic-group treatment that covers key derivation and presignatures. \citet{vaudenay2003security}
surveys the early history. The contrast with Schnorr is structural, not quantitative (research question~B1).

\subsection{BIP340 Schnorr}

BIP340 \citep{wuille2020bip340} fixes the Schnorr scheme \citep{schnorr1991efficient} with three design decisions.
\emph{X-only public keys}: $P$ is encoded by $x(P)$ alone and implicitly has even $y$ (the signer negates $d$ if
needed), saving a byte and making keys compatible with Taproot tweaking \citep{wuille2020bip341}. \emph{Tagged hashes}:
$H_{\text{tag}}(m)=\mathrm{SHA256}(\mathrm{SHA256}(\text{tag})\,\|\,\mathrm{SHA256}(\text{tag})\,\|\,m)$ for the
tags \code{BIP0340/aux}, \code{BIP0340/nonce}, \code{BIP0340/challenge}, which separates domains at no cost since the
64-byte prefix fills exactly one compression block that can be precomputed. \emph{Key-prefixed challenge}:
$e = H_{\text{challenge}}(x(R)\,\|\,x(P)\,\|\,m)\bmod n$, which prevents related-key attacks and makes the scheme
non-malleable. Signing: $k_0=H_{\text{nonce}}(t\,\|\,x(P)\,\|\,m)\bmod n$ with $t = d\oplus H_{\text{aux}}(\text{aux})$,
$R=[k_0]G$, $k=k_0$ or $n-k_0$ so that $y(R)$ is even, $s=k+ed\bmod n$, signature $(x(R),s)$ in 64 bytes. Verification:
lift $x(P)$ and check
\begin{equation}
  [s]G = R + [e]P \quad\text{with } y(R) \text{ even and } x(R) \text{ as signed.}
  \label{eq:schnorr-verify}
\end{equation}
Correctness is the one-line identity $s=k+ed\Rightarrow [s]G=[k]G+[e][d]G$ (check~S6, formalised in
Section~\ref{sec:formal}). Our pure-Python implementation passes all 19 official test vectors, including the negative
vectors for $x\ge p$, $s\ge n$, odd $y(R)$ and wrong $R$; the Rust benchmark harness checks the same vectors with
both \libsecp{} and \kk{}, and 1000 signatures produced by each library are byte-identical and verify under the other
and under the Python reference (hypothesis~\Hname{H23}).

\paragraph{Proof structure.} Schnorr signatures are EUF-CMA secure under the discrete-logarithm assumption in the
random-oracle model via the forking lemma \citep{pointcheval2000security}; the reduction loses a factor of the number
of hash queries, and \citet{seurin2012exact} shows this loss is essentially unavoidable for forking-based proofs and
that the random oracle cannot be dispensed with for a natural class of reductions. The linear structure $s=k+ed$ is
also what makes batch verification and multi-signatures \citep{bellare2006multi,maxwell2019simple,nick2021musig2}
possible; the same linearity is what ECDSA's $k^{-1}$ destroys.

\subsection{Batch verification and multi-scalar multiplication}

Given $b$ signatures $(R_i,s_i)$ on messages $m_i$ under keys $P_i$, choose random weights $a_i$ ($a_1=1$, 128 bits
otherwise) and check
\begin{equation}
  \Big[\sum_i a_i s_i\Big]G = \sum_i [a_i]R_i + \sum_i [a_i e_i]P_i .
  \label{eq:batch}
\end{equation}
If any signature is invalid the check fails except with probability $2^{-128}$ \citep{naccache1994can,bellare1998fast,bernstein2012high}.
The right-hand side is a multi-scalar multiplication with $2b$ terms, computed by Straus interleaving
(cost $\approx 256$ doublings plus $2b\cdot 256/(w+1)$ additions with wNAF windows) or Pippenger's bucket method
(cost $\approx 2b\cdot\lceil 256/c\rceil$ additions plus $2^c$ buckets per window, asymptotically $O(b\cdot 256/\log b)$)
\citep{straus1964addition,pippenger1980evaluation,moller2001algorithms}. Batch verification does not change consensus:
it accepts exactly the sets of signatures that individual verification accepts (with the stated negligible error).
Hypothesis~\Hname{H13} measures the gain with our own instrumented Straus and Pippenger implementations on \kk{}
arithmetic (Section~\ref{sec:results}); the answer to~B2 is a saturating constant-factor speed-up of $3.1\times$
over single verification in the same arithmetic, bounded by the non-MSM work (square root for $R_i$, tagged hash).

\subsection{What can be simplified and what cannot (B3, B4)}

The algebraic identities behind the implementations---$x(-P)=x(P)$, $(\beta x,y)=[\lambda](x,y)$, Shamir's trick,
batch verification by random linear combination---are all consequences of the $\Z$-module structure of
$\langle G\rangle$ and of the shape of the curve equation; the symbolic checks of Section~\ref{sec:framework} and the
Lean statements of Section~\ref{sec:formal} confirm them but find nothing beyond them. We looked specifically for a
verification shortcut that avoids one of the two scalar multiplications in~\eqref{eq:schnorr-verify}: none exists
without changing the predicate, because any procedure that accepts exactly the solutions of $[s]G-[e]P=R$ must
evaluate a group element that depends on both $s$ and $e$, and in the generic-group model this needs $\Omega(\log n)$
group operations for each. The practical levers are the ones in Table~\ref{tab:sig-impl}: fixed-base tables for $G$,
GLV for $P$, Jacobian coordinates with a single final inversion, and batching.