Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security(…)
summary
Proposes a EHL + pRHL hopping rule that reduces expectation-based proof goals to related programs, implements it inside EasyCrypt integration, and proves soundness and relative completeness for a core language with procedures and adversarial code. Mechanized proofs show the expected linear cost of randomized quickselect and a full mechanized skiplist proof for average-case bounds. Artifacts are available and evaluated, and the approach supports cryptographic game style adversaries and library-style abstractions that transfer proofs between abstract and concrete implementations.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:24Framework design principles
- 4:13Expectation-based Hoare logic
- 7:49Meta-theory and Ecrypt integration
- 9:13Quickselect analysis
- 13:48Relational probabilistic logic
- 15:35Skip lists example
- 16:42Cryptographic applications
- 17:46Q&A
related talks
39mKeynote: Towards High-Assurance Cryptographic Software
08mShort Talk: Generalising secure compilation criteria
19mA quantitative probabilistic relational Hoare logic
20mFSLH: Flexible Mechanized Speculative Load Hardening
28mProving Obliviousness of Probabilistic Algorithms with Formal Verification
20mHyper Hoare Logic: (Dis-)Proving Program Hyperproperties
41mGKR based Zero-Knowledge Proofs
31mSequential Composition of Rational Proofs