Part III：新領域の開拓

特集

フォーマルメソッドの新潮流

6

匿名性とプライバシのためのフォーマルメソッド
真野

匿名性・プライバシって何だろう？

日本電信電話（株）

健 ● NTT コミュニケーション科学基礎研究所
定式化という問題が解決したかといえば，かならずしもそうとは言えない．たとえば前者の研究では，プライバインターネットを利用してショッピングをしたり，オシを通信の送信者と受信者の関係として捉えているのだークションに参加したり，あるいは掲示版に書き込みをが，そのような図式に当てはまらないプライバシの例はしたりする場合，そのことによって自分にかかわる情報，いくらでも挙げることができる．

いわゆる個人情報やプライバシといったものが危険にさフォーマルメソッドのための匿名性・プライバシの定らされないかどうかを気にする人も多いだろう．情報通式化は，フォーマルであることはもちろんだが，さらに信技術の発展に伴い，ネットワークを介して我々の重要一般性があるということも求められる．ここで一般性とな情報がやりとりされる機会は増加している．もちろん，は，ショッピングや掲示版といった個別具体的な事例・個人情報保護法などの法整備によって不必要な情報の保状況に依存しないという意味である．一般性のあるメソ管・流通は避けられる傾向にあるが，それがどうしてもッドを構築するには，まず問題の定式化自体に一般性が必要な場面では，いかにして匿名性・プライバシを保護なくてはならないことは明らかだろう．しかし，そのよするか，そして，正しく保護されていることをどうやっうな定式化が本当に可能だろうか？て確認するかは重要な問題だ．本特集のテーマであるフ

そもそもそれらの日常的な意味も，人により場合によォーマルメソッドは，そのような問題に対する抜本的なり，微妙にしかし確実に違っているように見える．たと解決となり得る技術の 1 つである．

えば，“ 匿名性とプライバシ ” とひとくちに言うが，両では，フォーマルメソッドでシステムの匿名性やプラ者はどういう関係にあるのか？

匿名性はプライバシのイバシを検証するためには何が必要だろうか．数理論理

一部だ，と考える人は多いかもしれない．また，“ ネッ学という理論的基礎，そしてモデル検査器や定理証明器

トワークの匿名性とプライバシ ” などといった場合には，などの検証支援のツールといった，フォーマルメソッド

プライバシは守られるべきもの，匿名性はそのためのいで従来用いられてきた道具立てが必須なのはいうまでもわば必要悪，といった捉えられ方をされることもある．

ない．しかしその前に，匿名性・プライバシをフォーマもちろん，もっと違った捉え方をする人もいるだろう．

ルな議論に乗せるためには，そもそもまずそれらをフォ解決への手がかりを求めて，まずはいったんフォーマーマルに（あるいは数理的に）定式化する必要がある．そルメソッドから離れ，目を法律へと向けてみたいと思う．

して実は，現在のセキュリティのフォーマルメソッド研

なぜなら法律は，プライバシの問題を一般的に，かつフ究において，そのような定式化や分類学自体もホットなォーマルとは言わないまでも厳密に定式化した大先輩だ

テーマなのだ．

からだ．ただし，単に法的な定義をフォーマルに焼き直た と え ば Hughes と Shimatikov は， 匿 名 性 や プ ラ

そうというのではない．匿名性・プライバシの法的な取イ バ シ に 関 係 す る さ ま ざ ま な 性 質 を identity-related

り扱いを知ることでそこに潜む問題の難しさを明確化す

property と呼び，該当する数十の性質を，function viewるのが，次の章の目的である．そのあと“匿名性とプラと protocol graph という独自の枠組みでフォーマルかつイバシのためのフォーマルメソッド概観 ” の章では，匿統一的に分類／整理している 3）．また，匿名性に関して名性・プライバシ検証のためのフォーマルメソッドを，のみだが，知識論理と呼ばれる論理体系で一般的に記述代表的な研究を取り上げて説明する．そして，“ 法的なするという Halpern と OʼNeill の研究もある （これにプライバシふたたび ” の章でふたたび法的な問題をフォついては，後でよりくわしく紹介する）．しかしそのよーマルな見方で振り返り，最後にまとめを述べる．

2）

うな研究によって，匿名性・プライバシのフォーマルな530

情報処理 Vol.49 No.5 May 2008

6 匿名性とプライバシのためのフォーマルメソッド
法的な匿名性・プライバシという判断が示された．
これらの要件は，基本的に現在でも踏襲されている

本章では，日本の現行法と判例に基づく匿名性とプラが，若干の変遷もある．たとえば，1 つ目の要件には “ 私イバシについて概観する．ただし，筆者は法律には素人生活上の ” という条件（私事性）が含まれるが，これは現なので，記述・議論が至らない点も多いかと思う．法的在では必須ではないとされている．たとえば，個人の犯なプライバシに関する詳しい説明は，たとえば文献 6）

罪経歴はプライバシに属するが，法的に有罪となっていなどを参考にされたい．なお，本章では特に断らないかる以上公の事実であって私事ではあり得ないからである．

ぎり，“ プライバシ ” という言葉を，フォーマルな意味また，上記の要件以外にも考慮されるべきこととして，ではなく法的な意味で用いる．

表現の自由とプライバシの関係，公人とプライバシの関係などが挙げられる．

●プライバシ権と個人情報保護

さらにもう 1 つ注意すべき点として，1 つ目の要件に日本においてプライバシの侵害から個人を守る法的枠関連して，明示的ではないが前提とされていることがあ

組みには，プライバシ権と個人情報保護法がある．個人る．それは，公開された内容によって当該個人を同定可

情報保護法は，個人情報取扱事業者の義務を規定する法能だということである．このことは，とりわけ特定の個律であり，しばしば道路交通法に例えられる．つまり，人をモデルとした小説によるプライバシ侵害のときに問交通事故を防ぐために道路交通法があるように，個人情題となり，上記 “ 宴のあと ” 事件のほかにも，柳美里に報の取り扱いを巡るトラブルを防ぐためのルールが同法よるモデル小説に関する “ 石に泳ぐ魚 ” 事件の裁判（最だということである．そこで規定される個人情報は，“生高判平成 14 年 9 月 24 日判時 1802 号 60 頁）などでも争存する個人に関する情報であって，当該情報に含まれる点の 1 つとなっている．

氏名，生年月日その他の記述等により特定の個人を識別さて，個人を同定可能だということは，匿名ではないすることができるもの ” とされ，法的にはプライバシとということである．逆に言えば，匿名性が成り立っていされない情報も含む．この法律のフォーマルな取り扱いる状況ではプライバシ侵害はあり得ないということになも興味深いテーマだが，本稿ではこれ以上ふれないことる．これは，匿名性とプライバシの法的な関係の 1 つとにする．

言える．しかし，この関係は常に妥当なのだろうか？

プライバシを法的な権利として世界で最初に論じたのは，Harvard Law Review に 1890 年に発表された Warren●完全に匿名ならプライバシは守られる？と Brandeis の論文 “The Right to Privacy” だが，日本で問題の切実さを強調するため，あえてやや刺激的な例

それが本格的に議論されるようになったのは 1960 年代からはいることにする．目線入りのヌード写真，しかも以降である．日本におけるプライバシ権は，日本国憲法

自分の，を想像していただきたい．だれかに “ このとお第 13 条（個人の尊重）によって保証されると解されていり目線を入れるから，いやそれでも心配なら顔全部を黒るが，明文化はされていない．判例としては，1964 年

塗りするから，この写真をネットで公開していい？ ” とに “ 私生活をみだりに公開されないという法的保証ない

聞かれたら，あなたはどう答えるだろうか．完全に匿名し権利 ” としてのプライバシ権を認める，いわゆる “ 宴だったら構わない，と答える人ばかりではないと思う．のあと ” 事件に関する判決が出される（東京地判昭和 39

あるいは別の例として，インターネット掲示版で，特定年 9 月 28 日判時 385 号 12 頁）．本事件は，同名の小説の個人の行動を多人数で監視し逐一掲示するといういたが原告有田八郎のプライバシを侵害したとして，著者のずらが行われているという．筆者はこれを悪質なプライ三島由紀夫と出版元の新潮社を被告として提起された民バシ侵害だと考えるが，では仮にそのいたずらを，監視事訴訟である．その判決の中で，プライバシの侵害によされる個人の名前をふせて匿名で行ったらどうだろう．

る不法行為の成立要件として，公開された内容が，もはやプライバシ侵害ではないと言えるだろうか．たとえ監視されているのが誰かは分からなくても “ こいつ，

1. 私生活上の事実または私生活上の事実らしく受け取られるおそれのあることがらであること

こんなバカなことやってるよ！ ” といった誹謗中傷は可能だし，それがほかならぬ自分自身に向けられたもので

2. 一般人の感受性を基準にして当該私人の立場に立つたあることは，監視されている本人には分かるのである．

場合公開を欲しないであろうと認められることがらで以上は，匿名性が成り立っていてもプライバシを侵害あること
3. 一般の人々に未だ知られていないことがらであることされていると感じられそうな例のつもりである．しかしながらこのような単純な例では，“ もしかすると，なに情報処理 Vol.49 No.5 May 2008531

特集 ● フォーマルメソッドの新潮流

Part III：新領域の開拓
同一人物のものだと公表されてしまうとこの間の結びつきを公表されたら‥‥？

社会に貢献する活動

他人に知られたくない活動

したらどうだろう．もし “ 仮名 1 を使って偉そうなことを言っていながら，その陰でその他の活動

こそこそ仮名 2 のようなことをしているな…

んて · · · ” などと他人から非難されることになれば不快だし，仮名 1 による活動も困

仮名 1

仮名 2

仮名 3

難になってしまうかもれない．公表してほ…
…

結びつけ困難⇒ 匿名

しくないと感じるのが自然だろうし，少なくとも日常的な意味では，ある種のプライバシの侵害だと考えられるのではないだ

本人（実体）

ろうか．しかしながら，法的にはそれを公表することはプライバシ侵害にはあたら

図 -1 仮名の名寄せによるプライバシ侵害ないはずである．理由はもちろん，本人かのはずみで匿名でなくなってしまい，私を同定できての同定ができないからだ．現在の日本の判例に基づくと，しまうかもしれない ” という危惧に基づく不快・不安と仮名が完全であればあるほど，本人の同定が困難となるいう要素が残ってしまうため，前節の終わりに指摘したがゆえに，プライバシ侵害の要件を満たさなくなる．つ関係の妥当性を議論するためには精度を欠く．そこで以まり，完全な仮名による完全な匿名性の実現が，結果と下では，もうすこし凝った例を考えよう．“ 仮名（かめい）

してプライバシを守るどころか，このケースに関してはの名寄せ ” の問題である．

逆に法によるプライバシ保護を完全に不能にしてしまう

インターネットでは，よくハンドルと呼ばれる仮名がという，なんともパラドキシカルな状況なのである．な用いられる．しかも 1 つではなく，複数のハンドルを使ぜこのようなことが起こってしまうのだろう？

い分けている場合も多い．継続的に用いるハンドルはコった事柄は法的に保護するにはおよばないのか，あるい

テハン，一時的に利用してすぐに捨ててしまうハンドルはプライバシではなく何か別な枠組みで守られるべきこは捨てハンなどと呼ばれる．ネットの匿名性を利用して，となのか．

こうい

状況により複数のアイデンティティを使い分けているわ

筆者はこれが何らかの不備に起因するものかどうかすけだ．また仮名でできることは，掲示版への書き込みのら判断する力を持たないし，ここでの目的はそのようなようなとるに足らないことだけではない．たとえばコンことではない．しかしながら，前節の終わりに指摘した

ビニエンスストアでウェブマネーなどの電子現金を買え

匿名性とプライバシの関係の妥当性には何かしら困難なば，仮名だけである程度の経済活動もできる．ネット上問題が存在し，以上のような込み入った議論がつきまとで社会に貢献する活動を行ってはいるが，何らかの事情うということはご確認いただけたと思う．

で実名を明かせず仮名を使っているといった状況（たと問題が 1 つ確認されたところで，つけ焼き刃の法律論えば，独裁国家からの亡命者に対する情報提供など）もはいったん終わりにし，以降は本題のフォーマルメソッあり得るだろう．

ドに話をもどす．そして最後に，フォーマルな見方でふ

しかしここでも，インターネットにおける仮名だの匿たたびこの問題を眺めてみたいと思う．

名性だのはしょせん絵空事であって，たとえばプロバイダの通信履歴照会などで個人が特定される可能性だってあるではないか，と思われるかもしれない．しかし現在の暗号技術を使えば，ある比較的弱い仮定のもとに，仮匿名性とプライバシのためのフォーマルメ
ソッド概観

名と本人との結びつけができないことを理論的に証明で匿名性・プライバシ検証のためのフォーマルメソッド

きる仮名，つまり実質的に完全な仮名を作ることも不可には，大きく分けて 2 つのアプローチがある．1 つは状能ではないのである．この，“ ある比較的弱い仮定 ” を態遷移モデルに基づくアプローチで，セキュリティを記

厳密に述べるには計算量理論などの準備が必要となるが，述する様式とそれを検証する方法をともに与えるという詳細は文献 1）などを参照されたい．

意味において，工学的に高い有用性を持つ．もう 1 つは

さて仮にいま，ある人が上記のような仮名を複数使い知識論理に基づくアプローチで，その高い表現力によっ分け，仮名 1 でなにかしら社会に貢献する活動を，仮名て，さまざまなセキュリティ要件の微妙な違いの書き分

2 で他人に知られたくないプライベートな活動をしていけや，関係する性質の間の比較を容易にするというメリたとする（図 -1）．そのとき，仮名 1 と仮名 2 が，実はットを持つ．本章では，それぞれについて代表的な研究

532

情報処理 Vol.49 No.5 May 2008

6 匿名性とプライバシのためのフォーマルメソッドを取り上げつつ説明する．

●状態遷移モデルに基づくアプローチ
本アプローチは，状態遷移モデルでシステムの動作を記述し，さらにその動作の等価性に基づいて匿名性・プライバシを記述するというものである．また，その等価性を証明するのに，模倣あるいは双模倣と呼ばれる証明技法を用いるという特徴もある．本節では，代表的な研究として Kremer と Ryan のもの 4）を取り上げ，このアプローチについて概説する☆ 1．

: 何もしないプロセス: プロセス P とQ を非決定的に選択して実行: P とQ を並行に実行: 通信チャネル c へ値 d を送信: 通信チャネル c から x の 値を受信
: 新しい定数の生成: replication，P のコピーを無限個生成（ループ構文の代わり）

図 -2 プロセス式のプリミティブ

同値関係 ≡（抜粋）

まず，匿名性・プライバシは他のセキュリティと同じく，だれかに対して何らかの情報を隠すことである．隠したい相手は通常 “ 攻撃者 ” と呼ばれる．この攻撃者が遷移規則（抜粋）どういう能力を持つと想定するかが，セキュリティの記述にも検証にも重要であるが，それを規定するために，多くの検証で Dolev-Yao モデルというある種の理想化された攻撃者のモデルが採用されている．これにはいくつ

図 -3 プロセス式の動作（構造操作的意味論）かのバリエーションが存在するが，基本的な特徴は以下の 2 つの仮定を置くことである :これは直観的には “ 鍵 k で暗号化したものを同じ鍵で復号化すると元に戻る ” ということを表現しているが，さ1. システムで用いる暗号は “ 完全 ” である，すなわち，らに，前提とする性質が上の等式のみならば，k と同値

攻撃者は復号鍵を知らないかぎり，暗号化されたメッでない項を enc(x, k) といかように組み合わせても x をセージを解読できない．

作ることはできない．このことを，“k なしに enc(x, k)

2. 攻撃者は，通信路を “ 完全 ” に支配する，すなわち，を解読できない ” ことに対応させるのである．ほかにも，攻撃者はすべてのメッセージを盗聴できるだけでなく，たとえば公開鍵暗号の場合なら，秘密鍵から公開鍵への遅延させたり，不達にしたり，あるいは改竄・偽造し関数を記号 pub で表して dec(enc(x, pub(k)), k)= x といたメッセージを送り込んだりすることができる．

う等式を用いるといった具合に，さまざまな暗号要素技術がこの方法でフォーマルに定式化できる．

ただし，2 でできる盗聴や改竄は，あくまで 1 に定める

次に，仮定 2 の定式化では通信を伴うシステムの動作能力の範囲内のことのみである．たとえばもし，メッセの記述方法が重要だが，一般には状態遷移モデルが用いージが暗号化されていて，かつその復号鍵を攻撃者が知られる．状態遷移モデルには，オートマトン，ペトリネ

らないならば，盗聴はできてもその内容まで知ることはット，プロセス計算などがあるが，ここでは文献 4）でできない．Dolev-Yao に基づくフォーマルな検証のため用いられているプロセス計算を説明する．には，これら 2 つの仮定をフォーマルに定式化する必要がある．

プロセス計算とは，通信プロセスを記述するのに必要なプリミティブを代数の演算子として表現し，それら演仮定 1 の定式化には，主にメッセージ代数と呼ばれる算子を組み合わせることによって，代数的体裁の式とし方法が用いられる．メッセージ代数では，暗号化／復て通信プロセスを記述することができる理論的体系であ号化操作を enc, dec といった関数記号で表す．たとえば，る．プロセス計算のプリミティブとしては，図 -2 に示し

123 を鍵 k で暗号化したものは enc(123, k) という項になたものがある．プロセス式の動作は，構造操作的意味論る．そして，たとえば単純な対称鍵暗号の場合，それらと呼ばれるある種の推論体系によって定義される（図 -3）．の性質を次のようなたった 1 つの等式で表現する :dec(enc(x, k), k) = x☆1

この研究は applied pi-calculus と呼ばれるプロセス計算に基づいているが，本稿でこれについての技術的内容を厳密に述べることはできない．以下の説明でプロセス計算といったら，彼らが用いた体系を本稿のために筆者が大胆に単純化したものであり，正確さに欠ける部分もあることをあらかじめご容赦願いたい．

たとえば，通信チャネル c から暗号化されたデータenc(d, k) を送信して止まるプロセスは c̄(enc(d, k)); 0，cからデータを受け取って変数 x に格納し R という後続処理を行うプロセスは c(x); R，それらを並行に動作させたものは，c̄(enc(d, k)). 0 | c(x). R
情報処理 Vol.49 No.5 May 2008533

特集 ● フォーマルメソッドの新潮流

Part III：新領域の開拓と書く．

る攻撃者も識別できない ” と読み替えているわけである．

プロセス計算をシステムの記述に用いる最大のメリッ

実際文献 4）では，上記のような合同式をプライバシ

トの 1 つは，合同性と呼ばれるプロセスの等価性に関すと呼び，弱ラベル付き双模倣という証明技法を用いて，る研究の蓄積を利用できることである．いまプロセス間FOO と呼ばれる電子投票システムに関してそれが成りのある等価性を.で表すとすると，その等価性が合同的立つことをフォーマルに検証している．

であるとは，P . Q ならば，任意の文脈 C[ ]（これもプロセス式で表現される）について C[P] . C[Q] となるこ

●知識論理に基づくアプローチとを言う．代数的な体裁の記述にこのような等価性が定

前節で紹介した，情報隠蔽をある種の識別不能性に読まることを期待するのはきわめて自然であり，当たり前み替えて合同関係の形で定式化し，模倣証明技法で検証だと感じられるかもしれない．しかし，並行システムのするアプローチは，セキュリティを記述する様式とそれ記述においてそれが決して自明ではないことは，プロセを検証する方法をともに与えるという意味で，有用性がス計算研究の初期からよく知られた事実であり，多くの高い．実際，多くの検証ケーススタディがこのアプロー研究がなされている．

チで得られている．しかし，問題がないわけではない．

この合同性は，セキュリティの記述にも役立つ．たと1 つの問題は，識別不能性に基づく定式化と，我々がえば上に挙げた例で，攻撃者が鍵 k を知らないときに暗思い描く匿名性・プライバシは，本当に合致しているの号化されたメッセージの内容が洩れないことは，プロかということである．少なくとも，“ 法的な匿名性・プセス計算でどのように定式化できるだろう？

この場ライバシ ” の章で見たプライバシの定義と前節の定式化

合，合同性を用いて記述するために問題を次のように読の間を埋めるのは，かならずしも容易な作業ではない．

み替える : データ d の代わりに他の任意の d' を使っても，“ 攻撃者に · · · が分からない ” といった性質を，もっといかなる攻撃者もそれを識別できない．これは以下の合ダイレクトに記述する方法はないだろうか．

同式で表現できる :( o k)( c̄(enc(d, k)). 0 | c(x). R).

( o k)( c̄(enc(d', k)). 0 | c(x). R)

もう 1 つの問題は，性質を記述した個々の等式自体が（前節の例では電子投票という）個別具体的なシステムに依存していることである．冒頭の章でも述べたように，一般性のあるメソッド構築のために，“ 匿名性自体 ”，“プつまり，どういう攻撃者でもその動作がプロセス式で記ライバシ自体 ” をもっと一般的な形で記述できないだろ

述できるかぎり一種の文脈なので，合同性から識別できうか．

ないということだ．ここで両辺を ( o k) で囲っているの

本節で紹介する知識論理に基づくアプローチは，上のは，k を知っているとする範囲を限定し，攻撃者が k をような疑問に答えられる可能性を持つ．ここでは，代知らないという条件を規定するためである．

表的な研究である Halpern と OʼNeill の研究 2）をもとにでは，匿名性やプライバシはどうだろう．たとえば電解説する．彼らは，セキュリティの “· · · が分からない ”

子投票システムでは，匿名性・プライバシに関する性質という性質を記述するために，知識論理という体系を用として，“ どの有権者が，どの候補者に投票したか ” といる．知識論理とは，広くは様相論理と呼ばれる論理体いう情報の秘密が守られることが期待される．仮にいま，系の 1 つであり，知っている／知らないを表現する様相

有権者 v1，v2 がそれぞれ，候補者 c1，c2 に投票したとオペレータを導入することで一般の述語論理を拡張した

ライアントシステムの動作を表すプロセス式とすると，

知 識 を 表 現 す る オ ペ レ ー タ は Ki と 書 く．K はする．P を，投票者 x が候補者 y に投票する際の投票ク
その投票状況は，
P{x := v1, y := c1} | P{x := v2, y := c2}

ものである．
“know” の頭文字，i はその知識の持ち主を表す．たとえば，知識論理式 Ki(Beautiful(rose)) は，“ バラは美しい，ということを i さんは知っている ” を表す，とという式になる．さらに，それ以外の投票システム全体いった具合である．知識オペレータに否定を組み合を S とすると，電子投票に期待される先の性質は，次わせると，可能性を表現することもできる．たとえば，の合同式で表すことができる :¬Ki¬(Delicious(grasshopper)) は，“ バッタはおいしくS | P{x := v1, y := c1} | P{x := v2, y := c2}. S | P{x := v1, y := c2} | P{x := v2, y := c1}
ここでは先の性質を，“v1，v2 がそれぞれ c1，c2 に投票した状況と，それらの役割を入れ換えた状況とを，いかな

534

情報処理 Vol.49 No.5 May 2008

ない，ということを i さんは知っているわけではない ”ということだが，言い替えれば “ バッタはおいしいかもしれないと i は思っている ” となる．このことから¬Ki¬ を possibility の頭文字を使って Pi と略記する．
知識論理の特長の 1 つは，その高い表現力によってさ

6 匿名性とプライバシのためのフォーマルメソッド
まざまなセキュリティ要件の微妙な違いまで書き分けらIA の条件れることである．たとえば Halpern らは，極小匿名性と呼ばれる性質を以下のように定式化した :匿名性
導出¬Kj [ i (i, a)]

導出全体が双対

ここで， i (i, a) は，“i さんが a というアクションを行った ” ということ，つまり行為者と行為内容の結びつきだけを抽象的に表現する述語である．具体的な事例の匿名性を考えるときには，それに合わせて i の解釈を定める

同じ役割交換可能性

プライバシ
導出

AI の条件とすることによって，個別具体的な事例に依存しない形で匿名性を定式化している．式全体の意味は，“i が a を役割交換可能性

図 -4 匿名性とプライバシの双対性行ったことを，j は知っているわけではない ” である．
匿名性には，ほかにもいろいろなバリエーションがあいう問題の構造を表現することを試みる．このような設る．たとえば，“i が a を行ったとき，IA という集合の定では，行為者 i のプライバシは，攻撃者に “i がどう中の誰でもそれを行った可能性がある，と j は思っていいう行為をしたか ” が分からないといった性質になるが，る ” ということは，こんな風に書ける :これも匿名性と同様に知識論理でうまく表現できる．たP j 6 i ( il, a) @i (i, a) &il! IA

とえば，“i が a を行ったとき，彼はアクションの集合
AI の中でどれをも行った可能性がある，と j は思っている ” という性質，すなわち集合 AI 中でのプライバシは，こ の 性 質 は， 集 合 IA 中 で の 匿 名 性 と 呼 ば れ て い る．

i (i, a) という前提の必要性に関して，Halpern らは “ 疑われない性質 ”(unsuspectibility) との違いを指摘しているが，次章では別の側面にも触れる☆ 2．

以下のように書ける :i ]i, a g &P j 6i ]i, a lg @al ! A I

ところで，上記の匿名性と，前節の最後に示した等式

この式は，先に示した集合 IA 中での匿名性と対称的なとはどういう関係にあるだろう．これに関しては，文形をしていることが見て取っていただけると思う．実

献 5）で議論されている．等式は，投票者 v1 と v2 の役割

はこの対称性は，ある種構造的なものである．たとえが逆だったとしてもそれを識別できないということを表ば，役割交換可能性から集合中での匿名性を導出できた

していたが，このような性質も知識論理で一般的に定式

ように，役割交換可能性から集合中でのプライバシを導化できる :ける．再度電子投票の例で言えば，AI として “ 絶対に]i ] i, a g / i ] i l, a lgg & P j 6i ] i l, a g / i ] i, a lg @1 票は得票する候補者への投票 ” を取ればいい．しかも
図 -4 のように，それら匿名性とプライバシの導出過程

これは役割交換可能性と呼ばれている性質である．では，全体が対称的になっているのである．こういった対称性

たとえば役割交換可能性から集合中での匿名性を導くこを数学ではしばしば双対と呼ぶ．つまりこのような見方とはできるだろうか？

では，匿名性とプライバシは双対だ，ということになる．

厳密な証明は参照論文にあたっていただくとして，電子投票に即して直観的に言えば，

この双対性は，単にものの見方として面白いだけでIA として “ 絶対に棄権しない有権者 ” の集合を取ればはなく，工学的な有用性も持つ．実は，同じく図 -4 で，いい．知識論理による記述には，以上のように関係する上下の役割交換可能性は同一の性質である．なぜならば，性質の間の厳密な比較を容易にするメリットもある．

役割交換可能性はそれ自身対称的な形をしているからだ．

次に，プライバシについて考えてみよう．上と同じく
文献 5）に基づいて説明する．ここでは Halpern らにな

この性質に着目して，匿名性とプライバシの検証を効率良く行う方法を文献 5）では示している．

らって，述語 i (i, a) を使って定式化できるプライバシを考える．つまり，“ 公開を欲しない ” という意図や “ 未だ知られていない ” といった条件をあえて捨象し，行為者と行為内容の結びつきだけに着目してプライバシと法的なプライバシふたたび
前節で紹介した，フォーマルに定式化された匿名性とその双対としてのプライバシを，法的なプライバシと比☆2

極小匿名に同様の前提を追加してもその意味が変わらないことは，容易に証明できる．

較してみよう．
いろいろな食い違いがある．たとえば，法的なプライ情報処理 Vol.49 No.5 May 2008535

特集 ● フォーマルメソッドの新潮流

Part III：新領域の開拓

バシは基本的に 1 つだが，双対としてのプライバシの方ロール権という考え方☆ 3 とも親和性が高いと思われる．

は知識論理の記述力を生かしてさまざまなバリエーシ

また自己情報証明は，フォーマルな定義との対応もはっョンを記述し分けられることを特長とする．また，法きしりている．実は，双対としてのプライバシの定義に的なプライバシには，“ 公開を欲しない ” という意図やあるθ(i, a) という前提が成立することの確認に相当す“ 未だ知られていない ” といった条件が明示されているるのである．

が，双対としてのプライバシではそれらは捨象され，具繰り返すが，以上はあくまで 1 つの可能性としての議体的なプライバシを定める際のある種のパラメタとなっ論であって，現実の法的なプライバシがかくあるべきだ，ている．また，何かが公開されることと特定の攻撃者がと述べているわけではない．実際たとえば，日本では匿それを知ることとは，法的には違いがあるだろう．しか名での訴訟が認められていないため，公にすることなくし，筆者がさらに大きな違いだと考えるのは，法的には自己情報証明を行うことは現状の法制度では困難だ，と匿名性侵害（厳密には個人の同定可能性）がプライバシ侵いった問題もある．しかしながら，匿名性・プライバシ害の要件になっているのに対して，フォーマルな匿名性のフォーマルな定式化が，法的な込み入った議論を見通とその双対としてのプライバシとは対称的でむしろ対等しよく行うのに資する場合もある，ということを示す例だ，ということである．

ではあると筆者は考える．

この最後の食い違いに関しても，とりあえず，フォーマルな匿名性とプライバシの両方が成立する状況ならば法的なプライバシも保証されている，といった関係は成おわりにり立ちそうである．しかし逆に，法的なプライバシ侵害

本稿では，匿名性とプライバシのためのフォーマルメにおける同定可能性という要件は絶対なのだろうか．実

ソッド，とりわけそれらの定式化に焦点をあて，さらに際 “ 法的な匿名性・プライバシ ” の章で私事性に関して妥当性や一般性を法律との対応を通して見てきた．法律も見たように，プライバシの要件には変遷がある．専門とフォーマルメソッドとのこのような対応を議論するこ

家にうかがったところ，現在のところ同定可能性を要件とは，近年注目されている法令工学との関連でも重要とから外した判例は存在しないとのことである．しかし一なるだろう．他のセキュリティと比べて，匿名性とプラ方，たとえば重度の皮膚病の医学写真などと関連して，イバシのフォーマルな研究の歴史は浅く，今後ますます高度にセンシティブな情報にかかわる場合は目線を入れ発展していくことが期待される．て匿名にしさえすればいいとはいえないのではないか，といった議論もあるようだ．また，仮名の名寄せの例が謝辞

現実に問題となるような社会状況になれば，要件の再検また貴重な助言をくださった，岡村久道先生と壇俊光先討が必要になるかもしれない．

生に感謝いたします．

しかし私事性と違い，同定可能性に関しては単に条件を外せばいいというわけではない．ある人のプライバシを広く保証することは，裏を返せばその他の人の知る権利を制限することになるが，同定可能性を単に外してしまうことは，法的なプライバシの範囲を過度に広げてしまう恐れがある．では，どうすればいいだろう？
以下はあくまで可能性としての議論だが，たとえば代わりに，公開された情報が確かに自分の情報であるということを証明できること，すなわち “ 自己情報証明 ” 可能性を要件とするのはどうだろう．すなわち，私のプライバシ侵害に関して，他人から見てその行為の行為者たる私を同定できるかどうかを問題とする代わりに，私がたしかにその行為を行ったのだということをなんらかの方法で証明する，ということである．これは，法的なプライバシに関して近年注目されている自己情報コント☆3536

公権力による情報の収集に対して，個人がそれらの情報をコントロール（開示，変更，消去など）できるという考え方．

情報処理 Vol.49 No.5 May 2008

筆者との拙い法律談義におつき合いくださり，参考文献
1）Chaum, D. L. : Untraceable Electronic Mail, Return Addresses, andDigital Pseudonyms, Communication of the ACM, Vol.24, No.2, pp.84-90(1981).
2）Halpern, J. Y. and OʼNeill, K. R. : Anonymity and Information Hiding
in Multiagent Systems, J. Computer Security, Vol.13, No.3, pp.483-514(2005).
3）Hughes, D. and Shmatikov, V. : Information Hiding, Anonymity andPrivacy : A Modular Approach, J. Computer Security, Vol.12, No.1,pp.3-36 (2004).
4）Kremer, S. and Ryan, M. : Analysis of An Electronic Voting Protocolin the Applied Pi Calculus, In European Symposium on ProgrammingESOP 2005, pp.186-200, 2005. LNCS 3444.
5）M a n o , K . , K a w a b e , Y. , S a k u r a d a , H . a n d Ts u k a d a , Y. : R o l eInterchangeability and Verification of Electronic Voting, In 2006
Symposium on Cryptography and Information Security (SCISʼ06)(2006).
6）新保史生：プライバシの権利の生成と展開，成文堂 (2000).
（平成 20 年 3 月 25 日受付）
真野 健（正会員）
mano@theory.brl.ntt.co.jp
1989 年名古屋大学大学院工学研究科情報工学専攻修士課程修了．同年日本電信電話（株）入社．現在コミュニケーション科学基礎研究所主任研究員．項書換え系，プロセス計算，数理的技法による情報セキュリティの研究に従事．電子情報通信学会，日本ソフトウェア科学会各会員．