| 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
|
| Project Status |
Completed (Fiscal Year 2013)
|
| Budget Amount *help |
¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
Fiscal Year 2013: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2012: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2011: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
|
|---|
| 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.
|
