コンシェルジュサーバを持つ電話システムの形式的検証
スポンサーリンク
概要
- 論文の詳細を見る
電話による詐欺から身を守るには,発信者が詐欺師でないことを確認することが重要である.山本らは,この確認作業を(半)自動化するシステム(コンシェルジュサーバ)を提案している.電話がかかる際,コンシェルジュサーバは,電話接続の前に発信者に情報を求める.発信者からの情報が適切なものでなければ,接続は拒否される.本稿では,コンシェルジュサーバを持つ電話システムを形式化し,その正しさを検証する.我々は,I/O-オートマトン理論に基づく形式的仕様記述言語を用いてこの電話システムを記述し,さらに,トレース一致によりこの電話システムの正しさを示す.
- 2012-03-01
著者
-
河辺 義信
日本電信電話株式会社nttコミュニケーション科学基礎研究所
-
河辺 義信
愛知工業大学情報科学部情報科学科
-
黒野 恵人
愛知工業大学情報科学部情報科学科
-
前田 彩
愛知工業大学情報科学部情報科学科
-
河辺 義信
愛知工業大学 情報科学部 情報科学科
-
黒野 恵人
愛知工業大学 情報科学部 情報科学科
関連論文
- π計算に基づくプログラミング言語NepiのためのGUI機能
- ゲーム列による安全性証明の形式化と自動化(数理的技法による情報セキュリティ)
- 匿名性とプライバシ保護の数理的技法 (特集 コミュニケーション環境の未来に向けた研究最前線)
- ETAPS 2006参加報告(会議レポート)
- Nepiネットワークプログラミングシステムの形式的検証(ソフトウェア工学の基礎)
- π-計算の名前制限の名前生成による実装の正しさ
- プロセス代数に基づくネットワークプログラム言語 (特集論文1 情報科学研究の最前線--より安全で快適な情報処理技術を目指して) -- (快適にコンピュータを使えるために)
- π-計算に基づくモバイルエージェントの形式化
- アクタモデルのπ計算に基づく意味づけ : エージェントの形式化に向けて
- 攻撃者を考慮した匿名性検証法 (第20回 回路とシステム軽井沢ワークショップ論文集) -- (形式的手法)
- 電子投票プロトコルに対する無証拠性の定理証明
- 順序ソート項書換え系における合流性のモジュラ性
- 電子投票プロトコルに対する無証拠性の定理証明 (特集 人と共存するコンピュータセキュリティ技術)
- コンシェルジュサーバを持つ電話システムの形式的検証
- AT-1-2 Larch Proverによる論理パズルの解法(AT-1.システム数理における様々なツールの紹介,チュートリアルセッション,ソサイエティ企画)
- コンシェルジュサーバを持つ電話システムの形式的検証