Search

Your search keyword '"Narendran, Paliath"' showing total 331 results
Start Over Author "Narendran, Paliath"
331 results on '"Narendran, Paliath"'

101. Finding canonical rewriting systems equivalent to a finite set of ground equations in polynomial time

Author

Gallier, Jean, Narendran, Paliath, Plaisted, David, Raatz, Stan, Snyder, Wayne, Goos, G., editor, Hartmanis, J., editor, Barstow, D., editor, Brauer, W., editor, Brinch Hansen, P., editor, Gries, D., editor, Luckham, D., editor, Moler, C., editor, Pnueli, A., editor, Seegmüller, G., editor, Stoer, J., editor, Wirth, N., editor, Lusk, Ewing, editor, and Overbeek, Ross, editor

Published
1988
Full Text
View/download PDF

105. Asymmetric Unification and the Combination Problem in Disjoint Theories

Author

Erbatur, Serdar, Kapur, Deepak, Marshall, Andrew, Meadows, Catherine, Narendran, Paliath, Ringeissen, Christophe, Department of Computer Science [Verona] (UNIVR | DI), Università degli studi di Verona = University of Verona (UNIVR), The University of New Mexico [Albuquerque], Naval Research Laboratory (NRL), University at Albany [SUNY], State University of New York (SUNY), Combination of approaches to the security of infinite states systems (CASSIS), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), INRIA, University of Verona (UNIVR), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)

Subjects
Physics::General Physics, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, High Energy Physics::Phenomenology, Computer Science::Programming Languages, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Computer Science::Computation and Language (Computational Linguistics and Natural Language and Speech Processing)
Abstract

Asymmetric unification is a new paradigm for unification modulo theories that introduces irreducibility constraints on one side of a unification problem. It has important applications in symbolic cryptographic protocol analysis, for which it is often necessary to put irreducibility constraints on portions of a state. However many facets of asymmetric unification that are of particular interest, including its behavior under combinations of disjoint theories, remain poorly understood. In this paper we give a new formulation of the method for unification in the combination of disjoint equational theories developed by Baader and Schulz that both gives additional insights into the disjoint combination problem in general, and furthermore allows us to extend the method to asymmetric unification, thus giving the first unification method for asymmetric unification in the combination of disjoint theories.

Published
2014

106. Hierarchical Combination of Unification Algorithms

Author

Erbatur, Serdar, Kapur, Deepak, Marshall, Andrew, Narendran, Paliath, Ringeissen, Christophe, Department of Computer Science [Verona] (UNIVR | DI), University of Verona (UNIVR), The University of New Mexico [Albuquerque], Naval Research Laboratory (NRL), University at Albany [SUNY], State University of New York (SUNY), Combination of approaches to the security of infinite states systems (CASSIS), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Università degli studi di Verona = University of Verona (UNIVR), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

International audience; A critical question in unification theory is how to obtain a unification algorithm for the combination of non-disjoint equational theories when there exists unification algorithms for the constituent theories. The problem is known to be difficult and can easily be seen to be undecidable in the general case. Therefore, previous work has focused on identifying specific conditions and methods in which the problem is decidable. We continue the investigation in this paper, building on previous combination results. We are able to develop a novel approach to the non-disjoint combination problem. The approach is based on a new set of restrictions and combination method such that if the restrictions are satisfied the method produces an algorithm for the unification problem in the union of non-disjoint equational theories.

Published
2013

109. String rewriting and security analysis: an extension of a result of Book and Otto

Author

Anantharaman, Siva, Narendran, Paliath, Rusinowitch, Michael, Laboratoire d'Informatique Fondamentale d'Orléans (LIFO), Ecole Nationale Supérieure d'Ingénieurs de Bourges-Université d'Orléans (UO), University at Albany [SUNY], State University of New York (SUNY), Combination of approaches to the security of infinite states systems (CASSIS), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Université d'Orléans (UO)-Ecole Nationale Supérieure d'Ingénieurs de Bourges, Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Protocol Security, Computer Science::Logic in Computer Science, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, String Rewriting, Regular Languages, Pushdown Automata, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Computer Science::Cryptography and Security
Abstract

In their seminal work Dolev and Yao used string rewriting to check protocol security against an active intruder. The main technical result and algorithm were improved by Book and Otto who formulated the security check in terms of an extended word problem for cancellation rules. We extend their main decidability result to a larger class of string rewrite systems called opt-monadic systems., Journal of Automata, Languages and Combinatorics, Volume 16, Numbers 2-4, 2011, 75-90

Published
2012

110. Unification modulo Block Chaining

Author

Anantharaman, Siva, Bouchard, Christopher, Narendran, Paliath, Rusinowitch, Michael, Laboratoire d'Informatique Fondamentale d'Orléans (LIFO), Université d'Orléans (UO)-Ecole Nationale Supérieure d'Ingénieurs de Bourges, University at Albany [SUNY], State University of New York (SUNY), Combination of approaches to the security of infinite states systems (CASSIS), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Ecole Nationale Supérieure d'Ingénieurs de Bourges-Université d'Orléans (UO), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)

Subjects
Block chaining, Equational unification, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, Protocol, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Computer Science::Cryptography and Security
Abstract

To appear.; We model block 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.

Published
2011

111. Unification Over Distributive Exponentiation (Sub)Theories

Author

Erbatur, Serdar, Marshall, Andrew M., Kapur, Deepak, and Narendran, Paliath

Abstract

Arithmetic operators are extensively used in cryptographic protocols. While a protocol using such operations may appear safe if semantic properties of these operations are not used by an intruder, the protocol can become vulnerable otherwise. Several such examples have been reported in the literature. The focus in this paper is on the modular exponentiation operator and its interaction with modular multiplication operators. Unification algorithms for theories involving exponentiation and multiplication operations play an important role in state exploration based approaches for finding attacks. This paper gives decidability results for unification problems for subtheories of exponentiation. The first property considered is the simplification of exponentiation when the exponent is an expression involving modular multiplication T. The second property investigated is the simplification of exponentiation in which the base expression is expressed using yet another modular multiplication *. Extensions of these theories in which modular multiplication T is associative and/or commutative are investigated. The approach used for developing unification algorithms is novel and hierarchical, in the sense a unification algorithm for properties of the multiplication operator can be employed as a plug-in into the inference rules for unification derived from equational properties of exponentiation with multiplication operations. A table summarizing all known results about theories of exponentiation is included as well., Journal of Automata, Languages and Combinatorics, Volume 16, Numbers 2-4, 2011, 109-140

Published
2011
Full Text
View/download PDF

113. Active Intruders with Caps

Author

Anatharaman, Siva, Lin, Hai, Lynch, Chris, Narendran, Paliath, Rusinowitch, Michael, Laboratoire d'Informatique Fondamentale d'Orléans (LIFO), Université d'Orléans (UO)-Ecole Nationale Supérieure d'Ingénieurs de Bourges, University at Albany [SUNY], State University of New York (SUNY), Combination of approaches to the security of infinite states systems (CASSIS), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Ecole Nationale Supérieure d'Ingénieurs de Bourges-Université d'Orléans (UO), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, Computer Science::Programming Languages, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Computer Science::Cryptography and Security
Abstract

International audience; We address the insecurity problem for cryptographic protocols, for an active intruder and a bounded number of sessions. By modeling each protocol step as a rigid Horn clause, and the intruder abilities as an equational theory over a convergent rewrite system, the problem of active intrusion is formulated as a Cap Unification problem. Cap Unification is an extension of Equational Unification: we look for a cap to be placed on a given set of terms, so that it unifies with a given term modulo the equational theory.

Published
2008

114. On extended regular expressions

Author

Carle, Benjamin, Narendran, Paliath, Scheriff, Colin, Contejean, Evelyne, and Évelyne Contejean

Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

In this paper we extend the work of Campeanu, Salomaa and Yu on extended regular expressions featured in the Unix utility egrep and the popular scripting language Perl. We settle the open issue of closure under intersection and provide an improved pumping lemma that will show that a larger class of languages is not recognizable by extended regular expressions.

Published
2007

128. On the equivalence problem for regular Thue systems

Author

Narendran, Paliath

Subjects
Formal Languages, Language Analysis, Scientific Research, Theory of Computation, Mathematics of Computing, Context-Free Grammars, Grammars, Models of Computation, Mathematical Models
Published
1986

129. Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis

Author

Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació, Universitat Politècnica de València. Escola Tècnica Superior d'Enginyeria Informàtica, European Regional Development Fund, Ministerio de Ciencia e Innovación, Generalitat Valenciana, National Science Foundation, EEUU, University at Albany, University of Illinois at Urbana-Champaign, Erbatur, Serdar, Escobar Román, Santiago, Kapur, Deepak, Liu, Zhiqiang, Lynch, Christopher A., Meadows, Catherine, Meseguer, José, Narendran, Paliath, Santiago Pinazo, Sonia, Sasse, Ralf, Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació, Universitat Politècnica de València. Escola Tècnica Superior d'Enginyeria Informàtica, European Regional Development Fund, Ministerio de Ciencia e Innovación, Generalitat Valenciana, National Science Foundation, EEUU, University at Albany, University of Illinois at Urbana-Champaign, Erbatur, Serdar, Escobar Román, Santiago, Kapur, Deepak, Liu, Zhiqiang, Lynch, Christopher A., Meadows, Catherine, Meseguer, José, Narendran, Paliath, Santiago Pinazo, Sonia, and Sasse, Ralf

Abstract

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-38574-2_16, We present a new paradigm for unification arising out of a technique commonly used in cryptographic protocol analysis tools that employ unification modulo equational theories. This paradigm relies on: (i) a decomposition of an equational theory into (R,E) where R is confluent, terminating, and coherent modulo E, and (ii) on reducing unification problems to a set of problems s=?ts=?t under the constraint that t remains R/E-irreducible. We call this method asymmetric unification. We first present a general-purpose generic asymmetric unification algorithm. and then outline an approach for converting special-purpose conventional unification algorithms to asymmetric ones, demonstrating it for exclusive-or with uninterpreted function symbols. We demonstrate how asymmetric unification can improve performanceby running the algorithm on a set of benchmark problems. We also give results on the complexity and decidability of asymmetric unification.

Published
2013

130. Effective symbolic protocol analysis via equational irreducibility conditions

Author

Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació, European Regional Development Fund, Ministerio de Ciencia e Innovación, Generalitat Valenciana, National Science Foundation, EEUU, Erbatur, Serdar, Escobar Román, Santiago, Kapur, Deepak, Liu, Zhiqiang, Lynch, Christopher, Meadows, Catherine, Meseguer, José, Narendran, Paliath, Santiago Pinazo, Sonia, Sasse, Ralf, Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació, European Regional Development Fund, Ministerio de Ciencia e Innovación, Generalitat Valenciana, National Science Foundation, EEUU, Erbatur, Serdar, Escobar Román, Santiago, Kapur, Deepak, Liu, Zhiqiang, Lynch, Christopher, Meadows, Catherine, Meseguer, José, Narendran, Paliath, Santiago Pinazo, Sonia, and Sasse, Ralf

Abstract

We address a problem that arises in cryptographic protocol analysis when the equational properties of the cryptosystem are taken into account: in many situations it is necessary to guarantee that certain terms generated during a state exploration are in normal form with respect to the equational theory. We give a tool-independent methodology for state exploration, based on unification and narrowing, that generates states that obey these irreducibility constraints, called contextual symbolic reachability analysis, prove its soundness and completeness, and describe its implementation in the Maude-NPA protocol analysis tool. Contextual symbolic reachability analysis also introduces a new type of unification mechanism, which we call asymmetric unification, in which any solution must leave the right side of the solution irreducible. We also present experiments showing the effectiveness of our methodology.

Published
2012

131. Rewriting Techniques & Applications

Author

Narendran, Paliath, Rusinowitch, Michaël, Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), and P. Narendran & M. Rusinowitch

Subjects
Reécriture, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], rewriting
Abstract

Ouvrage (éditeur).; This volume contains the proceedings of the conference RTA'99.

Published
1999

132. Unfication of Concept Terms in Description Logics

Author

Baader, Franz and Narendran, Paliath

Subjects
Description Logic, inference problem, Unification, concept description language, ddc:004, Beschreibungslogik, Inferenzproblem, Vereinheitlichung, Konzeptbeschreibungssprache
Abstract

Unification of concept terms is a new kind of inference problem for Description Logics, which extends the equivalence problem by allowing to replace certain concept names by concept terms before testing for equivalence. We show that this inference problem is of interest for applications, and present first decidability and complexity results for a small concept description language.

Published
1997

137. Cap unification

Author

Anantharaman, Siva, primary, Lin, Hai, additional, Lynch, Christopher, additional, Narendran, Paliath, additional, and Rusinowitch, Michael, additional

Published
2010
Full Text
View/download PDF

138. Any ground associative-commutative theory has a finite canonical system

Author

Narendran, Paliath, Rusinowitch, Michaël, INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria), and INRIA

Subjects
[INFO.INFO-OH]Computer Science [cs]/Other [cs.OH]
Abstract

Projet EURECA; We show that theories presented by a set of ground equations and with several associative-commutative symbols always admit a finite canonical system. In particular, the result is obtained through the construction of a reduction ordering which is AC-compatible and total on the set of congruence classes generated by the associativity and commutativity axioms. Such orderings are fundamental for deriving complete theorem proving strategies with built-in associative commutative unification.

Published
1990

140. Unification of Concept Terms in Description Logics: Revised Version

Author

Aachen University of Technology, Baader, Franz, Narendran, Paliath, Aachen University of Technology, Baader, Franz, and Narendran, Paliath

Abstract

Unification of concept terms is a new kind of inference problem for Description Logics, which extends the equivalence problem by allowing to replace certain concept names by concept terms before testing for equivalence. We show that this inference problem is of interest for applications, and present first decidability and complexity results for a small concept description language., This revised version of LTCS-Report 97-02 provides a stronger complexity result in Section 6. An abridged version will appear in Proc. ECAI'98 .

Published
1998

141. Unification of Concept Terms in Description Logics: Revised Version

Author

Baader, Franz, Narendran, Paliath, Baader, Franz, and Narendran, Paliath

Abstract

Unification of concept terms is a new kind of inference problem for Description Logics, which extends the equivalence problem by allowing to replace certain concept names by concept terms before testing for equivalence. We show that this inference problem is of interest for applications, and present first decidability and complexity results for a small concept description language., This revised version of LTCS-Report 97-02 provides a stronger complexity result in Section 6. An abridged version will appear in Proc. ECAI'98 .

Published
1998

143. Unfication of Concept Terms in Description Logics

Author

Aachen University of Technology, Baader, Franz, Narendran, Paliath, Aachen University of Technology, Baader, Franz, and Narendran, Paliath

Abstract

Unification of concept terms is a new kind of inference problem for Description Logics, which extends the equivalence problem by allowing to replace certain concept names by concept terms before testing for equivalence. We show that this inference problem is of interest for applications, and present first decidability and complexity results for a small concept description language.

Published
1997

144. Intruders with Caps.

Author

Hutchison, David, Kanade, Takeo, Kittler, Josef, Kleinberg, Jon M., Mattern, Friedemann, Mitchell, John C., Naor, Moni, Nierstrasz, Oscar, Pandu Rangan, C., Steffen, Bernhard, Sudan, Madhu, Terzopoulos, Demetri, Tygar, Doug, Vardi, Moshe Y., Weikum, Gerhard, Baader, Franz, Anantharaman, Siva, Narendran, Paliath, and Rusinowitch, Michael

Abstract

In the analysis of cryptographic protocols, a treacherous set of terms is one from which an intruder can get access to what was intended to be secret, by adding on to the top of a sequence of elements of this set, a cap formed of symbols legally part of his/her knowledge. In this paper, we give sufficient conditions on the rewrite system modeling the intruder's abilities, such as using encryption and decryption functions, to ensure that it is decidable if such caps exist. The following classes of intruder systems are studied: linear, dwindling, Δ-strong, and optimally reducing; and depending on the class considered, the cap problem ("find a cap for a given set of terms") is shown respectively to be in P, NP-complete, decidable, and undecidable. [ABSTRACT FROM AUTHOR]

Published
2007
Full Text
View/download PDF

146. A Unification Algorithm for Analysis of Protocols with Blinded Signatures.

Author

Hutter, Dieter, Stephan, Werner, Kapur, Deepak, Narendran, Paliath, and Wang, Lida

Abstract

Analysis of authentication cryptographic protocols, particularly finding flaws in them and determining a sequence of actions that an intruder can take to gain access to the information which a given protocol purports not to reveal, has recently received considerable attention. One effective way of detecting flaws is to hypothesize an insecure state and determine whether it is possible to get to that state by a legal sequence of actions permitted by the protocol from some legal initial state which captures the knowledge of the principals and the assumptions made about an intruder's behavior. Relations among encryption and decryption functions as well as properties of number theoretic functions used in encryption and decryption can be specified as rewrite rules. This, for example, is the approach used by the NRL Protocol Analyzer, which uses narrowing to reason about such properties of cryptographic and number-theoretic functions. Following [15], a related approach is proposed here in which equation solving modulo most of these properties of cryptographic and number-theoretic functions is done by developing new unification algorithms for such theories. A new unification algorithm for an equational theory needed to reason about protocols that use the Diffie-Hellman algorithm is developed. In this theory, multiplication forms an abelian group; exponentiation function distributes over multiplication, and exponents can commute. This theory is useful for analyzing protocols which use blinded signatures. It is proved that the unification problem over this equational theory can be reduced to the unification problem modulo the theory of abelian groups with commuting homomorphisms with an additional constraint. Baader's unification algorithm for the theory of abelian groups with commuting homomorphisms, which reduces the unification problem to solving equations over the polynomial ring over the integers with the commuting homomorphisms serving as indeterminates, is generalized to give a unification algorithm over the theory of abelian groups with commuting homomorphism with a linear constraint. It is also shown that the unification problem over a (simple) extension of the equational theory considered here (which is also an extension of the equational theory considered in [15]) is undecidable. [ABSTRACT FROM AUTHOR]

Published
2005

147. An E-unification Algorithm for Analyzing Protocols That Use Modular Exponentiation.

Author

Goos, Gerhard, Hartmanis, Juris, van Leeuwen, Jan, Nieuwenhuis, Robert, Kapur, Deepak, Narendran, Paliath, and Wang, Lida

Abstract

Modular multiplication and exponentiation are common operations in modern cryptography. Unification problems with respect to some equational theories that these operations satisfy are investigated. Two different but related equational theories are analyzed. A unification algorithm is given for one of the theories which relies on solving syzygies over multivariate integral polynomials with noncommuting indeterminates. For the other theory, in which the distributivity property of exponentiation over multiplication is assumed, the unifiability problem is shown to be undecidable by adapting a construction developed by one of the authors to reduce Hilbert's 10th problem to the solvability problem for linear equations over semi-rings. A new algorithm for computing strong Gröbner bases of right ideals over the polynomial ring Z is proposed; unlike earlier algorithms proposed by Baader as well as by Madlener and Reinert which work only for right admissible term orderings with the boundedness property, this algorithm works for any right admissible term ordering. The algorithms for some of these unification problems are expected to be integrated into Naval Research Lab.'s Protocol Analyzer (NPA), a tool developed by Catherine Meadows, which has been successfully used to analyze cryptographic protocols, particularly emerging standards such as the Internet Engineering Task Force's (IETF) Internet Key Exchange [11] and Group Domain of Interpretation [12] protocols. Techniques from several different fields — particularly symbolic computation (ideal theory and Gröebner basis algorithms) and unification theory — are thus used to address problems arising in state-based cryptographic protocol analysis. [ABSTRACT FROM AUTHOR]

Published
2003
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results