  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.
