首页    期刊浏览 2024年11月29日 星期五
登录注册

文章基本信息

  • 标题:Partial Order Reduction for Security Protocols
  • 本地全文:下载
  • 作者:David Baelde ; St{\'e}phanie Delaune ; Lucca Hirschi
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2015
  • 卷号:42
  • 页码:497-510
  • DOI:10.4230/LIPIcs.CONCUR.2015.497
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:Security protocols are concurrent processes that communicate using cryptography with the aim of achieving various security properties. Recent work on their formal verification has brought procedures and tools for deciding trace equivalence properties (e.g. anonymity, unlinkability, vote secrecy) for a bounded number of sessions. However, these procedures are based on a naive symbolic exploration of all traces of the considered processes which, unsurprisingly, greatly limits the scalability and practical impact of the verification tools. In this paper, we mitigate this difficulty by developing partial order reduction techniques for the verification of security protocols. We provide reduced transition systems that optimally eliminate redundant traces, and which are adequate for model-checking trace equivalence properties of protocols by means of symbolic execution. We have implemented our reductions in the tool Apte, and demonstrated that it achieves the expected speedup on various protocols.
  • 关键词:Cryptographic protocols; verification; process algebra; trace equivalence
国家哲学社会科学文献中心版权所有