mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +00:00
zeekay
abf99d05fc
Restructured from flat .tex/.pdf files into per-paper subdirectories. Added Antje Worring as co-author on all papers. Synced PDFs to pdfs/ for download site.
60 lines
1.8 KiB
TeX
60 lines
1.8 KiB
TeX
\section{Cryptographic Primitive Verification}
|
|
|
|
|
|
\subsection{BLS Signature Aggregation}
|
|
|
|
BLS signatures allow aggregation: $n$ individual signatures can be combined into a single
|
|
signature of constant size. Correctness requires that aggregation preserves validity.
|
|
|
|
\begin{lstlisting}[language=Lean,caption={BLS aggregation correctness}]
|
|
-- Abstract model of BLS
|
|
axiom G1 : Type
|
|
axiom G2 : Type
|
|
axiom GT : Type
|
|
axiom pairing : G1 -> G2 -> GT
|
|
|
|
axiom sign : SecretKey -> Message -> G1
|
|
axiom verify : PublicKey -> Message -> G1 -> Prop
|
|
axiom aggregate_sigs : List G1 -> G1
|
|
axiom aggregate_keys : List PublicKey -> PublicKey
|
|
|
|
-- Correctness: individual verification
|
|
axiom verify_sign :
|
|
∀ sk pk msg, KeyPair sk pk ->
|
|
verify pk msg (sign sk msg)
|
|
|
|
-- Aggregation correctness
|
|
theorem aggregate_verify
|
|
(sks : List SecretKey) (pks : List PublicKey)
|
|
(msg : Message)
|
|
(h_pairs : ∀ i, KeyPair (sks[i]) (pks[i]))
|
|
(h_len : sks.length = pks.length) :
|
|
verify (aggregate_keys pks) msg
|
|
(aggregate_sigs (sks.map (· |> sign · msg))) := by
|
|
exact bls_aggregate_theorem h_pairs h_len
|
|
\end{lstlisting}
|
|
|
|
\subsection{Hash Function Properties}
|
|
|
|
\begin{lstlisting}[language=Lean,caption={Hash function model}]
|
|
-- Collision resistance as a type
|
|
structure CollisionResistant (H : Bytes -> Hash) : Prop where
|
|
no_collision : ∀ x y, x ≠ y -> H x ≠ H y
|
|
|
|
-- Merkle tree verification
|
|
theorem merkle_proof_sound
|
|
(H : Bytes -> Hash)
|
|
(hcr : CollisionResistant H)
|
|
(root : Hash) (leaf : Bytes) (proof : MerkleProof) :
|
|
verifyProof H root leaf proof ->
|
|
leaf ∈ leavesOf root := by
|
|
intro hverify
|
|
induction proof with
|
|
| nil => exact leaf_of_root hverify
|
|
| cons sibling rest ih =>
|
|
have := step_preserves_membership hcr hverify
|
|
exact ih this
|
|
\end{lstlisting}
|
|
|
|
%% ============================================================
|