講演名 2002/5/17
線形論理に基づいたセキュリティ・プロトコルの論理的検証法(<特集>自動推論 : 演繹, 帰納, モデル検査/生成, 仮説推論アブダクション, 論理プログラム, プランニング, 時相論理, etc.)
岡田 光弘, 長谷部 浩二,
PDFダウンロードページ PDFダウンロードページへ
抄録(和) 線形論理を用いたセキュリティ・プロトコルの論理的記述法及び検証法の枠組が与えられる.まずプロトコルに従ったプロセスを線形論理の証明により表現する方法を示し,さらにこの表現方法を用いた安全性検証の枠組について述べる.線形論理をもとにした実時間システムの表現法が既に知られている.我々はこの方法に従い,上の枠組を拡張して時刻認証を用いたプロトコルにおけるメッセージの新鮮さの量的時間制約による表現法も示す.さらにこの時間制約条件の分析手法をもとに,時刻認証を用いたプロトコルに対する攻撃を防御するための時間制約条件を導出する方法を示す.
抄録(英) We give a framework of logical methods for specifying and verifying security protocols based on linear logic. A process following a security protocol is represented by a linear logic proof, and using this method, we give a framework of security verification method. By means of a known method for specifying real-time systems based on linear logic, we represent freshness of messages with timestamps by quantative time constraints and give a method of deducing conditions for protection against attacks.
キーワード(和) 線形論理 / 証明 / セキュリティ・プロトコル / 安全性検証 / 実時間 / 時刻認証
キーワード(英) Linear logic / Proof / Security protocol / Security verification / Real-Time / Timestamp
資料番号 AI2002-9
発行日

研究会情報
研究会 AI
開催期間 2002/5/17(から1日開催)
開催地(和)
開催地(英)
テーマ(和)
テーマ(英)
委員長氏名(和)
委員長氏名(英)
副委員長氏名(和)
副委員長氏名(英)
幹事氏名(和)
幹事氏名(英)
幹事補佐氏名(和)
幹事補佐氏名(英)

講演論文情報詳細
申込み研究会 Artificial Intelligence and Knowledge-Based Processing (AI)
本文の言語 JPN
タイトル(和) 線形論理に基づいたセキュリティ・プロトコルの論理的検証法(<特集>自動推論 : 演繹, 帰納, モデル検査/生成, 仮説推論アブダクション, 論理プログラム, プランニング, 時相論理, etc.)
サブタイトル(和)
タイトル(英) Logical Verifications for Security Protocols Based on Linear Logic
サブタイトル(和)
キーワード(1)(和/英) 線形論理 / Linear logic
キーワード(2)(和/英) 証明 / Proof
キーワード(3)(和/英) セキュリティ・プロトコル / Security protocol
キーワード(4)(和/英) 安全性検証 / Security verification
キーワード(5)(和/英) 実時間 / Real-Time
キーワード(6)(和/英) 時刻認証 / Timestamp
第 1 著者 氏名(和/英) 岡田 光弘 / Mitsuhiro OKADA
第 1 著者 所属(和/英) 慶應義塾大学文学部
Faculty of Letters, Keio University
第 2 著者 氏名(和/英) 長谷部 浩二 / Koji HASEBE
第 2 著者 所属(和/英) 慶應義塾大学文学部
Faculty of Letters, Keio University
発表年月日 2002/5/17
資料番号 AI2002-9
巻番号(vol) vol.102
号番号(no) 91
ページ範囲 pp.-
ページ数 6
発行日