Verification of Authentication Protocols
Ms. Madhumita Chatterjee,
M.Tech,
1999,
76 pp.
Department of
Computer Science and Engineering
Indian Institute of Technology Bombay,
Powai, Mumbai 400 076.
Supervisor(s):
Prof G. Sivakumar
Authentication protocols are the basis of security in many
distributed systems, and it is therefore essential to ensure that these
protocols function correctly. Unfortunately, cryptographic protocol design has
been error prone and many popular protocols have been shown to have flaws.
Different methods for verification of such protocols have been proposed over the
years.
In this project we have used an equational logic to model authentication
protocols. This logic is based on belief and trust, similar to the Ban logic.
A set of inference rules have been specified which infer new beliefs
from an initial set of beliefs depending on the type of encrypted message seen.
The protocols and their properties specified in this equational logic have then
been given as input to the equational theorem prover RRL, which has been success
fully used for automatic verification of the properties specified.
Experiments with several well-known protocols such as Kerberos, Needham
Schroeder and Otway Rees yielded the expected results.