diff --git a/paper/ltl.pdf b/paper/ltl.pdf index 60cdeae..61d3c5e 100644 Binary files a/paper/ltl.pdf and b/paper/ltl.pdf differ diff --git a/paper/ltl.tex b/paper/ltl.tex index bf4d685..6b8a93f 100755 --- a/paper/ltl.tex +++ b/paper/ltl.tex @@ -766,10 +766,10 @@ mechanized in the present corpus. The deployed internal consumer is a quorum-custody signing service: its inbound boundary accepts a log-derived statement only when independently attested verifier backends agree, and its policy consumes recorded -observations, never operator labels. A prospective external case study -examined the Swiss Post e-voting system, whose vendored Ed25519 dependency -matches an attested subject at family level but not at the attested version. -The model treats that as a useful negative: attestations are version-exact by +observations, never operator labels. A prospective external study +examined a production codebase whose vendored Ed25519 dependency matches an +attested subject at family level but not at the attested version. The model +treats that as a useful negative: attestations are version-exact by construction, and a family-level match confers nothing. \subsection{Proof portability across forks}