Automatic verification for later-correspondence of security protocols

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationStructured Object-Oriented Formal Language and Method - 4th International Workshop, SOFL+MSVL 2014, Revised Selected Papers
EditorsZhenhua Duan, Shaoying Liu
PublisherSpringer Verlag
Pages111-126
Number of pages16
ISBN (Electronic)9783319174037
DOIs
Publication statusPublished - 2015
Externally publishedYes
Event4th International Workshop on Structured Object-Oriented Formal Language, SOFL 2014 and International Workshop on Modeling, Simulation, and Verification Language, MSVL 2014 - Luxembourg, Luxembourg
Duration: Nov 6 2014Nov 6 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8979
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference4th International Workshop on Structured Object-Oriented Formal Language, SOFL 2014 and International Workshop on Modeling, Simulation, and Verification Language, MSVL 2014
Country/TerritoryLuxembourg
CityLuxembourg
Period11/6/1411/6/14

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Automatic verification for later-correspondence of security protocols'. Together they form a unique fingerprint.

Cite this