On computer-assisted verification of privacy related properties

在互联网上，有许多服务和协议应该提供隐私。通过扩展计算机辅助匿名性证明技术，提出了一种新的证明隐私相关属性的方法。具体来说，我们形式化了receipt-freeness属性，这是电子投票的隐私相关属性，是匿名性的扩展，我们证明了Lee等人的电子投票协议是receipt-free的。此外，我们还正式描述了Crowds协议。Crowds是一种用于网络访问的通信系统，可以保护发送者的隐私。在这项研究中，发送者的隐私进行了计算机辅助证明，并在一个形式化的规范语言描述的扩展人群，这是为了保护接收者的隐私。最后，本研究描述了Alloy中两个系统的迹等价的充分条件，这使得隐私相关属性的全自动证明成为可能。

On the Internet, there are many services and protocols where privacy should be provided. By extending a computer-assisted proof technique for anonymity, this study developed a new method to prove privacy related properties. Specifically, we formalized the receipt-freeness property, which is a privacy-related property for electronic voting and is an extension of anonymity, and we proved that an electronic voting protocol by Lee et al. is receipt-free. Also, we described the Crowds protocol formally. Crowds is a communication system for a web access that preserves the sender's privacy. In this study, a computer-assisted proof for the sender's privacy is conducted, and an extension of Crowds which is for preserving the recipient's privacy is described in a formal specification language. Finally, this study described a sufficient condition for a trace equivalence of two systems in Alloy, which enables a fully automatic proof of privacy related properties.