Events & News
Colloquium
| Category | Lecture |
| Date | Friday, June 22, 2012 |
| Time | 10:00 am |
| Concludes | 11:00 am |
| Location | Gould-Simpson 906 |
| Speaker | Zhang Yu |
Formal Analysis of Security Protocols and Cryptography
In this talk I will first review the formal analysis techniques for security protocols and cryptography. In particular, I will show how program equivalence can be used to formalize security properties, in both symbolic models and computational models.
The second part of the talk will introduce a logic framework FunCrypt that we have developed based on Hofmann's SLR type system for characterizing polynomial-time computations. The logic supports formal reasoning of computational indistinguishability, which is an important notion in complexity-theoretic cryptography and is used to define many security criteria. We built a proof system that justify directly computational indistinguishability between programs and prove that the system is sound with respect to the standard definition of security. This enables automatization of the verification of (often complex) cryptographic proofs. We show that the system is applicable in cryptography by verifying several cryptographic constructions in our proof system, e.g., El-Gamal public key encryption and Blum-Blum-Shub PSG.