Loading...
Please wait, while we are loading the content...
Similar Documents
A reduced semantics for deciding trace equivalence using constraint systems.
| Content Provider | CiteSeerX |
|---|---|
| Author | Baelde, David Hirschi, Lucca |
| Abstract | Abstract. 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. [17] 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 optimization in the form of a reduced symbolic semantics that eliminates redundant interleavings on the fly. 1 |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Trace Equivalence Reduced Semantics Constraint System Finite Process Many Privacy-type Property Partial Order Reduction Technique Symbolic Execution Security Protocol Trace Equivalence Property Redundant Interleavings Reduced Symbolic Semantics Equivalence Checking Classical Combinatorial Explosion Problem Interesting Class Suitable Process Algebra Constraint Solving Reachability Property Many Interleavings Practical Tool |
| Content Type | Text |
| Resource Type | Article |
