CAP UNIFICATION : A Tool for Crypto Protocol Analysis

Title: CAP UNIFICATION : A Tool for Crypto Protocol Analysis
Speaker: Professor Siva ANANTHARAMAN （University of ORLEANS, France）
Time: 4:00pm,Monday，April 12th
Venue: Lecture Room 334,State Key Lab of Computer Science, Level 3 Building #5, Institute of Software, CAS

Abstract:Syntactic Unification (of J. Herbrand, J. A. Robinson) underlies almost all formal deduction techniques. Unification is said to be semantic when the issue is one of unifying two given terms not syntactically, but modulo some given equational theory. In this talk, we first illustrate how this notion can be extended to one called Cap Unification (modulo some given “Intruder Theory”), that allows to model in a natural manner cryptographic protocols and also to analyze them from the security viewpoint.

Now, it is necessary for such an analysis that unification modulo the intruder theory be decidable. So we also present, briefly, a decision procedure for solving this problem — assuming that the protocols employ the so-called ECB (or `homomorphic’) mode for encrypting the messages: messages decomposed into blocks are encrypted block-wise.

Biography:
Siva ANANTHARAMAN is currently Emeritus Professor at the University of ORLEANS (France). He did his `Docteur-ès-Scinces’ (D.Sc) in Algebraic Geometry/Comutative Algebra, at Orsay, University Paris-XI; switched to Computer Science in 1990.
Domains of Interest and Research:
– Automated Deduction (Theorem Proving),
– AC-rewriting/AC-matching based Software; application to static analysis (for certain classes) of programs
– Unification modulo theories; application to Crypto-Protool Analysis
– Process Algebra with Cost funtions
– Tree/Dag automata for the (security) analysis of compressed, unstructured (XML-) documents