Interactive verification of Markov chains: Two distributed protocol case studies

Johannes Hölzl
(Technische Universität München)
Tobias Nipkow
(Technische Universität München)

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.

In Uli Fahrenberg, Axel Legay and Claus Thrane: Proceedings Quantities in Formal Methods (QFM 2012), Paris, France, 28 August 2012, Electronic Proceedings in Theoretical Computer Science 103, pp. 17–31.
Published: 14th December 2012.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: