**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