Quantitative verification of gossip protocols for certificate transparency

Oxford, Michael ORCID: 0000-0001-7033-8902 (2021). Quantitative verification of gossip protocols for certificate transparency. University of Birmingham. Ph.D.

Text - Accepted Version
Available under License Creative Commons Attribution.

Download (9MB) | Preview


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.

Type of Work: Thesis (Doctorates > Ph.D.)
Award Type: Doctorates > Ph.D.
Parker, Davidd.a.parker@bham.ac.ukorcid.org/0000-0003-4137-8862
Mark, Ryanm.d.ryan@bham.ac.ukUNSPECIFIED
Licence: Creative Commons: Attribution 4.0
College/Faculty: Colleges (2008 onwards) > College of Engineering & Physical Sciences
School or Department: School of Computer Science
Funders: Engineering and Physical Sciences Research Council
Subjects: Q Science > Q Science (General)
Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Q Science > QA Mathematics > QA76 Computer software
URI: http://etheses.bham.ac.uk/id/eprint/11578


Request a Correction Request a Correction
View Item View Item


Downloads per month over past year