Equational Reasoning and Unification in Protocol Verification

Title:  Equational Reasoning and Unification in Protocol Verification

Speaker:  Christopher Lynch (Clarkson University) (http://people.clarkson.edu/~clynch/ )

Time: 10:00, Friday, 12th July, 2013

Venue: Lecture Room, 3rd Floor, Building #5, State Key Laboratory of  Computer Science, Institute of Software, Chinese Academy of Sciences

Cryptographic protocols are ubiquitous on the internet today.  Just as in the case of other software, users must be assured of the correctness of the protocols, even in the presence of malicious intruders.  A symbolic method has been developed to analyze the message passing of protocols and find attacks or show correctness under a certain model.  An advantage of the symbolic method is that it is thorough and can be automated.  However, the symbolic method ignores properties of the cryptographic algorithms.  We will discuss the symbolic method of cryptographic protocol analysis. We show how equational theories allow properties of the cryptographic algorithms to be taken into consideration.  A major part of the symbolic process involves unifying terms.  We develop new efficient methods for unifying terms under an equational theory.