一句话：提出约简符号语义与偏序归约，消除冗余交错，加速安全协议的迹等价判定。
安全协议的许多隐私性质可在进程代数中建模为迹等价。对有限进程类，这类性质已能通过符号执行与约束求解判定，但现有原型工具常因探索大量行为交错而组合爆炸。本文将 Mödersheim 等人针对可达性性质的偏序归约工作加以推广，使其适用于等价性检查，并提出一种约简符号语义，在符号执行过程中即时消除冗余交错。该技术已集成到工具 APTE 中。完整基准测试表明，其性能获得显著提升。
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\"odersheim 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.Comment: Accepted for publication in LMCS
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{BaeldeDH17,
title = {A Reduced Semantics for Deciding Trace Equivalence},
author = {David Baelde and Stéphanie Delaune and Lucca Hirschi},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 2},
year = {2017},
doi = {10.23638/lmcs-13(2:8)2017}
}