David Baelde ; Stéphanie Delaune ; Lucca Hirschi - A Reduced Semantics for Deciding Trace Equivalence

lmcs:3309 - Logical Methods in Computer Science, June 8, 2017, Volume 13, Issue 2 - https://doi.org/10.23638/LMCS-13(2:8)2017
A Reduced Semantics for Deciding Trace EquivalenceArticle

Authors: David Baelde ; Stéphanie Delaune ; Lucca Hirschi

    Many privacy-type properties of security protocols can be modelled using trace equivalence properties in suitable process algebras. It has been shown that such properties can be decided for interesting classes of finite processes (i.e., without replication) by means of symbolic execution and constraint solving. However, this does not suffice to obtain practical tools. Current prototypes suffer from a classical combinatorial explosion problem caused by the exploration of many interleavings in the behaviour of processes. Mödersheim et al. have tackled this problem for reachability properties using partial order reduction techniques. We revisit their work, generalize it and adapt it for equivalence checking. We obtain an optimisation in the form of a reduced symbolic semantics that eliminates redundant interleavings on the fly. The obtained partial order reduction technique has been integrated in a tool called APTE. We conducted complete benchmarks showing dramatic improvements.


    Volume: Volume 13, Issue 2
    Published on: June 8, 2017
    Accepted on: May 10, 2017
    Submitted on: June 8, 2017
    Keywords: Computer Science - Logic in Computer Science,C.2.2,D.2.4,F.3.1
    Funding:
      Source : OpenAIRE Graph
    • Security properties, process equivalences and automated verification; Funder: French National Research Agency (ANR); Code: ANR-14-CE28-0030
    • Reasoning about Physical properties Of security Protocols with an Application To contactless Systems; Funder: European Commission; Code: 714955

    Consultation statistics

    This page has been seen 2017 times.
    This article's PDF has been downloaded 355 times.