Author name cluster

Christopher Lynch

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

9 papers

2 author rows

GandALF Workshop 2022 Workshop Paper

CryptoSolve: Towards a Tool for the Symbolic Analysis of Cryptographic Algorithms

Dalton Chichester
Wei Du
Raymond Kauffman
Hai Lin
Christopher Lynch
Andrew M. Marshall
Catherine A. Meadows
Paliath Narendran

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.

PDF Details DOI

FSCD Conference 2021 Conference Paper

An RPO-Based Ordering Modulo Permutation Equations and Its Applications to Rewrite Systems

Dohan Kim 0001
Christopher Lynch

Rewriting modulo equations has been researched for several decades but due to the lack of suitable orderings, there are some limitations to rewriting modulo permutation equations. Given a finite set of permutation equations E, we present a new RPO-based ordering modulo E using (permutation) group actions and their associated orbits. It is an E-compatible reduction ordering on terms with the subterm property and is E-total on ground terms. We also present a completion and ground completion method for rewriting modulo a finite set of permutation equations E using our ordering modulo E. We show that our ground completion modulo E always admits a finite ground convergent (modulo E) rewrite system, which allows us to obtain the decidability of the word problem of ground theories modulo E.

Details

I&C Journal 2014 Journal Article

Efficient general AGH-unification

Zhiqiang Liu
Christopher Lynch

General E-unification is an important tool in cryptographic protocol analysis, where the equational theory E represents properties of the cryptographic algorithm, and uninterpreted function symbols represent other functions. The property of a homomorphism over an Abelian group is common in encryption algorithms such as RSA. The general E-unification problem in this theory is NP-complete, and existing algorithms are highly nondeterministic. We give a mostly deterministic set of inference rules for solving general E-unification modulo a homomorphism over an Abelian group, and prove that it is sound, complete and terminating. These inference rules have been implemented in Maude, and will be incorporated into the Maude-NRL Protocol Analyzer (Maude-NPA).

Details DOI

I&C Journal 2011 Journal Article

Automatic decidability and combinability

Christopher Lynch
Silvio Ranise
Christophe Ringeissen
Duc-Khanh Tran

Verification problems can often be encoded as first-order validity or satisfiability problems. The availability of efficient automated theorem provers is a crucial pre-requisite for automating various verification tasks as well as their cooperation with specialized decision procedures for selected theories, such as Presburger Arithmetic. In this paper, we investigate how automated provers based on a form of equational reasoning, called paramodulation, can be used in verification tools. More precisely, given a theory T axiomatizing some data structure, we devise a procedure to answer the following questions. Is the satisfiability problem of T decidable by paramodulation? Can a procedure based on paramodulation for T be efficiently combined with other specialized procedures by using the Nelson–Oppen schema? Finally, if paramodulation decides the satisfiability problem of two theories, does it decide satisfiability in their union? The procedure capable of answering all questions above is based on Schematic Saturation; an inference system capable of over-approximating the inferences of paramodulation when solving satisfiability problems in a given theory T. Clause schemas derived by Schematic Saturation describe all clauses derived by paramodulation so that the answers to the questions above are obtained by checking that only finitely many different clause schemas are derived or that certain clause schemas are not derived.

Details DOI

LPAR Conference 2007 Conference Paper

Protocol Verification Via Rigid/Flexible Resolution

Stéphanie Delaune
Hai Lin 0005
Christopher Lynch

Abstract We propose a decision procedure, i. e. an inference system for clauses containing rigid and flexible variables. Rigid variables are only allowed to have one instantiation, whereas flexible variables are allowed as many instantiations as desired. We assume a set of clauses containing only rigid variables together with a set of clauses containing only flexible variables. When the flexible clauses fall into a particular class, we propose an inference system based on ordered resolution that is sound and complete and for which the inference procedure will halt. An interest in this form of problem is for cryptographic protocol verification for a bounded number of protocol instances. Our class allows us to obtain a generic decidability result for a large class of cryptographic protocols that may use for instance CBC (Cipher Block Chaining) encryption and blind signature.

Details

CSL Conference 2004 Conference Paper

Unsound Theorem Proving

Christopher Lynch

Abstract We discuss the benefits of complete unsound inference procedures for efficient methods of disproof. We give a framework for converting a sound and complete saturation-based inference procedure into successive unsound and complete procedures, that serve as successive approximations to the theory. The idea is to successively add new statements in such a way that the inference procedure will halt. Then the satisfiability is evaluated over a stronger theory. This gives an over-approximation to the given theory. We show how to successively compute better over-approximations. Similarly, a sound an incomplete theorem prover will give an under-approximation. In our framework, we succesively compute better over and under-approximations in this way. We illustrate this framework with Knuth-Bendix Completion, and show that in some theories this method becomes a decision procedure. Then we illustrate the framework with a new method for the (nonground) word problem, based on Congruence Closure. We show a class where this becomes a decision procedure. Also, we show that this new inference system is interesting in its own right. Given a particular goal, in many cases we can halt the procedure at some point and say that all the equations for solving the goal have been generated already. This is generally not possible in Knuth-Bendix Completion.

Details

LPAR Conference 2001 Conference Paper

Complexity of Linear Standard Theories

Christopher Lynch
Barbara Morawska 0001

Abstract We give an algorithm for deciding E -unification problems for linear standard equational theories (linear equations with all shared variables at a depth less than two) and varity 1 goals (linear equations with no shared variables). We show that the algorithm halts in quadratic time for the non-uniform E -unification problem, and linear time if the equational theory is varity 1. The algorithm is still polynomial for the uniform problem. The size of the complete set of unifiers is exponential, but membership in that set can be determined in polynomial time. For any goal (not just varity 1) we give a NEXPTIME algorithm.

Details

I&C Journal 1998 Journal Article

Local Simplification

Christopher Lynch

We present a modification to the paramodulation inference system, where semantic equality and nonequality literals are stored aslocal simplifierswith each clause. The local simplifiers are created when new clauses are generated and inherited by the descendants of that clause. Then the local simplifiers can be used to perform demodulation and unit simplification, if certain conditions are satisfied. This reduces the search space of the theorem proving procedure and the length of the proofs obtained. In fact, we show that for ground SLD resolution with any selection rule, any set of clauses has a polynomial length proof. Without this technique, proofs may be exponential. We show that this process is sound, complete, and compatible with deletion rules (e. g. , demodulation, subsumption, unit simplification, and tautology deletion), which do not have to be modified to preserve completeness. We also show the relationship between this technique and model elimination.

Details DOI

TCS Journal 1995 Journal Article

Redundancy criteria for constrained completion

Christopher Lynch
Wayne Snyder

This paper studies completion in the case of equations with constraints consisting of first-order formulae over equations, disequations, and an irreducibility predicate. We present several inference systems which show in a very precise way how to take advantage of redundancy notions in this framework. A notable feature of these systems is the variety of trade-offs they present for removing redundant instances of the equations involved in an inference. The irreducibility predicates simulate redundancy criteria based on reducibility (such as prime superposition and Blocking in Basic Completion) and the disequality predicates simulate the notion of subsumed critical pairs; in addition, since constraints are passed along with equations, we can perform hereditary versions of all these redundancy checks. This combines in one consistent framework stronger versions of all practical critical pair criteria. We also provide a rigorous analysis of the problem with completing sets of equations with initial constraints. Finally, an interesting consequence concerning the recalculation of critical pairs in completion procedures is discussed.

Details DOI