Automatic verification for later-correspondence of security protocols

Xiaofei Xie, Xiaohong Li, Yang Liu, Li Li, Ruitao Feng, Zhiyong Feng

研究成果: Chapter in Book/Report/Conference proceedingConference contribution

1 被引用数 (Scopus)

抄録

Ensuring correspondence is very important and useful in designing security protocols. Previously, many research works focus on the verification of former-correspondence which means “if the protocol executes some event, then it must have executed some other events before”. However, in some security protocols, it is also important to ensure the engagement of some events after an event happens. In this work, we propose a new property called later-correspondence, which is very useful for e-commerce protocols. The applied π-calculus is extended to specify the protocols. A simplified intruder model is proposed for modeling the intruder capabilities which includes the malicious behaviors of both protocol agents and intruders. The later-correspondence is verified based on the Labeled Transition System (LTS) using model checking. In order to avoid the states explosion, we limit the number of protocol sessions and reduce most of the useless messages from the intruder knowledge with message pattern filtering. We implement our method in a model checker PAT [23] and the verification results show that our method can verify later-correspondence in an effective way.

本文言語英語
ホスト出版物のタイトルStructured Object-Oriented Formal Language and Method - 4th International Workshop, SOFL+MSVL 2014, Revised Selected Papers
編集者Zhenhua Duan, Shaoying Liu
出版社Springer Verlag
ページ111-126
ページ数16
ISBN(電子版)9783319174037
DOI
出版ステータス出版済み - 2015
外部発表はい
イベント4th International Workshop on Structured Object-Oriented Formal Language, SOFL 2014 and International Workshop on Modeling, Simulation, and Verification Language, MSVL 2014 - Luxembourg, ルクセンブルク
継続期間: 11 6 201411 6 2014

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
8979
ISSN(印刷版)0302-9743
ISSN(電子版)1611-3349

会議

会議4th International Workshop on Structured Object-Oriented Formal Language, SOFL 2014 and International Workshop on Modeling, Simulation, and Verification Language, MSVL 2014
国/地域ルクセンブルク
CityLuxembourg
Period11/6/1411/6/14

All Science Journal Classification (ASJC) codes

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「Automatic verification for later-correspondence of security protocols」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル