|
近年ＩＣＴ社会において，プライバシ保護の必要性が強く叫ばれている．本研究では，従来より提案されていた「匿名性」の論理的な定義とその検証法を用いて，さまざまなプライバシ関連の性質を証明する手法を明らかにした．具体的には，「無証拠性」と呼ばれる，電子投票の秘密を守るための条件を匿名性として定式化し，Ｌｅｅらの電子投票プロトコルの無証拠性の証明に応用した．また，Ｃｒｏｗｄｓと呼ばれる秘密通信路の分散実装（および，その拡張）を形式的に記述し，その正しさを示した．さらには，プライバシを示す上で必要になるトレース一致と呼ぶ条件を，Ａｌｌｏｙと呼ばれる全自動の検証器を用いて検証する手法について明らかにした．
|
