Analysis of Certificate Transparency using Probabilistic Verification

Lead Research Organisation: University of Birmingham
Department Name: School of Computer Science


Public key certificates are vital for internet security as they help users know which websites have been properly authenticated. However, there have been reports of certificates being issued incorrectly by supposedly trusted third parties. This led to them being exploited in man-in-the-middle attacks with devastating results.

To improve the auditing of issued certificates, one idea proposed is to have them be submitted to a public, append-only log that anybody can view. This is part of an open framework called certificate transparency. However, a problem with this system is that a subset of users can be made to exclusively contact a `fake' log that contains fraudulent certificates. To prevent this, clients across the network could be made to gossip with each other and verify if they are seeing the same version of the log.

Researchers such as Chuat et al have designed gossip protocols which disseminate information whenever misbehaviour from the log is noticed. At present it is not known how effective these protocols are in detecting attacks. For this research project, we would like to apply probabilistic model checking to analyse how these protocols behave and look for potential weaknesses. We also seek to propose any recommendations to improve the performance and detectability of these protocols. Finally, we will apply our methods to other systems that use gossip protocols to help users verify consistency for other transparency logs.


10 25 50

Studentship Projects

Project Reference Relationship Related To Start End Student Name
EP/N509590/1 01/10/2016 30/09/2021
1832982 Studentship EP/N509590/1 01/10/2016 25/12/2019 Michael Colin Oxford
Description So far, we have fully described a methodology which allows us to mathematically analyse the behaviour of certain gossip protocols used for certificate transparency (CT) in a client/server network topology. The metrics we are able to measure using our approach includes the expected proportion of clients to be gossiped newly generated data sourced from a CT log per gossip round, the expected cumulative amount of log connections made as part of the protocol logic and the success rate of detecting a simple "split-world" attack (i.e. two different parties have different views of the CT log). Furthermore, we have shown a way how to improve the protocol performance and demonstrated it via model checking.

4th FEBRUARY 2020 - We have collated our findings into a draft paper that we hope to submit to a conference or workshop in the near future. Following on from the initial work, we noticed a problem of not taking into account any margin of error in the probabilities we initially used in our models. To correct this, we have developed a way of searching through a parameter space that describes all potential models to find a worst-case result for our properties, taking it as evidence of what the results may be for all cases.
Exploitation Route We hope that our findings and recommendations will be taken into consideration by CT gossip developers. We also want to demonstrate how it can be possible to apply probabilistic verification to problems in cyber security.
Sectors Digital/Communication/Information Technologies (including Software)