saymrwulf/proof-aware-crypto-tooling-agent
1
0
Fork 0
mirror of https://github.com/saymrwulf/proof-aware-crypto-tooling-agent.git synced 2026-09-04 20:03:40 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

paper: position the two-disciplines bridge explicitly (intro, 2 sentences)

Browse source 
The LTL does not mechanize cryptographic security proofs (EasyCrypt and
relatives own that bridge, now cited); 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. Fit maintained at 4 pages (bottom
margin 1.95cm, bibliography scriptsize); pages 1 and 4 visually
inspected; 18 references.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
mrwulf 2026-07-07 10:06:12 +02:00
parent 3aa8d4b2bf
commit d4872b140a
2 changed files with 13 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

BIN
paper/ltl.pdf
View file

Binary file not shown.

16
paper/ltl.tex
View file

@ -1,5 +1,5 @@
\documentclass[10pt,twocolumn]{article} \documentclass[10pt,twocolumn]{article}
\usepackage[margin=1.7cm,bottom=2.1cm]{geometry} \usepackage[margin=1.7cm,bottom=1.95cm]{geometry}
\usepackage[T1]{fontenc} \usepackage[T1]{fontenc}
\usepackage{lmodern} \usepackage{lmodern}
\usepackage{microtype} \usepackage{microtype}
@ -134,7 +134,13 @@ databases---applied to a payload with different trust semantics:
exact assumption set}. We claim no novelty for any component (the hash exact assumption set}. We claim no novelty for any component (the hash
structure and proof algorithms are RFC~9162 verbatim); the contribution structure and proof algorithms are RFC~9162 verbatim); the contribution
is the composition, its trust model, and a deployed, reproducible is the composition, its trust model, and a deployed, reproducible
instance. 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:log} describes the log and its trust model,
\S\ref{sec:dogfood} the self-referential signing loop, \S\ref{sec:dogfood} the self-referential signing loop,
@ -400,7 +406,7 @@ and this paper were produced with substantial assistance from Claude
(Anthropic). All claims are enforced by the referenced check scripts and (Anthropic). All claims are enforced by the referenced check scripts and
are independently re-checkable from the public artifacts. are independently re-checkable from the public artifacts.
\begin{thebibliography}{19}\footnotesize \begin{thebibliography}{19}\scriptsize
\setlength{\itemsep}{1pt} \setlength{\itemsep}{1pt}
\bibitem{rfc6962} B.~Laurie, A.~Langley, E.~K\"asper. \bibitem{rfc6962} B.~Laurie, A.~Langley, E.~K\"asper.
@ -428,6 +434,10 @@ Users. \emph{USENIX Security}, 2015.
Automatic verification of transparency protocols. Automatic verification of transparency protocols.
\emph{IEEE EuroS\&P}, 2023. arXiv:2303.04500. \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. \bibitem{aeneas} S.~Ho, J.~Protzenko.
Aeneas: Rust verification by functional translation. Aeneas: Rust verification by functional translation.
\emph{Proc.\ ACM Program.\ Lang.} 6 (ICFP): 711--741, 2022. \emph{Proc.\ ACM Program.\ Lang.} 6 (ICFP): 711--741, 2022.