Automated Verification of Asymmetric Encryption
Staff - Faculty of Informatics
Start date: 19 October 2009
End date: 20 October 2009
The Faculty of Informatics is pleased to announce a seminar given by Chan Ngo
DATE: Monday, October 19th, 2009
PLACE: USI Università della Svizzera italiana, room SI-015, Informatics building (Via G. Buffi 13)
TIME: 13.30
ABSTRACT:
Two major directions in cryptography have developed: formal and computational. In formal approaches, the knowledge of attackers is often treated in terms of message deducibility and indistinguishability relations. The formal approach uses simple, manageable formal languages to describe cryptographic protocols; this approach is amenable to automation, suitable for computer tools, but its accuracy is often unclear. The computational approach is harder to handle mathematically, involves probability theory and considers limits in computing power; proofs are done by hand, but it is more accurate, hence widely accepted.Much effort has been made to bridge the gap between the two approaches.As the previous work has shown that using static equivalence from cryptographic pi calculus as a notion of formal indistinguishability yields the soundness of the interpretations. Bana et al. have introduced Formal Indistinguishability Relations (FIR), as an abstraction of computational indistinguishability. In this work, we extend the notion of FIR to cope with the Random Oracle Model (ROM) to prove security notions as IND-CPA. Indeed, when dealing with hash functions in the ROM and one-way functions, it is important to correctly abstract the notion of weak secrecy. To fix these problems, we consider pairs of formal indistinguishability relations and formal non-deducibility relations. We provide a general framework along with general theorems, that ensure soundness of our approach and then we use our new frameworkto verify several examples of encryption schemes among which the construction of Bellare Rogaway and Hashed ElGamal.
BIO:
Chan received a B.E. degree in Computer Engineering from Hanoi University of Technology, Vietnam in 2005 and then M.S degree (DEA in France) in Computer Science from University of Grenoble 1. His current research interests are information security, formal methods, and verificatio
HOST: Prof. Natasha Sharygina
