Abstract. Certificate transparency is a promising solution to publicly auditing Internet certificates. However, there is the potential of split-world attacks, where users are directed to fake versions of the log where they may accept fraudulent certificates. To ensure users are seeing the same version of a log, gossip protocols have been designed where users share and verify log-generated data. This thesis proposes a methodology of evaluating such protocols using probabilistic model checking, a collection of techniques for formally verifying properties of stochastic systems. It also describes the approach to modelling and verifying the protocols and analysing several aspects, including the success rate of detecting inconsistencies in gossip messages and its efficiency in terms of bandwidth. This thesis also compares different protocol variants and suggests ways to augment the protocol to improve performances, using model checking to verify the claims. To address uncertainty and unscalability issues within the models, this thesis shows how to transform models by allowing the probability of certain events to lie within a range of values, and abstract them to make the verification process more efficient. Lastly, by parameterising the models, this thesis shows how to search possible model configurations to find the worst-case behaviour for certain formal properties.