BAN論理からProtocol Composition Logicへ : セキュリティプロトコルの論理的検証法(<特集>数理的技法による情報セキュリティ)
スポンサーリンク
概要
- 論文の詳細を見る
We give an overview of several inference-based formal verification methods for security protocols. Especially, we survey the basic ideas of BAN logic and Protocol Composition Logic (PCL) and their related works such as Basic Protocol Logic (BPL). We also discuss some recent works on computational semantics for PCL.
- 2007-12-26
著者
-
岡田 光弘
慶應義塾大学文学部哲学専攻
-
長谷部 浩二
産業技術総合研究所システム検証研究センター
-
長谷部 浩二
産業技術総合研究所
-
Okada Mitsuhiro
慶應義塾大学文学部
-
Okada Mitsuhiro
Department Of Philosphy Keio University
-
Okada Mitsuhiro
Department Of Philosophy Keio University
-
岡田 光弘
Department of Philosphy, Keio University
関連論文
- 現代応用オントロジーの哲学的・論理学的源泉(オントロジーの進化と普及(前編))
- 線形論理に基づく計算モデルの理論概説
- 線形論理に基づいたセキュリティ・プロトコルの論理的検証法(自動推論 : 演繹, 帰納, モデル検査/生成, 仮説推論アブダクション, 論理プログラム, プランニング, 時相論理, etc.)
- ウィトゲンシュタイン, 言語の限界, 飯田隆著, 講談社, 1997年.
- BAN論理からProtocol Composition Logicへ : セキュリティプロトコルの論理的検証法(数理的技法による情報セキュリティ)
- A Hierarchy of the Fragments of the System of Inductive Definition : Preliminary Report
- Semantic Characterizations for Reachability and Trace Equivalence in a Linear Logic-Based Process Calculus : Preliminary Report
- A Relationship among Gentzen's Proof-Reduction, Kirby-Paris' Hydra Game, and Buchholz's Hydra Game(Preliminary Report)(Mathematical Incompleteness in Arithmetic)
- 論理記号導入規則による論理的意味論について
- ソフトウェアの安全性をめぐる課題について(人に触れる機械の課題)
- 矛盾は矛盾か (特集 ラッセルのパラドックス・100年)
- 歪んだ真珠(バロック) : 音楽における規則性VS反規則性,またはロゴスVSパトス
- オントロジー応用のための方法論の考察と展望(哲学とAIにおける対象世界モデリング)(〔第4回〕)
- 現代のフォーマルオントロジーの動向とオントロジー工学(「哲学とAIにおける対象世界モデリング」〔第3回〕)
- フッサールのフォーマルオントロジーとその影響(哲学とAIにおける対象世界モデリング〔第2回〕)
- オントロジーの哲学的・論理学的背景
- 「哲学とAIにおける対象世界モデリング」の企画にあたって
- 日本語の文末表現における意味解釈と音響特性
- フッサールの形式論理学分析における「多様体」概念の役割
- Characterization Theorems for Multiplicative Fragment of Intuitionistic Non-Commutative Linear Logic : Preliminary Report
- 3.線形論理に基づく並行計算モデル : 並行計算の論理的理解の試み (並行計算の理論の最近の動向)
- 倫理学入門のためのPersonal Guide
- デカルトにおける「論証」の概念と彼の形而上学的論証の論理的基準(100集記念号)
- A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic(Preliminary Report)(Non-Classical Logics and Their Kripke Semantics)
- 諸状況における終助詞「か」の意味解釈と音響特性
- 論理学入門のためのPersonal Guide
- 「普遍学」の夢と現実 : 論理推論体系の可能性を求めて(文学部創設百周年記念論文集I)
- フッサ-ル初期の「哲学的-数学的諸研究の終結テ-マ」とゲッチンゲン学派の論理哲学
- 論理的意味論と整合性証明
- Some Remarks on a Difference between Gentzen's Finitist and Heyting's Intuitionist Approaches toward Intuitionistic Logic and Arithmetic
- Completeness Proofs for Linear Logic Based on the Proof Search Method(Preliminary Report)(Type Theory and its Applications to Computer Systems)
- Note on the Strong Normalizability of the Logic with Self-Referential Predicates
- "The Concluding Theme of Philosophical-Mathematical Students" in the Early Husserl, and the Logical Philosophy of Goettingen School