Presentation Information
[B-16-13]Tamarin Prover を用いた DNS 通信の機関プライバシの一考察
〇Satoru Sunahara1, Niko Kuroda, Shigeki Hagihara2 (1. Hokkaido University., 2. Chitose Institute of Science and Technology.)
Keywords:
Formal Verification,DNS,Institutional privacy,Tamarin Prover,Anonymity
現代のインターネットにおいてDNSは不可欠なシステムであるが、従来の平文送信では利用者のプライバシーが脅かされる危険性がある。近年、再帰リゾルバと権威DNSサーバ間の暗号化通信方式が標準化されつつあるが、その匿名性は十分に評価されていない。そこで本研究では、形式検証ツール「Tamarin Prover」を用い、ECH（Encrypted Client Hello）を用いた直接通信方式と、ODoH（Oblivious DNS over HTTPS）に代表されるマルチリレー方式を統一的にモデル化し、提供される匿名性を形式的に比較評価した。評価にあたっては、通信経路上の受動攻撃者を想定し、「送信元匿名性」と「DNS問い合わせ匿名性」の2つの指標から観測等価性を検証した。検証の結果、直接通信方式は通信経路上の攻撃者に対して問い合わせ内容を保護するものの、送信元匿名性は成立せず、権威DNSサーバの侵害時には全ての匿名性が失われることが判明した。一方、マルチリレー方式では、ProxyまたはTarget リゾルバのいずれか一方が侵害された場合でも、送信元と問い合わせ内容の対応付けを防ぎ、高い匿名性を維持できることを確認した。ただし、中継ノードが共謀した場合には匿名性が失われるため、実運用ではノードの独立性が重要となる。本研究により各方式の匿名性の特徴が明らかとなり、今後はトラフィック解析や能動攻撃を考慮したより現実的な脅威モデルでの評価を進める予定である。