Algorithm and Information Colloquium (AIC)
　　
Title: A logic for reasoning about computational indistinguishability--- Cryptography viewed from logic and programming languages

Speaker: Yu Zhang 

Time: 16:30 – 17:30, April 7, 2010, Wednesday

Place:  Lecture Room, Level 3, Building No. 5, Institute of Software

Tea time: 16:00 – 16:30, Common Room, Level 3, Building No. 5

Abstract:

Computational indistinguishability is an important notion in complexity-theoretic cryptography and is used to define many security criteria. However, in traditional cryptography, proving computational indistinguishability is usually informal and becomes error-prone when cryptographic constructions are getting complex. I will present a formal proof system based on an extension of Hofmann’s SLR language, which can capture probabilistic polynomial-time computations through typing and is sufficient for expressing cryptographic constructions. We in particular define rules that justify directly the computational indistinguishability between programs and prove that these rules are sound with respect to the set-theoretic semantics, hence the standard definition of security.

The novelty of the work is the application of results from implicit complexity (we are using SLR and safe recursion), an area not yet being noticed in security and cryptography. With the aide of techniques from programming languages, our system can well manage the complexity issue in cryptographic proofs.

Our recent work has extended the system with a notion of game indistinguishability, which targets the game based style of proofs that are advocated by many cryptographers. We also show that the system is applicable in cryptography by verifying several cryptographic constructions in our proof system, e.g., Goldreich and Micali’s construction of pseudorandom generator, El-Gamal encryption, Blum-Blum-Shub PSG, and so on.

Biography:

Zhang Yu is an associate professor of Laboratory for Computer Science, ISCAS. He received his Ph.D. from Ecole Normale Superieure de Cachan in France in 2005. After that, he had been working in French Commissariat of Atomic Energy, INRIA, and Macao University of Science and Technology. His research interests include logic, programming languages, foundation
for computer security, and formal methods.