diff --git a/llms.txt b/llms.txt index cbd089c..6d4b43b 100644 --- a/llms.txt +++ b/llms.txt @@ -18,7 +18,7 @@ ## Live evidence - Transparency log (RFC 9162): https://ltl.zkdefi.org — signed replay attestations of the Lean proofs, one leaf per fork. -- The paper: https://ltl.zkdefi.org/paper — "LTL: Lean Transparency Log". +- The paper: https://ltl.zkdefi.org/paper — "The Lean Transparency Log: Distributing Kernel-Checked Correctness Evidence for Deployed Ed25519 Implementations" (revised, with security proofs; prior version at /paper/v0.1). ## For agents diff --git a/paper/ltl-v0.0.pdf b/paper/ltl-v0.0.pdf deleted file mode 100644 index 25e8471..0000000 Binary files a/paper/ltl-v0.0.pdf and /dev/null differ diff --git a/paper/ltl-v0.0.tex b/paper/ltl-v0.0.tex deleted file mode 100644 index e5ba255..0000000 --- a/paper/ltl-v0.0.tex +++ /dev/null @@ -1,481 +0,0 @@ -\documentclass[10pt,twocolumn]{article} -\usepackage[margin=1.7cm,bottom=1.95cm]{geometry} -\usepackage[T1]{fontenc} -\usepackage{lmodern} -\usepackage{microtype} -\usepackage{amsmath} -\usepackage{amssymb} -\usepackage{booktabs} -\usepackage{tikz} -\usetikzlibrary{arrows.meta} -\usepackage[hidelinks]{hyperref} -\usepackage{xcolor} -\newcommand{\code}[1]{\texttt{\small #1}} -% poor-man's semantic brackets (stmaryrd unavailable in minimal TeX trees) -\newcommand{\den}[1]{[\![#1]\!]} -\setlength{\columnsep}{0.8cm} - -\title{\textbf{LTL: Lean Transparency Log}\\[2pt] -\large Where Deductive and Cryptographic Proof Vouch for Each Other} -\author{saymrwulf\\ \small \url{ltl.zkdefi.org}} -\date{July 2026} - -\begin{document} -\maketitle - -\begin{abstract} -Interactive theorem provers can certify the functional correctness of -deployed cryptographic code, but the resulting assurance is expensive to -\emph{consume}: re-checking a realistic proof corpus takes a proof -toolchain and hours of kernel time, which excludes almost every -downstream user, including autonomous agents that must decide which -cryptographic library to trust. We describe the \emph{Lean Transparency -Log} (LTL)\footnote{Not to be confused with linear temporal -logic~\cite{pnueli77}; the collision is acknowledged and, in a paper -about verification, difficult to resist.}, a deployed RFC~9162-style -transparency log whose leaves are \emph{replay attestations}: signed -statements that the Lean~4 proofs of a specific Rust repository, at a -specific git commit, re-check with exactly their documented axiom sets. -Consumers verify one signature and a logarithmic inclusion proof in -milliseconds; the hours of kernel time are paid once, by the log -operator. Three design decisions distinguish the LTL from prior -attestation transparency systems: (i)~consumers re-derive verification -verdicts locally from the \emph{observed axiom cones} carried in each -attestation, so the operator is trusted for observations, never for -verdicts; (ii)~axiom cones are matched against per-theorem -\emph{documented boundaries} exactly, in both directions; and (iii)~the -log's tree heads are signed by a binary built from the very Ed25519 -implementation whose correctness certificates are leaves of the log, and -each signature embeds the operator's own Merkle self-check of that leaf. -We report a small production deployment covering four verified -production Ed25519 implementations, describe what the accumulated -evidence does and does not establish, and outline the natural next step: -verifying the log's own proof-checking algorithms in Lean and entering -those certificates into the log they defend. -\end{abstract} - -\section{Introduction} -\label{sec:intro} - -Formal verification of deployed cryptographic code has matured from -research prototypes to substantial artifacts: verified-by-construction -libraries such as HACL*~\cite{hacl} and Fiat-Crypto~\cite{fiatcrypto} -ship in mainstream software, and post-hoc verification pipelines such as -Aeneas~\cite{aeneas} make it possible to state and prove theorems about -\emph{existing} production Rust code. The corpus underlying this paper -is of the latter kind: four production Ed25519 -implementations---upstream \code{curve25519-dalek}/\code{ed25519-dalek} -and three deployed forks (Solana, RISC~Zero, Betrusted)---each carry -Lean~4~\cite{lean4} certificates, proven against that fork's own -extracted model, covering field arithmetic over $\mathbb{F}_{2^{255}-19}$, -the complete twisted Edwards laws~\cite{bernsteinlange,twisted}, scalar -arithmetic mod $\ell$, encoding/decoding with constructive point -decompression, and a four-tier characterization of signature -verification~\cite{ed25519,rfc8032} whose strongest tier states: the -extracted verifier accepts iff the signature's $R$ component decompresses -to a valid curve point equal to $[k](-A)+[s]B$. - -\paragraph{What the certificates state.} Concretely, the corpus is a -stack of theorems about extracted code, each stated through a -\emph{denotation} from machine representation to mathematics. Field -elements are five 51-bit limbs denoting -$\den{(a_0,\dots,a_4)}=\sum_i a_i2^{51i}\bmod p$, and every -operation carries a two-clause specification---the value is right -\emph{and} the representation invariant is preserved, e.g. -\begin{align*} -\footnotesize -\forall a\,b.\ &\mathrm{bnd}\,a \Rightarrow \mathrm{bnd}\,b \Rightarrow{}\\[-2pt] -&\exists c.\ \code{mul}\,a\,b = \code{ok}\,c \,\wedge\, \mathrm{bnd}\,c -\,\wedge\, \den{c} = \den{a}\cdot\den{b}. -\end{align*} -Point operations are proven to implement the complete twisted Edwards -addition law on -$E : -x^2+y^2 = 1+d\,x^2y^2$ over $\mathbb{F}_p$, -\begin{equation*} -\small -(x_1,y_1)+(x_2,y_2)= -\Bigl(\tfrac{x_1y_2+x_2y_1}{1+d\,x_1x_2y_1y_2},\; -\tfrac{y_1y_2+x_1x_2}{1-d\,x_1x_2y_1y_2}\Bigr), -\end{equation*} -including the completeness fact that makes it branch-free ($a=-1$ is a -square and $d$ a non-square in $\mathbb{F}_p$, so the denominators never -vanish~\cite{bernsteinlange}). -At the apex, writing $\code{accept}(A,m,R,s)$ for ``the extracted -verifier returns \code{ok}'', with $k$ the scalar produced by the hash -oracle $H(R,A,m)$ and no properties assumed of $H$, the byte-level tier -states -\begin{equation*} -\footnotesize -\code{accept}(A,m,R,s) \;\Leftrightarrow\; \code{compress}([s]B-[k]A) = R, -\end{equation*} -and the strongest tier lifts byte equality to the group: -\begin{equation*} -\footnotesize -\code{accept}(A,m,R,s) \;\Leftrightarrow\; \code{decompress}(R) = [k](-A)+[s]B, -\end{equation*} -with decompression itself proven (exact byte parsing, the -$(p{+}3)/8$-power square root, sign-bit root selection). Each theorem's -axiom cone is pinned exactly---the standard three below the apex, the -enumerated oracle boundary at the apex tiers. - -The economics of \emph{consuming} such evidence are poor: re-checking -one fork's certificates takes $\approx$30 minutes of Lean kernel time -and a pinned toolchain. A wallet, a package manager, or an autonomous -agent choosing a cryptographic backend cannot pay this per -decision---and need not: a deterministic re-check yields a fact that can -be attested once and distributed. - -This is the classic transparency-log trade---Certificate -Transparency~\cite{rfc6962,rfc9162} for certificate issuance, Sigstore's -Rekor~\cite{sigstore} for signing events and supply-chain -attestations~\cite{intoto}, key transparency~\cite{coniks}, checksum -databases---applied to a payload with different trust semantics: -\emph{evidence of machine-checked mathematical truth, together with its -exact assumption set}. We claim no novelty for any component (the hash -structure and proof algorithms are RFC~9162 verbatim); the contribution -is the composition, its trust model, and a deployed, reproducible -instance. The LTL does not mechanize cryptographic security -proofs---that inter-disciplinary bridge is already being built by -EasyCrypt and its relatives~\cite{easycrypt}. It bridges the adjacent, -mostly empty gap: type-theory-certified artifacts have no distribution -infrastructure, and cryptographic transparency infrastructure has never -carried kernel-checked mathematics---each discipline solving the -other's problem. - -\S\ref{sec:log} describes the log and its trust model, -\S\ref{sec:dogfood} the self-referential signing loop, -\S\ref{sec:deploy} the deployment and what its evidence establishes, -and \S\ref{sec:next} the verification agenda for the log itself. - -\section{The Lean Transparency Log} -\label{sec:log} - -\begin{figure*}[t] -\centering -\begin{tikzpicture}[every node/.style={font=\small}] - \tikzset{box/.style={draw, rounded corners=2pt, minimum width=1.6cm, minimum height=0.56cm}} - % leaves: 0-3 failed run (gray), 4-7 verified (black) - \foreach \i/\c in {0/gray, 1/gray, 2/gray, 3/gray, 4/black, 5/black, 6/black, 7/black} - \node[box, draw=\c, text=\c] (l\i) at (\i*2.05,0) {leaf \i}; - \node[box, draw=black, very thick, fill=black!6] at (4*2.05,0) {\textbf{leaf 4}}; - \node[text=gray, font=\footnotesize] at (3*2.05/2 - 1.02,-0.62) {failed-audit run --- retained forever}; - \node[font=\footnotesize] at (5.5*2.05 + 0.35,-0.62) {verified attestations (16/16, boundary-exact)}; - % internal nodes - \foreach \i in {0,...,3} - \node[box] (m\i) at (\i*4.1+1.025,1.25) {node}; - \foreach \i in {0,1} - \node[box] (n\i) at (\i*8.2+3.075,2.5) {node}; - \node[box, thick] (root) at (7.175,3.75) {root}; - \foreach \a/\b in {l0/m0, l1/m0, l2/m1, l3/m1, l4/m2, l5/m2, l6/m3, l7/m3, - m0/n0, m1/n0, m2/n1, m3/n1, n0/root, n1/root} - \draw[gray!70] (\a) -- (\b); - % signature head - \node[box, thick, minimum width=5.2cm] (sig) at (7.175,4.95) - {signed tree head: $\mathrm{Ed25519}(\mathrm{root})$}; - \draw[-{Stealth}] (root) -- (sig); - % the self-certification loop, routed through clear space on the right - \draw[-{Stealth}, thick, dashed] - (sig.east) .. controls (13.2,4.95) and (12.4,1.6) .. (l4.north east); - \node[align=left, font=\footnotesize, anchor=west] at (12.45,3.1) - {signed by the binary built\\ from the source attested at\\ leaf 4; the operator verifies\\ that leaf's inclusion first}; -\end{tikzpicture} -\caption{The deployed 8-leaf log. Leaves 0--3 record an early replay whose -audit step failed (two tooling defects, since fixed); an append-only ledger -retains them. The tree head is signed by a binary built from the -implementation attested at leaf 4, and each signature embeds the operator's -own inclusion check of that leaf against the tree being signed.} -\label{fig:loop} -\end{figure*} - -\paragraph{Roles.} The system has exactly two roles with deliberately -asymmetric costs and capabilities. The \emph{operator} (one per log) -owns a Lean toolchain, replays proof corpora, holds the log's signing -key, and bears append-only obligations. \emph{Consumers} (unbounded) -hold the operator's public key, receive small evidence files, and verify -with $\approx$25 lines of standard-library code. Nothing a consumer does -requires a theorem prover. - -\paragraph{Leaves: replay attestations.} A leaf is the canonical JSON -serialization of an attestation recording: the subject repository URL -and \emph{git commit} (which cryptographically pins the entire source -tree); the toolchain versions; the resource-control regime under which -the replay ran; and, per certificate, its name, replay status, and the -\emph{observed axiom cone}---the exact output of Lean's -\code{\#print axioms} for that theorem. For the corpus above each -attestation carries 16 certificates. - -\paragraph{Boundary-exact auditing.} Every certificate has a -\emph{documented} allowed axiom set. Foundational certificates must -carry exactly Lean's three standard axioms -(\code{propext}, \code{Classical.choice}, \code{Quot.sound}); the four -signature-tier certificates additionally carry a per-fork, explicitly -enumerated boundary (an opaque SHA-512 oracle and opaque wire-format -types---e.g., eleven axioms in total for the upstream fork). A cone is -\emph{clean} iff it equals its allowed set; deviation in either -direction---an unexpected axiom, or a missing boundary axiom---is -flagged. Each source repository enforces the same discipline in its own -check scripts; the log mirrors those sets and treats the repositories' -scripts as authoritative. - -\paragraph{Observation, not verdict.} Attestations include the -operator's pass/fail judgment, but consumers ignore it: the consumer's -tooling re-derives every verdict locally by comparing the -\emph{observed} cone against the consumer's own copy of the allowed -sets. An operator that labels a dirty cone ``clean'' gains nothing; an -attestation that omits observed cones is treated as unverifiable. This -narrows the trust placed in the operator to: ``the reported -\code{\#print axioms} output is what the kernel printed for this commit.'' - -\paragraph{Tree, heads, receipts.} Leaves are accumulated in an -RFC~9162 Merkle tree ($\mathrm{SHA}$-256 with $0x00/0x01$ -leaf/node domain separation). The operator signs tree heads; consumers -receive a \emph{receipt}: leaf index, sibling path, and the signed head. -Consumers additionally maintain a local pin store: same-size heads must -match the pinned root exactly (a mismatch is reported as equivocation -and is unrecoverable); growth requires a verified consistency proof from -the pinned size; shrinkage is rejected. A freshness policy bounds head -age. The full log is also published as a git repository (one file per -leaf, plus every head ever signed), so any cloner can recompute every -prefix root from the public leaves and audit the complete head history -without consistency proofs---a low-infrastructure witness -mechanism~\cite{rfc9162}; a standalone $\approx$150-line -standard-library verifier ships in the mirror. - -\section{The self-certifying signature} -\label{sec:dogfood} - -Tree heads are Ed25519 signatures, and this creates an opportunity for -coherence: the log \emph{contains} correctness certificates for an -Ed25519 implementation. The LTL's heads are therefore signed by a binary -built from the pinned source tree of exactly the implementation attested -in the log (serial backend pinned, matching the verified extraction), -and---before signing---the operator runs the same Merkle inclusion -verification a consumer runs, on the newest leaf attesting the signing -implementation, against the tree about to be signed. The verdict is -embedded in the signature block: - -{\small -\begin{verbatim} -signing_backend: verified-dalek-serial -signing_library_source_commit: aa0f6ab... -signing_library_leaf_index: 4 -signing_library_certificates_proven: 16/16 -self_inclusion: verified -\end{verbatim}} - -\noindent The signature vouches for the tree; the tree vouches for the -code that produced the signature; and the two vouchings are different -proof modalities (cryptographic and deductive), so the loop is -self-referential without being circular -(Fig.~\ref{fig:loop}). We state the honest extent of this claim -precisely: the Lean certificates cover the \emph{verification} path of -the library (the theorems' subject is the extraction image of that -path); the \emph{signing} path is not covered by any certificate and is -declared trusted base---the design merely ensures the trusted signing -code is the attested artifact rather than an unrelated third -implementation, and that consumers can check as much. Signature -\emph{verification} on consumer machines can optionally run through the -same certified-source binary, with the backend that actually ran -recorded in every result and a fail-closed policy flag available. -First-append bootstrapping is handled honestly: heads signed before the -signing library's attestation enters the log record -\code{self\_inclusion:\ library\_not\_in\_log}. - - - -\section{Deployment and evidence} -\label{sec:deploy} - -The LTL is deployed\footnote{Service: -\url{https://ltl.zkdefi.org} (read-only HTTP API and -documentation). Mirror: \url{https://github.com/saymrwulf/lean-transparency-log}. -Operator/consumer tooling and a twelve-lecture course: -\url{https://github.com/saymrwulf/proof-aware-crypto-tooling-agent}. The -underlying proof corpora are in the \code{saymrwulf/*-ed25519-verified} -repositories; every claim in this paper is re-checkable from these -artifacts.} with eight leaves: one attestation per fork from each of two -full replay runs (58--64 Lean files and $\approx$1{,}800\,s per -fork, under hard memory caps and core pinning). In the second run all -four forks reported 16/16 certificates proven with boundary-exact cones, -pinned to exact commits. The first run is deliberately still in the log: its audit step -failed due to two defects in the \emph{operator tooling} (a path issue -and a parser that mishandled Lean's line-wrapped axiom lists for the -eleven-axiom cones), and the operator signed attestations recording the -failure rather than suppressing the run. We consider the resulting -ledger---four failure leaves permanently beside four success -leaves---a feature of the trust model, and note that both defects were -fail-closed: valid proofs were rejected; invalid ones were never -accepted. - -\paragraph{What a verified receipt establishes.} Under the assumptions -enumerated below, a consumer who verifies a receipt knows: \emph{the -operator whose key I pinned attests that the Lean certificates of -repository $X$ at commit $Y$ re-check, with per-certificate observed -axiom cones as included---and this statement is part of the log -presented to every other consumer}. Combined with local verdict -re-derivation, this yields source-level assurance for the pinned -commit. It deliberately does \emph{not} establish: correctness of any -binary (consumers build from the pinned source; compilers are trusted -base), correctness of SHA-512 (an opaque oracle in the theorems), -correctness of the wire-format parsers (their outcomes are hypotheses of -the signature tiers), signing-side correctness, or side-channel -properties. The assumption set, in full: the Lean kernel and its three -axioms plus mathlib; faithfulness of the Charon/Aeneas -extraction~\cite{aeneas}; each fork's documented oracle boundary; -operator key custody and the trust-on-first-use key distribution -(mitigated by publishing the key in two independent locations); -collision resistance of SHA-256 for the log; unforgeability of Ed25519 -for the heads; and the consumer's own $\approx$25-line verifier. - -\paragraph{An observational by-product: proof portability.} Because the -four corpora prove the same theorems against four independent -extractions, the diff between proof files measures how portable proofs -are across real forks. Pure-mathematics files (e.g., a carry-telescope -lemma file) are byte-identical across all four; extraction-facing proof -scripts diverge sharply where the forks' code or the extractor's naming -differs (e.g., 215 changed lines for the byte-parser proofs on the two -forks whose extraction produces a closure-based loader; 121 lines for -the signature-glue proofs on the same-crate fork; 27 lines---all -annotation---between the two structurally closest forks, documenting the -one fork's \code{black\_box} optimization barrier). Per-target -verification, in other words, is doing measurable work exactly where the -targets actually differ. - -\section{Related work} -\label{sec:related} - -Certificate Transparency~\cite{rfc6962,rfc9162} supplies the data -structure and proof algorithms, used here unchanged. Rekor within -Sigstore~\cite{sigstore} is the closest deployed system: a transparency -log over signing events and supply-chain attestations such as -in-toto~\cite{intoto} link metadata; its payloads attest \emph{process} -(who signed, how an artifact was built), whereas LTL leaves attest -kernel-checked \emph{mathematical statements together with their -assumption sets}, and the consumer re-derives verdicts rather than -trusting labels. Key transparency~\cite{coniks} and checksum databases -share the pattern with different payloads. Proof-carrying -code~\cite{pcc} ships proofs to consumers who check them; the LTL serves -consumers who cannot run any checker, replacing proof transport with -attestation, inclusion, and signature---at the cost of trusting the -operator's kernel run, a cost the design minimizes but does not -eliminate. Cheval, Moreira and Ryan formally verify transparency -protocols themselves~\cite{cheval}; our direction is the complement -(we log the verification), and \S\ref{sec:next} proposes meeting in the -middle. Verified Merkle tree \emph{implementations} exist, notably in -EverCrypt~\cite{evercrypt}; \S\ref{sec:next} builds on that precedent -rather than claiming it. - -\section{Limitations and next steps} -\label{sec:next} - -\paragraph{Limitations.} The deployment is small (one operator, eight -leaves, four subject repositories) and the operator is a single party; -split-view defense currently rests on consumer-side pinning plus the -public git mirror rather than an independent witness network. Key -distribution is trust-on-first-use. The signing path of the dogfood -binary is unverified (declared, not proven). The corpus itself stops at -source-level assurance---reproducible builds and side-channel evidence -remain open---and ML-DSA slots in the head format are deliberately -recorded as unavailable rather than backed by an unverified -implementation. - -\paragraph{Verifying the accumulator itself.} The natural next step -applies the corpus's own discipline to the log's cryptographic half, -which is currently the \emph{unproven} half of the composition. All of -the following are tractable Lean targets: (i)~completeness of the -RFC~9162 inclusion verifier (honest proofs verify---no assumptions); -(ii)~\emph{soundness as an explicit reduction}: an accepting inclusion -proof for a leaf outside the tree yields a SHA-256 collision, making -collision resistance a documented boundary axiom audited exactly like -the SHA-512 oracle in the Ed25519 tiers; (iii)~the analogous statement -for the consistency verifier (acceptance implies prefix, modulo -collisions); (iv)~domain separation as a lemma; and (v)~total -correctness of the consumer's pin-store state machine (equivocation -detection, rollback rejection). Verified Merkle implementations in -F*~\cite{evercrypt} and algorithm verifications in other systems show -these proofs are well within reach; the LTL-specific closure is -\emph{where the certificates go}: into the log they defend, checked by -the certified checker they specify, alongside a consumer policy flag -requiring the certified verifier. At that point both proving traditions -in the composition run on certified code, and the remaining trusted base -is two hash assumptions, a compiler, an extraction pipeline, and one -key. - -\paragraph*{Acknowledgments.} The proof corpora, tooling, deployment, -and this paper were produced with substantial assistance from Claude -(Anthropic). All claims are enforced by the referenced check scripts and -are independently re-checkable from the public artifacts. - -\begin{thebibliography}{19}\scriptsize -\setlength{\itemsep}{1pt} - -\bibitem{rfc6962} B.~Laurie, A.~Langley, E.~K\"asper. -\emph{Certificate Transparency}. RFC 6962, 2013. - -\bibitem{rfc9162} B.~Laurie, E.~Messeri, R.~Stradling. -\emph{Certificate Transparency Version 2.0}. RFC 9162, 2021. - -\bibitem{sigstore} Z.~Newman, J.~S.~Meyers, S.~Torres-Arias. -Sigstore: Software Signing for Everybody. -\emph{ACM CCS}, pp.~2353--2367, 2022. - -\bibitem{intoto} S.~Torres-Arias, H.~Afzali, T.~K.~Kuppusamy, -R.~Curtmola, J.~Cappos. in-toto: Providing farm-to-table guarantees for -bits and bytes. \emph{USENIX Security}, 2019. - -\bibitem{coniks} M.~S.~Melara, A.~Blankstein, J.~Bonneau, -E.~W.~Felten, M.~J.~Freedman. CONIKS: Bringing Key Transparency to End -Users. \emph{USENIX Security}, 2015. - -\bibitem{pcc} G.~C.~Necula. Proof-Carrying Code. -\emph{ACM POPL}, pp.~106--119, 1997. - -\bibitem{cheval} V.~Cheval, J.~Moreira, M.~Ryan. -Automatic verification of transparency protocols. -\emph{IEEE EuroS\&P}, 2023. arXiv:2303.04500. - -\bibitem{easycrypt} G.~Barthe, B.~Gr\'egoire, S.~Heraud, -S.~Zanella~B\'eguelin. Computer-Aided Security Proofs for the Working -Cryptographer. \emph{CRYPTO}, LNCS 6841, pp.~71--90, 2011. - -\bibitem{aeneas} S.~Ho, J.~Protzenko. -Aeneas: Rust verification by functional translation. -\emph{Proc.\ ACM Program.\ Lang.} 6 (ICFP): 711--741, 2022. - -\bibitem{lean4} L.~de~Moura, S.~Ullrich. -The Lean 4 Theorem Prover and Programming Language. -\emph{CADE-28}, LNCS 12699, pp.~625--635, 2021. - -\bibitem{hacl} J.-K.~Zinzindohou\'e, K.~Bhargavan, J.~Protzenko, -B.~Beurdouche. HACL*: A Verified Modern Cryptographic Library. -\emph{ACM CCS}, 2017. - -\bibitem{evercrypt} J.~Protzenko et al. -EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. -\emph{IEEE S\&P}, 2020. - -\bibitem{fiatcrypto} A.~Erbsen, J.~Philipoom, J.~Gross, R.~Sloan, -A.~Chlipala. Simple High-Level Code for Cryptographic Arithmetic---With -Proofs, Without Compromises. \emph{IEEE S\&P}, pp.~1202--1219, 2019. - -\bibitem{ed25519} D.~J.~Bernstein, N.~Duif, T.~Lange, P.~Schwabe, -B.-Y.~Yang. High-speed high-security signatures. -\emph{J.\ Cryptographic Engineering} 2(2): 77--89, 2012. - -\bibitem{rfc8032} S.~Josefsson, I.~Liusvaara. -\emph{Edwards-Curve Digital Signature Algorithm (EdDSA)}. RFC 8032, 2017. - -\bibitem{bernsteinlange} D.~J.~Bernstein, T.~Lange. -Faster addition and doubling on elliptic curves. -\emph{ASIACRYPT}, LNCS 4833, pp.~29--50, 2007. - -\bibitem{twisted} D.~J.~Bernstein, P.~Birkner, M.~Joye, T.~Lange, -C.~Peters. Twisted Edwards curves. -\emph{AFRICACRYPT}, LNCS 5023, pp.~389--405, 2008. - -\bibitem{pnueli77} A.~Pnueli. The temporal logic of programs. -\emph{IEEE FOCS}, pp.~46--57, 1977. - -\end{thebibliography} - -\end{document} diff --git a/paper/ltl.pdf b/paper/ltl.pdf index d379eb0..b9eea27 100644 Binary files a/paper/ltl.pdf and b/paper/ltl.pdf differ diff --git a/paper/ltl.tex b/paper/ltl.tex index bdb6729..d7de5aa 100755 --- a/paper/ltl.tex +++ b/paper/ltl.tex @@ -791,9 +791,12 @@ C. Peters. Twisted Edwards curves. AFRICACRYPT, LNCS 5023, pp. 389--405, Each leaf is the canonical JSON serialization (sorted keys, no insignificant whitespace, UTF-8) of an attestation. Below is leaf~8 of -the deployed log---the re-attestation of the upstream fork---with the -16-certificate array elided to its first (foundational) and last (apex) -entries; all other fields are verbatim. +the deployed log---the re-attestation of the upstream fork. The +16-certificate array is elided to its first (foundational) and last +(apex) entries, and long values (hashes, timestamps, version strings, +paths) are shortened with ellipses; field names, structure, and the +axiom lists are verbatim, and the unelided leaf is one \texttt{jq} +invocation away in the public mirror. \begin{quote}\ttfamily\scriptsize \{ "type": "pacta.attestation", "schema\_version": 1,\\ \hspace*{0.6em}"attestation": \{\\ diff --git a/provider/src/pacta_provider/web.py b/provider/src/pacta_provider/web.py index 911d76e..4839412 100644 --- a/provider/src/pacta_provider/web.py +++ b/provider/src/pacta_provider/web.py @@ -46,17 +46,12 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf if route in ("/", "/docs"): self._send_html(docs_html) elif route in ("/paper", "/paper/ltl.pdf", - "/paper/v0.1", "/paper/v0.1/ltl.pdf", - "/paper/v0.0", "/paper/v0.0/ltl.pdf"): - # /paper is the current (v2) paper; /paper/v0.1 the prior named - # version, /paper/v0.0 the pseudonymous version. Older versions - # are served but deliberately unlisted (the docs page links only - # the current one) - versions are preserved, not advertised. + "/paper/v0.1", "/paper/v0.1/ltl.pdf"): + # /paper is the current (revised) paper; /paper/v0.1 the prior + # version - preserved for citability, linked from the docs page. variant = "current" if route.startswith("/paper/v0.1"): variant = "v0.1" - elif route.startswith("/paper/v0.0"): - variant = "v0.0" body = paper_pdfs.get(variant) if body is None: self._send(404, {"error": f"paper ({variant}) not available on this deployment"}) @@ -231,9 +226,8 @@ def serve( docs_html = render_docs(log, base_path) paper_dir = Path(__file__).resolve().parents[3] / "paper" variants = { - "current": paper_dir / "ltl.pdf", # v2 (revised), the live paper - "v0.1": paper_dir / "ltl-v0.1.pdf", # prior named 4-page version - "v0.0": paper_dir / "ltl-v0.0.pdf", # pseudonymous version + "current": paper_dir / "ltl.pdf", # revised paper, the live one + "v0.1": paper_dir / "ltl-v0.1.pdf", # prior 4-page version } paper_pdfs = {name: p.read_bytes() for name, p in variants.items() if p.is_file()} handler = make_handler(log, base_path, docs_html, paper_pdfs) diff --git a/provider/src/pacta_provider/webdocs.py b/provider/src/pacta_provider/webdocs.py index ec12b15..8bcd920 100644 --- a/provider/src/pacta_provider/webdocs.py +++ b/provider/src/pacta_provider/webdocs.py @@ -271,10 +271,15 @@ our roadmap. (The full walk-through is lecture 11 in the course.)

The paper

-
LTL: Lean Transparency Log -(PDF, 4 pages) — the design in full: the trust model (observations, never verdicts), -the self-certifying signature, the deployment with its retained failure leaves, and an -exact account of what a verified receipt does and does not establish.
+
The Lean Transparency Log: Distributing +Kernel-Checked Correctness Evidence for Deployed Ed25519 Implementations +(PDF, 14 pages, revised) — the trust model with an explicit malicious-operator adversary, +security proofs for every consumer-facing claim (inclusion soundness as an explicit +SHA-256-collision extractor, pin-store safety with transferable equivocation evidence, +verdict integrity), the self-referential signing loop, the twelve-leaf deployment with +its retained failure leaves, and appendices with the leaf schema, the full ~25-line +consumer verifier, and the verbatim per-fork axiom boundaries. +Previous version: v0.1 (4 pages).

Log heads are signed offline; this service is read-only and holds no key material. Provider tooling, agent tooling, and the full course (12 Jupyter diff --git a/tests/test_web_and_witness.py b/tests/test_web_and_witness.py index 7545e41..3b542a6 100644 --- a/tests/test_web_and_witness.py +++ b/tests/test_web_and_witness.py @@ -63,20 +63,16 @@ def test_web_endpoints_and_online_proof_roundtrip(tmp_path): with urllib.request.urlopen(base + "/paper", timeout=10) as r: assert r.headers["Content-Type"] == "application/pdf" assert r.read(5) == b"%PDF-" - # versioned paper routes serve when their PDFs exist (current always - # does in this repo); older versions are unlisted but reachable - for path in ("/paper/ltl.pdf", "/paper/v0.1", "/paper/v0.0"): - try: - with urllib.request.urlopen(base + path, timeout=10) as r: - assert r.read(5) == b"%PDF-", path - except urllib.error.HTTPError as exc: - assert exc.code == 404 # variant PDF absent in this checkout - # older versions must NOT appear in the endpoint index (unlisted) + # the prior paper version stays reachable for citability + for path in ("/paper/ltl.pdf", "/paper/v0.1"): + with urllib.request.urlopen(base + path, timeout=10) as r: + assert r.read(5) == b"%PDF-", path + # the removed pseudonymous version must be gone entirely try: - urllib.request.urlopen(base + "/no-such", timeout=10) + urllib.request.urlopen(base + "/paper/v0.0", timeout=10) + raise AssertionError("expected 404 for removed /paper/v0.0") except urllib.error.HTTPError as exc: - idx = json.loads(exc.read()).get("endpoints", []) - assert not any("v0." in e for e in idx) + assert exc.code == 404 # the site's copy of the trust anchor (TOFU: two independent locations) with urllib.request.urlopen(base + "/log-public-key", timeout=10) as r: assert r.read() == (tmp_path / "k.pub").read_bytes()