Information Trust Institute block of abstract images
Information Trust Institute block of abstract images

Equivalence Properties of Cryptographic Protocols and Their Formal Verification


Rohit Chadha
Assistant Professor, Computer Science
University of Missouri

Watch This Session

(Video runs from 02:24:40 to 03:13:58)


The ubiquitous use of Internet has raised serious concerns of privacy and trust. In order to address these concerns, cryptographic protocols are often deployed. A cryptographic protocol is a distributed program that uses cryptographic techniques to achieve security goals. However, the design of such protocols is error-prone and serious bugs are often discovered. Thus, techniques and tools that can "prove" correctness of such protocols are an active area of research. Indistinguishability properties are important in specifying and verifying privacy properties of cryptographic protocols. In particular, they are needed to model anonymity properties, strong versions of confidentiality and resistance to offline guessing attacks, and can be conveniently modeled using process equivalences. In the lecture, we shall discuss the formal modeling of such equivalences and present an automated tool, AKISS, that verifies such properties for a bounded number of protocol sessions. This tool, developed in collaboration with Stefan Ciobaca and Steve Kremer, is based on formal logic techniques and has been used to verify voter privacy in an electronic voting protocol. The use of the tool will be demonstrated through examples.

Suggested Reading:

"Automated Verication of Equivalence Properties of Cryptographic Protocols"


Rohit Chadha is an assistant professor in the Department of Computer Science. His interests lie in security and program verification. He has an extensive experience in these areas, and has collaborated with several research teams across the world. His research on formalization and proofs of security properties of contract-signing protocols and verification of probabilistic programs has been highly cited.