Pith. sign in

REVIEW 3 major objections 6 minor 61 references

LeanDY unifies type-based and trace-based proofs so stateful, unbounded, XOR-using protocols can be verified modularly in Lean, including payment-channel punishment under chain liveness.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.5

2026-07-12 02:42 UTC pith:RSM7RCJY

load-bearing objection Solid Lean library that actually unifies type-based automation with interactive trace proofs for stateful/XOR protocols and payment-channel liveness; the case study is real work, not a toy. the 3 major comments →

arxiv 2607.03406 v2 pith:RSM7RCJY submitted 2026-07-03 cs.CR cs.PL

LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean

Simon Jeanteur , Lorenzo Veronese , Magdalena Solitro , Matteo Maffei This is my paper
classification cs.CR cs.PL
keywords symbolic protocol verificationLeantype systemstrace invariantsconditional secrecyXORpayment channelsblockchain liveness
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Protocol verification has long split into automated tools that struggle with state, time, unbounded runs, and conditional secrecy, versus interactive theorem proving that is flexible but weakly automated for protocol work. This paper argues that the two styles can be combined: compositional type-based reasoning for modularity and automation, plus inductive trace-based reasoning when more expressivity is needed. The result is LeanDY, a Lean library that lets users write protocols in a small domain-specific language, obtain protocol-specific automation for well-typed exchanges, and fall back to interactive proofs for cross-layer or liveness goals. The library handles dynamic compromise, mutable state, and recursive conditional secrecy for XOR, including chained release patterns. To show the approach scales, the authors build a SegWit-style blockchain model and fully formalize two-party payment channels, proving both ordinary safety facts and that a revoked close is eventually punished if defenders and miners meet explicit liveness bounds.

Core claim

LeanDY shows that a single mechanized framework can support secrecy and authentication for stateful unbounded protocols together with recursive conditional secrecy for XOR, and that the same framework can verify payment-channel punishment mechanisms and properties that depend on chain liveness by combining type-based exchange proofs with interactive trace reasoning.

What carries the argument

The valid_exchange property for each message exchange, lifted by the transition function to preservation of the valid_trace invariant; secrecy is expressed by monotone, trace-dependent labels (including releasable conditional swaps and meets for XOR) whose lattice structure and soundness relative to a Dolev-Yao attacker supply the automation.

Load-bearing premise

The on-chain punishment guarantee holds only if defenders react within a fixed block budget, miners eventually include valid transactions within another fixed budget, and a single canonical chain can be reconstructed from the protocol trace.

What would settle it

Exhibit a well-typed payment-channel execution under the stated participant and miner liveness bounds in which a revoked commitment is published and the corresponding punishment transaction never appears on the reconstructed chain before the to_self_delay expires.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. The paper presents LeanDY, a Lean library for symbolic Dolev–Yao protocol verification that unifies compositional type-based reasoning with inductive trace-based proofs, extending the design of DY*. Guided by language-and-automation co-design, it provides an eDSL for protocol exchanges, a general trace invariant (valid_trace) parameterized by user predicates, secrecy labels that form a complete lattice over trace properties (including conditional-swap/releasable labels and meet/join), and automation (prove_* tactics, intro_valid_exchange, Aesop configurations) that discharges routine valid_exchange goals while allowing interactive Lean proofs for protocol-specific obligations. The framework supports mutable state, dynamic compromise, and recursive conditional secrecy for XOR via basis-generated labeling environments. As a substantial case study, the authors formalize SegWit-style UTXO blockchain primitives (TXIDs, witnesses, scripts via a decidable Script type class, spendable pointers, prefix-based chain validity) and an in-depth two-party payment-channel protocol, proving transaction-structure safety lemmas and a conditional punishment-liveness theorem (punish.eventually_on_chain) under explicit participant- and miner-liveness hypotheses.

Significance. If the development is as claimed, this is a solid and timely contribution to mechanized symbolic protocol analysis. It addresses a genuine gap between push-button tools (ProVerif/Tamarin) with limited expressiveness for state, liveness, and XOR, and fully interactive general-purpose provers with little protocol-specific automation. Strengths that should be credited explicitly: (i) machine-checked core results (type-system soundness Property 2, transition_valid, valid_exchange preservation) and a non-trivial case study with safety lemmas and a liveness theorem stated with explicit hypotheses; (ii) a reusable library design (UserPreds, CryptoPreds, ValidParsable, from_basis labeling) rather than a one-off protocol proof; (iii) a unified treatment of recursive conditional secrecy for XOR with dynamic compromise, previously not combined in a single mechanized framework; (iv) publicly available code. The payment-channel formalization, including chain-liveness-dependent punishment, is a convincing expressiveness demonstration for layer-2 protocols that automated tools struggle with.

major comments (3)
  1. Sec. 3.1.3–3.2 and Property 2 / transition_valid: The central soundness claims are stated as Lean theorems, which is a major strength, but the manuscript never states whether the accompanying library is sorry-free for these results and for the payment-channel development, nor which lemmas (if any) remain as axioms or incomplete proofs. For a journal archival claim of a mechanized framework, please add an explicit inventory (e.g., number of theorems, remaining sorries, and which results are fully checked vs. sketched in the paper only).
  2. Sec. 4.2.5, Listing 3 (punish.eventually_on_chain): The theorem is correctly conditional on hlpunish, hlminer, htime_budget, hnot_corrupt, h_old, and hno_race, and the single-chain reconstruction (List.get_blockchain) is an explicit modeling choice. The central claim that LeanDY can express such properties is therefore intact. However, the security discussion should more sharply separate (a) what is proved about the protocol under those hypotheses from (b) what is assumed about the network and miners, and should discuss how fragile the conclusion is if miner_liveness fails for even a short window relative to toSelfDelay. A short threat-model paragraph would prevent over-reading the result as unconditional Lightning security.
  3. Sec. 3.2.2 and the LAC claims: The paper asserts protocol-specific automation that gracefully hands control back for cryptographic goals, illustrated on a small authentication example. The payment-channel case study is the real stress test, yet there is no quantitative report (LOC of protocol vs. proof, fraction of goals closed by intro_valid_exchange / aesop_type_system, manual proof effort for signing invariants and liveness). Without this, the claim that LeanDY improves on extrinsic DY* / F* workflows remains qualitative. Adding a short evaluation table for the payment-channel development would make the automation contribution load-bearing rather than anecdotal.
minor comments (6)
  1. Fig. 1 and Sec. 2: The conditional-release running example is clear, but the notation [L1/L2]_E is introduced before the general Label structure (corrupt0) of Sec. 3.1.3; a forward pointer would help readers who start from the example.
  2. Sec. 3.1.2: Nonces are fixed a priori (η decided before execution), a deliberate departure from DY*. The text should briefly discuss the modeling cost for protocols that generate unboundedly many fresh nonces at runtime, even if the payment-channel Nonce inductive type is finite-parameterized by timepoints.
  3. Sec. 4.1.2 Script type class: Abstracting the Bitcoin VM to a decidable eval is reasonable; please note explicitly which real script features (e.g., OP_CHECKLOCKTIMEVERIFY edge cases, script size limits, non-standard scripts) are out of scope so that the gap to BIP-compliant validation is clear.
  4. Sec. 5 Related Work: The comparison with Wallez’s extrinsic DY* and with TLA+/Why3 Lightning efforts is present but could more crisply list feature-by-feature differences (XOR conditional labels, basis automation, blockchain liveness in one library). A small comparison table would help.
  5. Typos / polish: “♂radiation-alt” in Sec. 2 appears to be a corrupted compromise symbol; “LAC” is expanded inconsistently; Listing 2 uses “Id.run do” without explaining the Id monad to non-Lean readers. A light copy-edit pass is warranted.
  6. Availability: The GitHub link [32] is given; please also pin a commit or artifact DOI for long-term reproducibility of the exact development corresponding to this technical report.

Circularity Check

0 steps flagged

No circularity: LeanDY's security claims are ordinary inductive invariants and conditional theorems, not results forced by definition or self-citation.

full rationale

This is a mechanized verification paper whose load-bearing results are (i) type-system soundness (Property 2: AttackerKnows implies public and valid_bytes), (ii) transition_valid (valid_exchange preserves valid_trace), and (iii) the payment-channel safety lemmas plus punish.eventually_on_chain under explicit participant/miner liveness hypotheses. None of these reduce by construction to their inputs: labels and CryptoPreds/UserPreds are user-supplied protocol-specific components that the type system and transition function then check against an independent Dolev-Yao attacker model; the correspondence assertions of Sec. 2 follow from the public-label requirement on network messages, not from embedding the goal into the label definition. Citations to DY* supply design lineage (trace + effectful primitives) by a disjoint author set and are not used as uniqueness theorems that force the new results. The liveness theorem states its external assumptions (hlpunish, hlminer, htime_budget, single-chain reconstruction) explicitly and does not claim to derive them. No fitted parameters, no self-definitional loop, no renaming of a known empirical pattern. The derivation chain is self-contained against the stated symbolic model.

Axiom & Free-Parameter Ledger

0 free parameters · 5 axioms · 2 invented entities

The central claims rest on the standard Dolev-Yao symbolic model, the monotonicity of labels and events, the single-chain reconstruction of the blockchain from the trace, and the two external liveness hypotheses used for punishment. No numeric free parameters are fitted; the invented entities are the library constructs themselves, which are given independent evidence by the machine-checked theorems.

axioms (5)
  • domain assumption Dolev-Yao adversary that can apply any constructor/destructor to known terms and that never forgets public data (AttackerKnows inductive predicate).
    Standard symbolic model used throughout Sec. 3.1.2; every confidentiality claim is relative to this adversary.
  • domain assumption Labels and validity predicates are monotone with respect to trace extension (corruption and events are permanent).
    Required for the security lattice and for valid_trace preservation; stated explicitly in Sec. 3.1.1 and 3.1.3.
  • ad hoc to paper A single canonical blockchain is recovered by filtering MsgSent events that parse as blocks (List.get_blockchain).
    Modeling choice in Sec. 4.1.1 that collapses consensus forks; used by every on-chain safety and liveness statement.
  • domain assumption Participant liveness of the defense exchange within punish_time blocks and miner liveness that includes any ValidLongEnough transaction within miner_time blocks.
    External hypotheses of Theorem punish.eventually_on_chain (Listing 3); without them the punishment guarantee does not hold.
  • ad hoc to paper Script semantics are given by a decidable eval predicate of the Script type class rather than a full Bitcoin VM.
    Abstraction introduced in Sec. 4.1.2; all transaction-validity lemmas are relative to this interface.
invented entities (2)
  • Conditional-swap / releasable secrecy labels and the meet/join lattice over trace properties independent evidence
    purpose: Express recursive conditional secrecy for XOR and event-triggered release of revocation keys.
    Defined in Sec. 2 and 3.1.3; independent evidence is the type-system soundness theorem and the payment-channel proofs that use them.
  • LeanDY exchange DSL and the valid_exchange / transition_valid infrastructure independent evidence
    purpose: Give a uniform interface for protocol steps that can be type-checked automatically or proved interactively.
    Core of Sec. 3.2; independent evidence is the machine-checked preservation theorems.

pith-pipeline@v1.1.0-grok45 · 36737 in / 2782 out tokens · 27453 ms · 2026-07-12T02:42:20.075541+00:00 · methodology

0 comments
Cite this review

Pith. "Pith review of LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean." pith.science (2026). https://pith.science/paper/RSM7RCJY

@misc{pith2026260703406,
  author       = {Pith},
  title        = {Pith review of: LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/RSM7RCJY}},
  note         = {Machine review of arXiv:2607.03406}
}
Share X Bluesky LinkedIn Reddit HN
read the original abstract

Computer-aided formal verification is a widely used approach for the symbolic analysis of cryptographic protocols. However, many modern protocols rely on features that remain challenging for existing techniques. In particular, reasoning about state, time-dependent behavior, inductively defined data structures, unbounded executions, and conditional secrecy requires a level of expressiveness that is difficult to reconcile with effective automation. As a result, protocol verification has largely followed two disjoint paths: fully automated methods with limited expressiveness, or interactive proofs in general-purpose theorem provers that offer flexibility but only limited, non-specialized automation. We present an orthogonal approach that bridges this gap by combining compositional type-based reasoning with trace-based reasoning, enabling modular verification of stateful and unbounded protocols. Guided by the language-and-automation co-design (LAC) principle, our approach delivers protocol-specific automation while retaining high expressiveness. We implement this framework as the LeanDY library for the Lean proof assistant, building on and extending the design of DY*, and combining protocol-specific automation with interactive proofs. Our framework supports, in a unified setting, a broad class of functional and security requirements, including secrecy and authentication for stateful protocols, as well as recursive conditional secrecy for protocols using XOR. We formalize SegWit-style blockchain primitives in LeanDY and demonstrate its expressiveness by carrying out an in-depth formalization of payment channels on top of this blockchain model, verifying punishment mechanisms and properties that depend on chain liveness.

Figures

Figures reproduced from arXiv: 2607.03406 by Lorenzo Veronese, Magdalena Solitro, Matteo Maffei, Simon Jeanteur.

Figure 1
Figure 1. Figure 1: Conditional release protocol with two intermedi [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Typing rules for confidentiality labels. [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Core rules defining valid_bytes(). 4 u_sym_enc_pred : LabelingEnv 𝛼 𝜂 → 𝛼 → (m k : B 𝛼 𝜂) → T 𝛼 𝜂 → Prop 5 u_asym_enc_pred : LabelingEnv 𝛼 𝜂 → 𝛼 → (m k : B 𝛼 𝜂) → T 𝛼 𝜂 → Prop 6 . . . −− proofs of monotonicity Each field specifies protocol-specific restrictions on honest cryp￾tographic uses; for example, a protocol may allow signing only messages of a particular shape or only after a specific event has occ… view at source ↗
Figure 4
Figure 4. Figure 4: Selected derived rules for destructors and tuples. [PITH_FULL_IMAGE:figures/full_fig_p009_4.png] view at source ↗
Figure 6
Figure 6. Figure 6: Diagram of the flow of money of 𝑡𝑥𝑛 𝐴→𝐵 . in Sec. 4.1.2. Overall, the scripts under consideration are of type P2WSH Script, with Script structured as follows: 1 inductive Script where 2 | CommonFundS (s : CommonFund) −− funding output 3 | ToRemoteS (s : ToRemote) −− remote commitment output 4 | ToLocalS (s : ToLocal) −− delayed / punishable output 5 | . . . We explore each of these scripts, showcasing the … view at source ↗
Figure 5
Figure 5. Figure 5: High-level flow of the modeled payment-channel [PITH_FULL_IMAGE:figures/full_fig_p013_5.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

61 extracted references · 17 canonical work pages

  1. [1]

    Martín Abadi and Cédric Fournet. 2001. Mobile Values, New Names, and Secure Communication. InProceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(London, United Kingdom, 2001)(Popl ’01). Association for Computing Machinery, New York, NY, USA, 104–115. doi:10. 1145/360204.360213

    arXiv 2001

  2. [2]

    2011-10, 2011

    Gavin Andresen. 2011-10, 2011. BIP 11: M-of-N Standard Transactions. https: //github.com/bitcoin/bips/blob/master/bip-0011.mediawiki

    2011

  3. [3]

    Marcin Andrychowicz, Stefan Dziembowski, Daniel Malinowski, and Ł ukasz Mazurek. 2014. Modeling Bitcoin Contracts by Timed Automata. InFormal Modeling and Analysis of Timed Systems(Cham, 2014), Axel Legay and Marius Bozga (Eds.). Springer International Publishing, 7–22. doi:10.1007/978-3-319- 10512-3_2

    doi:10.1007/978-3-319- 2014

  4. [4]

    Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters. 2020. ConCert: A Smart Contract Certification Framework in Coq. InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs(New York, NY, USA, 2020-01-22)(CPP 2020). Association for Computing Machinery, 215–228. doi:10.1145/3372885.3373829

    doi:10.1145/3372885.3373829 2020

  5. [5]

    Michael Backes, Căt˘ alin Hri ¸tcu, and Matteo Maffei. 2014. Union, Intersection and Refinement Types and Reasoning about Type Disjoint- ness for Secure Protocol Implementations. 22, 2 (2014), 301–353. arXiv:https://journals.sagepub.com/doi/pdf/10.3233/JCS-130493 doi:10.3233/JCS- 130493

    work page doi:10.3233/jcs-130493 2014

  6. [6]

    Gilles Barthe, Ugo Dal Lago, Giulio Malavolta, and Itsaka Rakotonirina. 2022. Tidy: Symbolic Verification of Timed Cryptographic Protocols. InProceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (Los Angeles CA USA, 2022-11-07). ACM, 263–276. doi:10.1145/3548606.3559343

    doi:10.1145/3548606.3559343 2022

  7. [7]

    Giampaolo Bella and Lawrence C. Paulson. 1998. Kerberos Version IV: Inductive Analysis of the Secrecy Goals. InComputer Security — ESORICS 98(1998), Jean- Jacques Quisquater, Yves Deswarte, Catherine Meadows, and Dieter Gollmann (Eds.). Springer Berlin Heidelberg, 361–375

    1998

  8. [8]

    Gordon, and Sergio Maffeis

    Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, and Sergio Maffeis. 2011. Refinement Types for Secure Implementations. 33, 2, Article 8 (2011). doi:10.1145/1890028.1890031

    work page doi:10.1145/1890028.1890031 2011

  9. [9]

    Johan Bengtsson, Kim Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi

  10. [10]

    In Hybrid Systems III(Berlin, Heidelberg, 1996), Rajeev Alur, Thomas A

    UPPAAL — a Tool Suite for Automatic Verification of Real-Time Systems. In Hybrid Systems III(Berlin, Heidelberg, 1996), Rajeev Alur, Thomas A. Henzinger, and Eduardo D. Sontag (Eds.). Springer, 232–243. doi:10.1007/BFb0020949

    work page doi:10.1007/bfb0020949 1996

  11. [11]

    Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, and Tim Würtele. 2021. DY★: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code. In2021 IEEE European Symposium on Security and Privacy (EuroS&P)(2021). 523–542. doi:10.1109/EuroSP51992.2021.00042

    doi:10.1109/eurosp51992.2021.00042 2021

  12. [12]

    Gordon, and Riccardo Pu- cella

    Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, and Riccardo Pu- cella. 2004. TulaFale: A Security Tool for Web Services. InFormal Methods for Components and Objects(Berlin, Heidelberg, 2004), Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever (Eds.). Springer, 197–222. doi:10.1007/978-3-540-30101-1_9

    work page doi:10.1007/978-3-540-30101-1_9 2004

  13. [13]

    Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, and Santiago Zanella-Béguelin. 2014. Proving the TLS Hand- shake Secure (As It Is). InAdvances in Cryptology – CRYPTO 2014(2014). Springer, Berlin, Heidelberg, 235–255. doi:10.1007/978-3-662-44381-1_14

    work page doi:10.1007/978-3-662-44381-1_14 2014

  14. [14]

    Bruno Blanchet. 2001. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In14th IEEE Computer Security Foundations Workshop (CSFW-14) (Cape Breton, Nova Scotia, Canada, 2001-06). IEEE Computer Society, 82–96. doi:10.1109/CSFW.2001.930138

    doi:10.1109/csfw.2001.930138 2001

  15. [15]

    Bruno Blanchet, Vincent Cheval, and Véronique Cortier. 2022. ProVerif with Lemmas, Induction, Fast Subsumption, and Much More. In2022 IEEE Symposium on Security and Privacy (SP)(2022-05). 69–86. doi:10.1109/SP46214.2022.9833653

    doi:10.1109/sp46214.2022.9833653 2022

  16. [16]

    Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. 2013. Extending Sledgehammer with SMT Solvers. 51, 1 (2013), 109–128. doi:10.1007/ s10817-013-9278-5

    2013

  17. [17]

    Fran¸cois Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich

  18. [18]

    InBoogie 2011: First International Workshop on Intermediate Verification Languages(Wroclaw, Poland, 2011)

    Why3: Shepherd Your Herd of Provers. InBoogie 2011: First International Workshop on Intermediate Verification Languages(Wroclaw, Poland, 2011). 53–64. https://inria.hal.science/hal-00790310

    2011

  19. [19]

    Colin Boyd, Kristian Gjø steen, and Shuang Wu. 2020. A Blockchain Model in Tamarin and Formal Analysis of Hash Time Lock Contract. In2nd Work- shop on Formal Methods for Blockchains (FMBC 2020)(Dagstuhl, Germany, 2020) (Open Access Series in Informatics (OASIcs), Vol. 84), Bruno Bernardo and Diego Marmsoler (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für I...

    work page doi:10.4230/oasics.fmbc.2020.5 2020

  20. [20]

    Lea Salome Brugger, Laura Kovács, Anja Petkovic Komel, Sophie Rain, and Michael Rawson. 2023. CheckMate: Automated Game-Theoretic Security Rea- soning. InProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security(New York, NY, USA, 2023-11-21)(CCS ’23). Associa- tion for Computing Machinery, 1407–1421. doi:10.1145/3576915.3623183

    doi:10.1145/3576915.3623183 2023

  21. [21]

    Matteo Busi, Riccardo Focardi, and Flaminia L. Luccio. 2025. Strands Rocq: Why Is a Security Protocol Correct, Mechanically?. In2025 IEEE 38th Computer Security Foundations Symposium (CSF)(2025). 33–48. doi:10.1109/CSF64896.2025.00022

    doi:10.1109/csf64896.2025.00022 2025

  22. [22]

    Vincent Cheval and Bruno Blanchet. 2013. Proving More Observational Equiv- alences with ProVerif. InLecture Notes in Computer Science. Springer Berlin Heidelberg, 226–246. doi:10.1007/978-3-642-36830-1_12 17 Jeanteur et al

    work page doi:10.1007/978-3-642-36830-1_12 2013

  23. [23]

    Vincent Cheval and Caroline Fontaine. 2025. Automatic Verification of Finite Variant Property Beyond Convergent Equational Theories. In2025 IEEE 38th Computer Security Foundations Symposium (CSF)(2025-06). 521–536. doi:10.1109/ CSF64896.2025.00005

    arXiv 2025

  24. [24]

    Vincent Cheval, Charlie Jacomme, Steve Kremer, and Robert Künnemann. 2022. {SAPIC+}: Protocol Verifiers of the World, Unite! 3935–3952. https://www.usenix. org/conference/usenixsecurity22/presentation/cheval

    2022

  25. [25]

    2025.The Lean Reference Manual: The Grind Tactic

    Leonardo de Moura. 2025.The Lean Reference Manual: The Grind Tactic. https: //lean-lang.org/doc/reference/latest/The--grind--tactic/

    2025

  26. [26]

    Dolev and A

    D. Dolev and A. Yao. 1983. On the Security of Public Key Protocols. 29, 2 (1983), 198–208. doi:10.1109/TIT.1983.1056650

    doi:10.1109/tit.1983.1056650 1983

  27. [27]

    Jannik Dreier, Lucca Hirschi, Sasa Radomirovic, and Ralf Sasse. 2018. Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive Or. In2018 IEEE 31st Computer Security Foundations Symposium (CSF)(2018). 359–373. doi:10.1109/CSF.2018.00033

    doi:10.1109/csf.2018.00033 2018

  28. [28]

    Grzegorz Fabiański, Rafał Stefański, and Orfeas Stefanos Thyfronitis Litos. 2026. A Formally Verified Lightning Network. InFinancial Cryptography and Data Security(Cham, 2026), Christina Garman and Pedro Moreno-Sanchez (Eds.). Springer Nature Switzerland, 3–20. doi:10.1007/978-3-032-07024-1_1

    work page doi:10.1007/978-3-032-07024-1_1 2026

  29. [29]

    Javier Thayer Fábrega, Jonathan C

    F. Javier Thayer Fábrega, Jonathan C. Herzog, and Joshua D. Guttman. 1999. Strand Spaces: Proving Security Protocols Correct. 7, 2–3 (1999), 191–230. doi:10. 3233/JCS-1999-72-304

    1999

  30. [30]

    Matthias Grundmann and Hannes Hartenstein. 2026. Security of the Lightning Network: Model Checking a Stepwise Refinement with TLA+. InIntegrated For- mal Methods(Cham, 2026), Ferruccio Damiani and Marie Farrell (Eds.). Springer Nature Switzerland, 313–335

    2026

  31. [31]

    Hans Hüttel and Vilim Staroveski. 2020. Secrecy and Authenticity Properties of the Lightning Network Protocol:. InProceedings of the 6th International Conference on Information Systems Security and Privacy(Valletta, Malta, 2020). SCITEPRESS - Science and Technology Publications, 119–130. doi:10.5220/0008974801190130

    work page doi:10.5220/0008974801190130 2020

  32. [32]

    Hans Hüttel and Vilim Staroveˇ ski. 2022. Key Agreement in the Lightning Network Protocol. InInformation Systems Security and Privacy(Cham, 2022), Steven Furnell, Paolo Mori, Edgar Weippl, and Olivier Camp (Eds.). Springer International Publishing, 139–155. doi:10.1007/978-3-030-94900-6_7

    work page doi:10.1007/978-3-030-94900-6_7 2022

  33. [33]

    Vincent Jacquot and Benoît Donnet. 2023. CHAUSSETTE: A Symbolic Verifica- tion of Bitcoin Scripts. Springer. https://orbi.uliege.be/handle/2268/305862

    2023

  34. [34]

    Simon Jeanteur, Lorenzo Veronese, Magdalena Solitro, and Matteo Maffei. 2026. LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean. https://github.com/SecPriv/leandy

    2026

  35. [35]

    H. Kleisli. 1965. Every Standard Construction Is Induced by a Pair of Adjoint Functors. 16, 3 (1965), 544–546. jstor:2034693 doi:10.2307/2034693

    work page doi:10.2307/2034693 1965

  36. [36]

    Nadim Kobeissi, Georgio Nicolas, and Karthikeyan Bhargavan. 2019. Noise Ex- plorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols. In2019 IEEE European Symposium on Security and Privacy (EuroS&P)(2019). 356–370. doi:10.1109/EuroSP.2019.00034

    doi:10.1109/eurosp.2019.00034 2019

  37. [37]

    Ralf Küsters and Tomasz Truderung. 2008. Reducing Protocol Analysis with XOR to the XOR-free Case in the Horn Theory Based Approach. InProceedings of the 15th ACM Conference on Computer and Communications Security(Alexandria, Virginia, USA, 2008)(Ccs ’08). Association for Computing Machinery, New York, NY, USA, 129–138. doi:10.1145/1455770.1455788

    doi:10.1145/1455770.1455788 2008

  38. [38]

    2016-01, 2016

    Johnson Lau and Pieter Wuille. 2016-01, 2016. BIP 143: Transaction Signature Verification for Version 0 Witness Program. https://github.com/bitcoin/bips/ blob/master/bip-0143.mediawiki

    2016

  39. [39]

    Jannis Limperg and Asta Halkjæ r From. 2023. Aesop: White-Box Best-First Proof Search for Lean. InProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs(New York, NY, USA, 2023-01-11)(CPP 2023). Association for Computing Machinery, 253–266. doi:10.1145/3573105.3575671

    doi:10.1145/3573105.3575671 2023

  40. [40]

    Benjamin Lipp, Bruno Blanchet, and Karthikeyan Bhargavan. 2019. A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol. In2019 IEEE European Symposium on Security and Privacy (EuroS&P)(2019-06). 231–246. doi:10.1109/EuroSP.2019.00026

    doi:10.1109/eurosp.2019.00026 2019

  41. [41]

    2015-12, 2015

    Eric Lombrozo, Johnson Lau, and Pieter Wuille. 2015-12, 2015. BIP 141: Segregated Witness (Consensus Layer). https://github.com/bitcoin/bips/blob/master/bip- 0141.mediawiki

    2015

  42. [42]

    Eric Lombrozo and Pieter Wuille. 2016. BIP 144: Segregated Witness (Peer Services). https://github.com/bitcoin/bips/blob/master/bip-0144.mediawiki

    2016

  43. [43]

    Giulio Malavolta, Pedro Moreno-Sanchez, Aniket Kate, Matteo Maffei, and Sri- vatsan Ravi. 2017. Concurrency and Privacy with Payment-Channel Networks. InProceedings of the 2017 ACM SIGSAC Conference on Computer and Communi- cations Security(Dallas, Texas, USA, 2017)(Ccs ’17). Association for Computing Machinery, New York, NY, USA, 455–471. doi:10.1145/313...

    work page doi:10.1145/3133956.3134096 2017

  44. [44]

    Nikos Mavrogiannopoulos, Frederik Vercauteren, Vesselin Velichkov, and Bart Preneel. 2012. A Cross-Protocol Attack on the TLS Protocol. InProceedings of the 2012 ACM Conference on Computer and Communications Security(New York, NY, USA, 2012-10-16)(CCS ’12). Association for Computing Machinery, 62–72. doi:10.1145/2382196.2382206

    doi:10.1145/2382196.2382206 2012

  45. [45]

    Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin. 2013. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. InComputer Aided Verification(Berlin, Heidelberg, 2013)(Lecture Notes in Computer Science), Natasha Sharygina and Helmut Veith (Eds.). Springer, 696–701. doi:10.1007/978- 3-642-39799-8_48

    doi:10.1007/978- 2013

  46. [46]

    Paulson, and Markus Wenzel

    Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002.Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, Vol. 2283. Springer. doi:10.1007/3-540-45949-9

    doi:10.1007/3-540-45949-9 2002

  47. [47]

    Kenneth G Paterson, Matteo Scarlata, and Kien Tuong Truong. [n. d.]. Three Lessons From Threema: Analysis of a Secure Messenger. ([n. d.])

  48. [48]

    Lawrence C. Paulson. 1998. The Inductive Approach to Verifying Cryptographic Protocols. 6, 1–2 (1998), 85–128. doi:10.3233/JCS-1998-61-205

    work page doi:10.3233/jcs-1998-61-205 1998

  49. [49]

    Joseph Poon and Thaddeus Dryja. 2016. The Bitcoin Lightning Network: Scalable off-Chain Instant Payments

    2016

  50. [50]

    Sophie Rain, Georgia Avarikioti, Laura Kovács, and Matteo Maffei. 2023. Towards a Game-Theoretic Security Analysis of Off-Chain Protocols. In2023 IEEE 36th Computer Security Foundations Symposium (CSF)(2023-07). 107–122. doi:10.1109/ CSF57540.2023.00003

    arXiv 2023

  51. [51]

    Daniel Ricketts, Valentin Robert, Dongseok Jang, Zachary Tatlock, and Sorin Lerner. 2014. Automating Formal Proofs for Reactive Systems. InProceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Imple- mentation(Edinburgh, United Kingdom, 2014)(Pldi ’14). Association for Com- puting Machinery, New York, NY, USA, 452–462. doi:10.1...

    doi:10.1145/2594291.2594338 2014

  52. [52]

    Kristijan Rupić, Lovro Roˇ zić, and Ante Derek. 2020. Mechanized Formal Model of Bitcoin’s Blockchain Validation Procedures. In2nd Workshop on For- mal Methods for Blockchains (FMBC 2020)(Dagstuhl, Germany, 2020)(Open Access Series in Informatics (OASIcs), Vol. 84), Bruno Bernardo and Diego Marm- soler (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Inform...

    work page doi:10.4230/oasics.fmbc.2020.7 2020

  53. [53]

    Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhar- gavan, and Jean Yang. 2011. Secure Distributed Programming with Value- Dependent Types. InProceedings of the 16th ACM SIGPLAN International Con- ference on Functional Programming(Tokyo, Japan, 2011)(Icfp ’11). Association for Computing Machinery, New York, NY, USA, 266–278. doi:...

    work page doi:10.1145/2034773 2011

  54. [54]

    Nikhil Swamy, Căt˘ alin Hri¸tcu, Chantal Keller, Aseem Rastogi, Antoine Delignat- Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella-Béguelin

  55. [55]

    InProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(St

    Dependent Types and Multi-Monadic Effects in F*. InProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(St. Petersburg FL USA, 2016-01-11). ACM, 256–270. doi:10.1145/ 2837614.2837655

    arXiv 2016

  56. [56]

    Théophile Wallez. 2025. A Verification Framework for Secure Group Messaging. https://hal.science/tel-05455122

    2025

  57. [57]

    2026.DY* Unchained: Now with Composable Security Proofs and Precise Compromise Scenarios

    Théophile Wallez. 2026.DY* Unchained: Now with Composable Security Proofs and Precise Compromise Scenarios. https://eprint.iacr.org/2026/830

    2026

  58. [58]

    Théophile Wallez, Jonathan Protzenko, Benjamin Beurdouche, and Karthikeyan Bhargavan. 2023. TreeSync: Authenticated Group Management for Messaging Layer Security. 1217–1233

    2023

  59. [59]

    Théophile Wallez, Jonathan Protzenko, and Karthikeyan Bhargavan. 2023. Com- parse: Provably Secure Formats for Cryptographic Protocols. InProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (Copenhagen, Denmark, 2023)(Ccs ’23). Association for Computing Machinery, New York, NY, USA, 564–578. doi:10.1145/3576915.3623201

    work page doi:10.1145/3576915.3623201 2023

  60. [60]

    Woo and S.S

    T.Y.C. Woo and S.S. Lam. 1993. A Semantic Model for Authentication Protocols. InProceedings 1993 IEEE Computer Society Symposium on Research in Security and Privacy(1993). 178–194. doi:10.1109/RISP.1993.287633

    work page doi:10.1109/risp.1993.287633 1993

  61. [61]

    2012-02, 2012

    Pieter Wuille. 2012-02, 2012. BIP 30: Duplicate Transactions. https://github.com/ bitcoin/bips/blob/master/bip-0030.mediawiki 18

    2012