On computer-assisted verification of privacy related properties

点击翻译按钮获取中文摘要

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.