Search

This extended abstract gives a construction for lifting a Gr\"obner basis algorithm for an ideal in a polynomial ring over a commutative ring R under the condition that R also admits a Gr\"obner basis for every ideal in R.

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., Comment: In Proceedings GandALF 2022, arXiv:2209.09333

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., Comment: 28 pages, 6 figures, will be submitted for LMCS journal. arXiv admin note: substantial text overlap with arXiv:1706.05607

Building user trust in dialogue agents requires smooth and consistent dialogue exchanges. However, agents can easily lose conversational context and generate irrelevant utterances. These situations are called dialogue breakdown, where agent utterances prevent users from continuing the conversation. Building systems to detect dialogue breakdown allows agents to recover appropriately or avoid breakdown entirely. In this paper we investigate the use of semi-supervised learning methods to improve dialogue breakdown detection, including continued pre-training on the Reddit dataset and a manifold-based data augmentation method. We demonstrate the effectiveness of these methods on the Dialogue Breakdown Detection Challenge (DBDC) English shared task. Our submissions to the 2020 DBDC5 shared task place first, beating baselines and other submissions by over 12\% accuracy. In ablations on DBDC4 data from 2019, our semi-supervised learning methods improve the performance of a baseline BERT model by 2\% accuracy. These methods are applicable generally to any dialogue task and provide a simple way to improve model performance., Comment: 6 pages, 1 figure, accepted at the NeurIPS Workshop on Human in the Loop Dialogue Systems

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.

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.

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.

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., Comment: Revised based on reviewers' feedback

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.

An algorithm for unification modulo one-sided distributivity is an early result by Tid\'en 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.

Programs that process data that reside in files are widely used in varied domains, such as banking, healthcare, and web-traffic analysis. Precise static analysis of these programs in the context of software verification and transformation tasks is a challenging problem. Our key insight is that static analysis of file-processing programs can be made more useful if knowledge of the input file formats of these programs is made available to the analysis. We propose a generic framework that is able to perform any given underlying abstract interpretation on the program, while restricting the attention of the analysis to program paths that are potentially feasible when the program's input conforms to the given file format specification. We describe an implementation of our approach, and present empirical results using real and realistic programs that show how our approach enables novel verification and transformation tasks, and also improves the precision of standard analysis problems.

In current wireless systems, the base-Station (eNodeB) tries to serve its user-equipment (UE) at the highest possible rate that the UE can reliably decode. The eNodeB obtains this rate information as a quantized feedback from the UE at time n and uses this, for rate selection till the next feedback is received at time n + {\delta}. The feedback received at n can become outdated before n + {\delta}, because of a) Doppler fading, and b) Change in the set of active interferers for a UE. Therefore rate prediction becomes essential. Since, the rates belong to a discrete set, we propose a discrete sequence prediction approach, wherein, frequency trees for the discrete sequences are built using source encoding algorithms like Prediction by Partial Match (PPM). Finding the optimal depth of the frequency tree used for prediction is cast as a model order selection problem. The rate sequence complexity is analysed to provide an upper bound on model order. Information-theoretic criteria are then used to solve the model order problem. Finally, two prediction algorithms are proposed, using the PPM with optimal model order and system level simulations demonstrate the improvement in packet loss and throughput due to these algorithms.

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., Comment: 26 pages

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., Comment: In Proceedings UNIF 2010, arXiv:1012.4554

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., Comment: In Proceedings UNIF 2010, arXiv:1012.4554

A model for signal delay computation in RC networks is presented. The strength of the paradigm is its generality and simplicity. The definition of delay is applicable to RC meshes with potential resistive attenuating paths to ground. The algorithms can also be applied to undriven circuits (static charge sharing) and circuits with initial charge. To compute the delays, each node in the network is explored locally to derive a system of sparse linear equations. The solutions of the system are delay values based on the Elmore time constant at each point in the circuit.