-
Existence and Construction of a Gröbner Basis for a Polynomial Ideal
Authors:
Deepak Kapur,
Paliath Narendran
Abstract:
This extended abstract gives a construction for lifting a Gröbner basis algorithm for an ideal in a polynomial ring over a commutative ring R under the condition that R also admits a Gröbner basis for every ideal in R.
This extended abstract gives a construction for lifting a Gröbner basis algorithm for an ideal in a polynomial ring over a commutative ring R under the condition that R also admits a Gröbner basis for every ideal in R.
△ Less
Submitted 15 June, 2023;
originally announced June 2023.
-
CryptoSolve: Towards a Tool for the Symbolic Analysis of Cryptographic Algorithms
Authors:
Dalton Chichester,
Wei Du,
Raymond Kauffman,
Hai Lin,
Christopher Lynch,
Andrew M. Marshall,
Catherine A. Meadows,
Paliath Narendran,
Veena Ravishankar,
Luis Rovira,
Brandon Rozek
Abstract:
Recently, interest has been emerging in the application of symbolic techniques to the specification and analysis of cryptosystems. These techniques, when accompanied by suitable proofs of soundness/completeness, can be used both to identify insecure cryptosystems and prove sound ones secure. But although a number of such symbolic algorithms have been developed and implemented, they remain scattere…
▽ More
Recently, interest has been emerging in the application of symbolic techniques to the specification and analysis of cryptosystems. These techniques, when accompanied by suitable proofs of soundness/completeness, can be used both to identify insecure cryptosystems and prove sound ones secure. But although a number of such symbolic algorithms have been developed and implemented, they remain scattered throughout the literature. In this paper, we present a tool, CryptoSolve, which provides a common basis for specification and implementation of these algorithms, CryptoSolve includes libraries that provide the term algebras used to express symbolic cryptographic systems, as well as implementations of useful algorithms, such as unification and variant generation. In its current initial iteration, it features several algorithms for the generation and analysis of cryptographic modes of operation, which allow one to use block ciphers to encrypt messages more than one block long. The goal of our work is to continue expanding the tool in order to consider additional cryptosystems and security questions, as well as extend the symbolic libraries to increase their applicability.
△ Less
Submitted 21 September, 2022;
originally announced September 2022.
-
On Problems Dual to Unification: The String-Rewriting Case
Authors:
Zümrüt Akçam,
Kimberly A. Cornell,
Daniel S. Hono II,
Paliath Narendran,
Andrew Pulver
Abstract:
In this paper, we investigate problems which are dual to the unification problem, namely the Fixed Point (FP) problem, Common Term (CT) problem and the Common Equation (CE) problem for string rewriting systems. Our main motivation is computing fixed points in systems, such as loop invariants in programming languages. We show that the fixed point (FP) problem is reducible to the common term problem…
▽ More
In this paper, we investigate problems which are dual to the unification problem, namely the Fixed Point (FP) problem, Common Term (CT) problem and the Common Equation (CE) problem for string rewriting systems. Our main motivation is computing fixed points in systems, such as loop invariants in programming languages. We show that the fixed point (FP) problem is reducible to the common term problem. Our new results are: (i) the fixed point problem is undecidable for finite convergent string rewriting systems whereas it is decidable in polynomial time for finite, convergent and dwindling string rewriting systems, (ii) the common term problem is undecidable for the class of dwindling string rewriting systems, and (iii) for the class of finite, monadic and convergent systems, the common equation problem is decidable in polynomial time but for the class of dwindling string rewriting systems, common equation problem is undecidable.
△ Less
Submitted 30 December, 2023; v1 submitted 27 February, 2021;
originally announced March 2021.
-
On Asymmetric Unification for the Theory of XOR with a Homomorphism
Authors:
Christopher Lynch,
Andrew M. Marshall,
Catherine Meadows,
Paliath Narendran,
Veena Ravishankar
Abstract:
Asymmetric unification, or unification with irreducibility constraints, is a newly developed paradigm that arose out of the automated analysis of cryptographic protocols. However, there are still relatively few asymmetric unification algorithms. In this paper we address this lack by exploring the application of automata-based unification methods. We examine the theory of xor with a homomorphism, A…
▽ More
Asymmetric unification, or unification with irreducibility constraints, is a newly developed paradigm that arose out of the automated analysis of cryptographic protocols. However, there are still relatively few asymmetric unification algorithms. In this paper we address this lack by exploring the application of automata-based unification methods. We examine the theory of xor with a homomorphism, ACUNh, from the point of view of asymmetric unification, and develop a new automata-based decision procedure. Then, we adapt a recently developed asymmetric combination procedure to produce a general asymmetric- ACUNh decision procedure. Finally, we present a new approach for obtaining a solution-generating asymmetric-ACUNh unification automaton. We also compare our approach to the most commonly used form of asymmetric unification available today, variant unification.
△ Less
Submitted 29 June, 2019;
originally announced July 2019.
-
On Problems Dual to Unification
Authors:
Zümrüt Akçam,
Daniel S. Hono II,
Paliath Narendran
Abstract:
In this paper, we investigate a problem dual to the unification problem, namely the Common Term (CT) problem for string rewriting systems. Our main motivation was in computing fixed points in systems, such as loop invariants in programming languages. We show that the fixed point problem is reducible to the common term problem. We also prove that the common term problem is undecidable for dwindling…
▽ More
In this paper, we investigate a problem dual to the unification problem, namely the Common Term (CT) problem for string rewriting systems. Our main motivation was in computing fixed points in systems, such as loop invariants in programming languages. We show that the fixed point problem is reducible to the common term problem. We also prove that the common term problem is undecidable for dwindling string rewriting systems.
△ Less
Submitted 3 October, 2017; v1 submitted 18 June, 2017;
originally announced June 2017.
-
Asymmetric Unification and Disunification
Authors:
Veena Ravishankar,
Kimberly A. Gero,
Paliath Narendran
Abstract:
We compare two kinds of unification problems: Asymmetric Unification and Disunification, which are variants of Equational Unification. Asymmetric Unification is a type of Equational Unification where the right-hand sides of the equations are in normal form with respect to the given term rewriting system. In Disunification we solve equations and disequations with respect to an equational theory for…
▽ More
We compare two kinds of unification problems: Asymmetric Unification and Disunification, which are variants of Equational Unification. Asymmetric Unification is a type of Equational Unification where the right-hand sides of the equations are in normal form with respect to the given term rewriting system. In Disunification we solve equations and disequations with respect to an equational theory for the case with free constants. We contrast the time complexities of both and show that the two problems are incomparable: there are theories where one can be solved in Polynomial time while the other is NP-hard. This goes both ways. The time complexity also varies based on the termination ordering used in the term rewriting system.
△ Less
Submitted 5 October, 2017; v1 submitted 15 June, 2017;
originally announced June 2017.
-
Lynch-Morawska Systems on Strings
Authors:
Daniel S. Hono II,
Paliath Narendran,
Rafael Veras
Abstract:
We investigate properties of convergent and forward-closed string rewriting systems in the context of the syntactic criteria introduced in \cite{LynchMorawska} by Christopher Lynch and Barbara Morawska (we call these $LM$-Systems). Since a string rewriting system can be viewed as a term-rewriting system over a signature of purely monadic function symbols, we adapt their definition to the string re…
▽ More
We investigate properties of convergent and forward-closed string rewriting systems in the context of the syntactic criteria introduced in \cite{LynchMorawska} by Christopher Lynch and Barbara Morawska (we call these $LM$-Systems). Since a string rewriting system can be viewed as a term-rewriting system over a signature of purely monadic function symbols, we adapt their definition to the string rewriting case. We prove that the subterm-collapse problem for convergent and forward-closed string rewriting systems is effectively solvable. Therefore, there exists a decision procedure that verifies if such a system is an $LM$-System. We use the same construction to prove that the \emph{cap problem} from the field of cryptographic protocol analysis, which is undecidable for general $LM$-systems, is decidable when restricted to the string rewriting case.
△ Less
Submitted 31 May, 2016; v1 submitted 21 April, 2016;
originally announced April 2016.
-
Notes on Lynch-Morawska Systems
Authors:
Daniel S. Hono II,
Namrata Galatage,
Kimberly A. Gero,
Paliath Narendran,
Ananya Subburathinam
Abstract:
In this paper we investigate convergent term rewriting systems that conform to the criteria set out by Christopher Lynch and Barbara Morawska in their seminal paper "Basic Syntactic Mutation." The equational unification problem modulo such a rewrite system is solvable in polynomial-time. In this paper, we derive properties of such a system which we call an $LM$-system. We show, in particular, that…
▽ More
In this paper we investigate convergent term rewriting systems that conform to the criteria set out by Christopher Lynch and Barbara Morawska in their seminal paper "Basic Syntactic Mutation." The equational unification problem modulo such a rewrite system is solvable in polynomial-time. In this paper, we derive properties of such a system which we call an $LM$-system. We show, in particular, that the rewrite rules in an $LM$-system have no left- or right-overlaps. We also show that despite the restricted nature of an $LM$-system, there are important undecidable problems, such as the deduction problem in cryptographic protocol analysis (also called the the cap problem) that remain undecidable for $LM$-systems.
△ Less
Submitted 29 May, 2016; v1 submitted 20 April, 2016;
originally announced April 2016.
-
On Unification Modulo One-Sided Distributivity: Algorithms, Variants and Asymmetry
Authors:
Andrew M Marshall,
Catherine Meadows,
Paliath Narendran
Abstract:
An algorithm for unification modulo one-sided distributivity is an early result by Tidén and Arnborg. More recently this theory has been of interest in cryptographic protocol analysis due to the fact that many cryptographic operators satisfy this property. Unfortunately the algorithm presented in the paper, although correct, has recently been shown not to be polynomial time bounded as claimed. In…
▽ More
An algorithm for unification modulo one-sided distributivity is an early result by Tidén and Arnborg. More recently this theory has been of interest in cryptographic protocol analysis due to the fact that many cryptographic operators satisfy this property. Unfortunately the algorithm presented in the paper, although correct, has recently been shown not to be polynomial time bounded as claimed. In addition, for some instances, there exist most general unifiers that are exponentially large with respect to the input size. In this paper we first present a new polynomial time algorithm that solves the decision problem for a non-trivial subcase, based on a typed theory, of unification modulo one-sided distributivity. Next we present a new polynomial algorithm that solves the decision problem for unification modulo one-sided distributivity. A construction, employing string compression, is used to achieve the polynomial bound. Lastly, we examine the one-sided distributivity problem in the new asymmetric unification paradigm. We give the first asymmetric unification algorithm for one-sided distributivity.
△ Less
Submitted 18 June, 2015; v1 submitted 23 March, 2015;
originally announced March 2015.
-
Unification modulo a 2-sorted Equational theory for Cipher-Decipher Block Chaining
Authors:
Siva Anantharaman,
Christopher Bouchard,
Paliath Narendran,
Michaël Rusinowitch
Abstract:
We investigate unification problems related to the Cipher Block Chaining (CBC) mode of encryption. We first model chaining in terms of a simple, convergent, rewrite system over a signature with two disjoint sorts: list and element. By interpreting a particular symbol of this signature suitably, the rewrite system can model several practical situations of interest. An inference procedure is present…
▽ More
We investigate unification problems related to the Cipher Block Chaining (CBC) mode of encryption. We first model chaining in terms of a simple, convergent, rewrite system over a signature with two disjoint sorts: list and element. By interpreting a particular symbol of this signature suitably, the rewrite system can model several practical situations of interest. An inference procedure is presented for deciding the unification problem modulo this rewrite system. The procedure is modular in the following sense: any given problem is handled by a system of `list-inferences', and the set of equations thus derived between the element-terms of the problem is then handed over to any (`black-box') procedure which is complete for solving these element-equations. An example of application of this unification procedure is given, as attack detection on a Needham-Schroeder like protocol, employing the CBC encryption mode based on the associative-commutative (AC) operator XOR. The 2-sorted convergent rewrite system is then extended into one that fully captures a block chaining encryption-decryption mode at an abstract level, using no AC-symbols; and unification modulo this extended system is also shown to be decidable.
△ Less
Submitted 6 February, 2014; v1 submitted 2 January, 2014;
originally announced January 2014.
-
On the Complexity of the Tiden-Arnborg Algorithm for Unification modulo One-Sided Distributivity
Authors:
Paliath Narendran,
Andrew Marshall,
Bibhu Mahapatra
Abstract:
We prove that the Tiden and Arnborg algorithm for equational unification modulo one-sided distributivity is not polynomial time bounded as previously thought. A set of counterexamples is developed that demonstrates that the algorithm goes through exponentially many steps.
We prove that the Tiden and Arnborg algorithm for equational unification modulo one-sided distributivity is not polynomial time bounded as previously thought. A set of counterexamples is developed that demonstrates that the algorithm goes through exponentially many steps.
△ Less
Submitted 22 December, 2010;
originally announced December 2010.
-
Unification modulo a partial theory of exponentiation
Authors:
Deepak Kapur,
Andrew Marshall,
Paliath Narendran
Abstract:
Modular exponentiation is a common mathematical operation in modern cryptography. This, along with modular multiplication at the base and exponent levels (to different moduli) plays an important role in a large number of key agreement protocols. In our earlier work, we gave many decidability as well as undecidability results for multiple equational theories, involving various properties of modula…
▽ More
Modular exponentiation is a common mathematical operation in modern cryptography. This, along with modular multiplication at the base and exponent levels (to different moduli) plays an important role in a large number of key agreement protocols. In our earlier work, we gave many decidability as well as undecidability results for multiple equational theories, involving various properties of modular exponentiation. Here, we consider a partial subtheory focussing only on exponentiation and multiplication operators. Two main results are proved. The first result is positive, namely, that the unification problem for the above theory (in which no additional property is assumed of the multiplication operators) is decidable. The second result is negative: if we assume that the two multiplication operators belong to two different abelian groups, then the unification problem becomes undecidable.
△ Less
Submitted 22 December, 2010;
originally announced December 2010.
