Title: CAP UNIFICATION : A Tool for Crypto Protocol Analysis
Speaker: Professor Siva ANANTHARAMAN
　　　　 University of ORLEANS, France
Time:　  4pm, Monday April 12
Venue:　 Lecture room, Lab for 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. 

About the speaker:

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