Unification modulo Block Chaining

Siva Anantharaman; Christopher Bouchard; Paliath Narendran; Michael Rusinowitch

inria-00618376, version 1

Unification modulo Block Chaining

Siva Anantharaman () ¹, Christopher Bouchard ()^a^, 2, Paliath Narendran () ², Michael Rusinowitch () ³

(2011)

Résumé : 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.

a – SUNY, University at Albany (NY)
1 : Laboratoire d'Informatique Fondamentale d'Orléans (LIFO)
Université d'Orléans : EA4022 – Ecole Nationale Supérieure d'Ingénieurs de Bourges
2 : University at Albany
State university of New York
3 : CASSIS (INRIA Lorraine - LORIA / LIFC)
INRIA – CNRS : FRE2661 – Université de Franche-Comté – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)

inria-00618376, version 1
http://hal.inria.fr/inria-00618376
oai:hal.inria.fr:inria-00618376
Contributeur : Siva Anantharaman <>
Soumis le : Jeudi 1 Septembre 2011, 15:16:35
Dernière modification le : Jeudi 1 Septembre 2011, 15:16:35

Voir la fiche détaillée

Exporter

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="report"><head>Rapports</head>
<biblStruct type="report" xml:id="inria-00618376"><monogr>
<author><persName><forename>Siva</forename><surname>Anantharaman</surname></persName>
<affiliation>
<orgName type="laboratory">LIFO</orgName>
<orgName type="team">Laboratoire d'Informatique Fondamentale d'Orléans</orgName>
<country>FR</country>
<orgName type="institution">Université d'Orléans : EA4022</orgName>
<orgName type="institution">Ecole Nationale Supérieure d'Ingénieurs de Bourges</orgName>
</affiliation>
</author>
<author><persName><forename>Christopher</forename><surname>Bouchard</surname></persName>
<affiliation>
<orgName type="team">University at Albany</orgName>
<country>US</country>
<orgName type="institution">State university of New York</orgName>
</affiliation>
</author>
<author><persName><forename>Paliath</forename><surname>Narendran</surname></persName>
<affiliation>
<orgName type="team">University at Albany</orgName>
<country>US</country>
<orgName type="institution">State university of New York</orgName>
</affiliation>
</author>
<author><persName><forename>Michael</forename><surname>Rusinowitch</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA / LIFC</orgName>
<orgName type="team">CASSIS</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : FRE2661</orgName>
<orgName type="institution">Université de Franche-Comté</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<title type="main" level="m">Unification modulo Block Chaining</title><title type="main" level="m">Unification modulo Block Chaining</title><imprint><biblScope type="publicationDate">2011-09-01</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/inria-00618376</idno></biblStruct>
</listBibl>
</listBibl>