Interactive verification of Markov chains: Two distributed protocol case studies
Johannes H\"olzl (Technische Universit\"at M\"unchen), Tobias Nipkow, (Technische Universit\"at M\"unchen)
TL;DR
This paper demonstrates how to verify properties of probabilistic protocols of arbitrary size using interactive proof assistants, through detailed case studies of ZeroConf and Crowds protocols.
Contribution
It introduces a method for verifying probabilistic protocols of any size using Isabelle/HOL, illustrated with two comprehensive case studies.
Findings
Verified ZeroConf protocol properties
Analyzed anonymity in Crowds protocol
Showed feasibility of interactive probabilistic verification
Abstract
Probabilistic model checkers like PRISM only check probabilistic systems of a fixed size. To guarantee the desired properties for an arbitrary size, mathematical analysis is necessary. We show for two case studies how this can be done in the interactive proof assistant Isabelle/HOL. The first case study is a detailed description of how we verified properties of the ZeroConf protocol, a decentral address allocation protocol. The second case study shows the more involved verification of anonymity properties of the Crowds protocol, an anonymizing protocol.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.