On-the-fly Model Checking of Security Protocols and Its Implementation by Maude
スポンサーリンク
概要
- 論文の詳細を見る
Trace analysis for a security protocol represents every possible run as a trace and analyzes whether any insecure run is reachable. The number of traces will be infinite due to (1) infinitely many sessions of a protocol, (2) infinitely many principals in the network, and (3) infinitely many messages that intruders can generate. This paper presents an on-the-fly model checking method by restricting/abstracting these infinite factors to a finite model. First, we restrict a typed process calculus to avoid recursive operations, so that only finitely many sessions are considered. Next, a bound variable is introduced as an index of a message to represent its intended destination, so that an unbounded number of principals are finitely described. Then, messages in which irrelevant parts are reduced in a protocol are unified to a parametric message based on the type information. We implement the on-the-fly model checking method using Maude, and automatically detect the flaws of several security protocols, such as the NSPK protocol and the Woo-Lam protocol, etc..
- 一般社団法人 情報処理学会の論文
著者
-
Ogawa Mizuhito
School of Information Science - Japan Advanced Institute Science and Technology
-
Li Guoqiang
School Of Information Science Japan Advanced Institute Of Science And Technology
関連論文
- Combining Testing and Static Analysis to Overflow and Roundoff Error Detection
- Context-sensitive points-to analysis for Java as all-in-one weighted pushdown model checking
- Stacking-based Context-Sensitive Points-to Analysis for Java
- On-the-fly Model Checking of Security Protocols and Its Implementation by Maude
- Modular Stacking-based Context-Sensitive Program Analysis
- Associative Search on Shogi Game Records
- Alternate Stacking Technique Revisited: Inclusion Problem of Superdeterministic Pushdown Automata
- Alternate Stacking Technique Revisited: Inclusion Problem of Superdeterministic Pushdown Automata
- Well-Structured Pushdown Systems, Part 1:Decidable Classes for Coverability
- Nested timed automata
- raSAT: SMT for polynomial inequality
- On-the-fly Model Checking of Security Protocols and Its Implementation by Maude
- On-the-fly Model Checking of Security Protocols and Its Implementation by Maude