Analysis of Certificate Transparency using Probabilistic Verification

公钥证书对互联网安全至关重要，因为它们可以帮助用户知道哪些网站已经过适当的身份验证。然而，有报道称，应该受到信任的第三方错误地颁发了证书。这导致他们在中间人袭击中被剥削，造成了毁灭性的后果。为了改进对已颁发证书的审计，提出的一个想法是将它们提交给一个公共的、仅附加的日志，任何人都可以查看。这是称为证书透明度的开放框架的一部分。然而，该系统的一个问题是，可以使一部分用户独占地联系包含欺诈性证书的“假”日志。为了防止这种情况，整个网络上的客户端可以相互八卦，并验证他们看到的是不是相同版本的日志。像Chuat等人这样的研究人员设计了八卦协议，每当发现日志中的不当行为时，就会传播信息。目前尚不清楚这些协议在检测攻击方面的有效性。对于这个研究项目，我们希望应用概率模型检查来分析这些协议的行为方式，并寻找潜在的弱点。我们还寻求提出任何建议，以改进这些协议的性能和可检测性。最后，我们将把我们的方法应用于其他使用八卦协议的系统，以帮助用户验证其他透明日志的一致性。

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.