2013 Fiscal Year Final Research Report
On computer-assisted verification of privacy related properties
| Project/Area Number |
23700024
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Aichi Institute of Technology |
|---|
Principal Investigator |
|
|---|
| Project Period (FY) |
2011 – 2013
|
| Keywords | プライバシ / 形式手法 / 検証 / 定理証明 / 無証拠性 / Crowds / セキュリティプロトコル |
|---|
| Research Abstract |
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.
|
