Analysis of Certificate Transparency using Probabilistic Verification
Lead Research Organisation:
University of Birmingham
Department Name: School of Computer Science
Abstract
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.
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.
Organisations
People |
ORCID iD |
| David Parker (Primary Supervisor) | |
| Michael Oxford (Student) |
Publications
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 | 30/09/2016 | 25/12/2019 | Michael 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. 1st FEBRUARY 2021 - PhD candidate submitted the thesis "Quantitative Verification of Gossip Protocols for Certificate Transparency" on the 18th December 2020 (awaiting viva). It contains chapters on how to model the CT gossip protocols are modelled, resolving uncertainty and scalability issues embedded within the probabilistic models by extending them with real-valued intervals and abstraction. We also apply Python libraries from machine learning to search over model parameters (e.g. client behaviour probabilities and their respective initial states) to find worst-case scenarios where the protocol performance may perform badly in. |
| 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 open problems in cyber security. |
| Sectors | Digital/Communication/Information Technologies (including Software) |
| URL | https://ieeexplore.ieee.org/abstract/document/9162197 |