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.