scholarly journals Computing knowledge in equational extensions of subterm convergent theories

2020 ◽  
Vol 30 (6) ◽  
pp. 683-709
Author(s):  
Serdar Erbatur ◽  
Andrew M. Marshall ◽  
Christophe Ringeissen
Keyword(s):  
General Procedure ◽  
Security Protocols ◽  
Equational Theory ◽  
Finite Measure ◽  
Decision Procedures ◽  
Rewrite Systems ◽  
Static Equivalence ◽  
Equivalence Problems ◽  
Rewrite System

AbstractWe study decision procedures for two knowledge problems critical to the verification of security protocols, namely the intruder deduction and the static equivalence problems. These problems can be related to particular forms of context matching and context unification. Both problems are defined with respect to an equational theory and are known to be decidable when the equational theory is given by a subterm convergent term rewrite system (TRS). In this work, we extend this to consider a subterm convergent TRS defined modulo an equational theory, like Commutativity. We present two pairs of solutions for these important problems. The first solves the deduction and static equivalence problems in rewrite systems modulo shallow theories such as Commutativity. The second provides a general procedure that solves the deduction and static equivalence problems in subterm convergent systems modulo syntactic permutative theories, provided a finite measure is ensured. Several examples of such theories are also given.

scholarly journals Transforming Prefix-constrained or Controlled Rewrite Systems

10.29007/m335 ◽  
2018 ◽  
Author(s):  
Nirina Andrianarivelo ◽  
Vivien Pelletier ◽  
Pierre Réty
Keyword(s):  
Rewrite Systems ◽  
Rewrite System

We present two techniques for transforming any prefix-constrained and any controlled term rewrite system into an ordinary rewrite system. We prove that both transformations preserve the rewrite com- putations, and preserve termination. In this way, prefix-constrained rewriting and controlled rewriting can be run, and termination can be checked, using the usual tools for ordinary rewriting.

THE BRESSAUD NORMAL FORM OF BRAIDS THROUGH WORD REWRITE SYSTEMS

2013 ◽  
Vol 22 (01) ◽  
pp. 1250135
Author(s):  
JEREMY CHAMBOREDON
Keyword(s):  
Normal Form ◽  
Knot Theory ◽  
Rewrite Systems ◽  
Rewrite System

We introduce a nondeterministic rewrite system which is conjectured to converge to the Bressaud normal form of braids as presented in [X. Bressaud, A normal form for braids, J. Knot Theory Ramifications17(6) (2008) 697–732]. We prove the conjecture for 3-strand braids.

scholarly journals Logics for The Applied pi Calculus

2006 ◽  
Vol 13 (19) ◽  
Author(s):  
Michael David Pedersen
Keyword(s):  
Dynamic Properties ◽  
Equational Theory ◽  
Strong Version ◽  
First Order ◽  
Original Definition ◽  
Master's Thesis ◽  
Pi Calculus ◽  
Static Equivalence ◽  
Definition Of ◽  
Reasoning About Knowledge

In this master's thesis we present a modal logic for Applied pi which characterises observational equivalence on processes. The motivation is similar to that of Applied pi itself, namely generality: the logic can be adapted to a particular application simply by defining a suitable equational theory on terms.<br /> <br />As a first step towards the logic for Applied pi, a strong version of static equivalence on frames is introduced in which term reductions are observable in addition to equality on terms. We argue that the strong version is meaningful in applications and give two refined definitions based on the notion of cores introduced in work by Boreale et al. for the Spi calculus. The refined definitions are useful because they do not involve universal quantification over arbitrary terms and hence are amenable to a logical characterisation. We show that the refined definitions coincide with the original definition of strong static equivalence under certain general conditions.<br /> <br />A first order logic for frames which characterises strong static equivalence and which yields characteristic formulae is then given based on the refined definitions of strong static equivalence. This logic facilitates direct reasoning about terms in a frame as well as indirect reasoning about knowledge deducible from a frame. The logic for Applied pi is then obtained by adding suitable Hennessy-Milner style modalities to the logic for frames, hence facilitating reasoning about both static and dynamic properties of processes. We finally demonstrate the logic with an application to the analysis of the Needham-Schroeder Public Key Protocol.

scholarly journals Finding small counterexamples for abstract rewriting properties

2018 ◽  
Vol 28 (8) ◽  
pp. 1485-1505
Author(s):  
HANS ZANTEMA
Keyword(s):  
Binary Relation ◽  
Normal Forms ◽  
Satisfying Assignment ◽  
Rewrite Systems ◽  
Abstract Setting ◽  
Sat Solver ◽  
Rewrite System ◽  
A Current

Rewriting notions like termination, normal forms and confluence can be described in an abstract way referring to rewriting only as a binary relation. Several theorems on rewriting, like Newman's lemma, can be proved in this abstract setting. For investigating possible generalizations of such theorems, it is fruitful to have counterexamples showing that particular generalizations do not hold. In this paper, we develop a technique to find such counterexamples fully automatically, and we describe our tool Carpa that follows this technique. The basic idea is to fix the number of objects of the abstract rewrite system, and to express the conditions and the negation of the conclusion in a satisfiability (SAT) formula, and then call a current SAT solver. In case the formula turns out to be satisfiable, the resulting satisfying assignment yields a counterexample to the encoded property. We give several examples of finite abstract rewrite systems having remarkable properties that are found in this way fully automatically.

scholarly journals E-unification by means of tree tuple synchronized grammars

1997 ◽  
Vol Vol. 1 ◽  
Author(s):  
Sébastien Limet ◽  
Pierre Réty
Keyword(s):  
Equational Theory ◽  
International Audience ◽  
Infinite Set ◽  
Rewrite System

International audience The goal of this paper is both to give an E-unification procedure that always terminates, and to decide unifiability. For this, we assume that the equational theory is specified by a confluent and constructor-based rewrite system, and that four additional restrictions are satisfied. We give a procedure that represents the (possibly infinite) set of solutions thanks to a tree tuple synchronized grammar, and that can decide upon unifiability thanks to an emptiness test. Moreover, we show that if only three of the four additional restrictions are satisfied then unifiability is undecidable.

scholarly journals Event structures and non-orthogonal term graph rewriting

1996 ◽  
Vol 6 (6) ◽  
pp. 545-578 ◽  
Author(s):  
David Clark ◽  
Richard Kennaway
Keyword(s):  
State Space ◽  
Garbage Collection ◽  
Event Structure ◽  
Graph Rewriting ◽  
Rewrite Systems ◽  
Event Structures ◽  
Asymmetric Conflicts ◽  
Algebraic Domain ◽  
Directed Completion ◽  
Rewrite System

We show that for every term graph in a left-linear but non-orthogonal term graph rewrite system, one can construct an event structure that represents all the possible reductions that can occur in reduction sequences starting from that term graph. Every finite reduction sequence from that graph corresponds to a configuration of the event structure, and Lévy-equivalent sequences correspond to the same configuration.Garbage collection is modelled in the event structure by an ‘erases’ relation. The asymmetric conflicts that arise in non-orthogonal rewrite systems are modelled by introducing a ‘prevents’ relation. The configurations of the event structure then form the state space of an event automaton. Taking the directed completion of this space yields a prime algebraic domain.

Towards a Standard for a Reliable Execution Environment for Security Protocols

2016 ◽  
Vol 2 (1) ◽  
pp. 78
Author(s):  
Mahalingam Ramkumar
Keyword(s):  
Information Systems ◽  
Full Advantage ◽  
Real World ◽  
Security Protocols ◽  
Low Complexity ◽  
High Integrity ◽  
Execution Environment ◽  
World Information ◽  
Digital Assets ◽  
Attack Models

Approaches for securing digital assets of information systems can be classified as active approaches based on attack models, and passive approaches based on system-models. Passive approaches are inherently superior to active ones. However, taking full advantage of passive approaches calls for a rigorous standard for a low-complexity-high-integrity execution environment for security protocols. We sketch broad outlines of mirror network (MN) modules, as a candidate for such a standard. Their utility in assuring real-world information systems is illustrated with examples.

Sign in / Sign up

Export Citation Format

Share Document