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.
24 lines
1.4 KiB
TeX
24 lines
1.4 KiB
TeX
\section{Conclusion}
|
|
|
|
|
|
Protocol bugs are the hardest bugs to find and the most expensive to exploit. Tamarin
|
|
Prover provides machine-checked guarantees that a protocol is secure against all
|
|
adversary strategies in the Dolev-Yao model. For Lux Network, Tamarin verification of
|
|
the FROST-BLS bridge protocol found a reflection attack that would have caused bridge
|
|
liveness failures, and verified that the hybrid PQ handshake provides forward secrecy
|
|
even against quantum-capable adversaries.
|
|
|
|
The investment is modest: each protocol model took 2--3 days to write and seconds to
|
|
verify. The return is certainty that the protocol logic is correct, independent of the
|
|
implementation.
|
|
|
|
\begin{thebibliography}{99}
|
|
\bibitem{tamarin} Meier, S. et al. ``The TAMARIN Prover for the Symbolic Analysis of Security Protocols.'' CAV, 2013.
|
|
\bibitem{dolev1983} Dolev, D. and Yao, A. ``On the Security of Public Key Protocols.'' IEEE Transactions on Information Theory, 1983.
|
|
\bibitem{frost} Komlo, C. and Goldberg, I. ``FROST: Flexible Round-Optimized Schnorr Threshold Signatures.'' SAC, 2020.
|
|
\bibitem{mlkem} NIST. ``Module-Lattice-Based Key-Encapsulation Mechanism Standard (ML-KEM).'' FIPS 203, 2024.
|
|
\bibitem{proverif} Blanchet, B. ``An Efficient Cryptographic Protocol Verifier Based on Prolog Rules.'' CSFW, 2001.
|
|
\bibitem{hybrid} Stebila, D. et al. ``Hybrid Key Exchange in TLS 1.3.'' IETF Draft, 2024.
|
|
\end{thebibliography}
|
|
|