Skip to Main content Skip to Navigation
New interface
Reports (Research report)

Unification modulo Block Chaining

Siva Anantharaman 1 Christopher Bouchard 2 Paliath Narendran 2 Michael Rusinowitch 3 
3 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : 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.
Document type :
Reports (Research report)
Complete list of metadata
Contributor : Siva Anantharaman Connect in order to contact the contributor
Submitted on : Thursday, September 1, 2011 - 3:16:35 PM
Last modification on : Friday, November 18, 2022 - 9:24:19 AM


  • HAL Id : inria-00618376, version 1


Siva Anantharaman, Christopher Bouchard, Paliath Narendran, Michael Rusinowitch. Unification modulo Block Chaining. [Research Report] 2011. ⟨inria-00618376⟩



Record views