Cryptology ePrint Archive: Report 2005/467

A Probabilistic Hoare-style logic for Game-based Cryptographic Proofs (Extended Version)

Ricardo Corin and Jerry den Hartog

Abstract: We extend a Probabilistic Hoare-style logic to formalize game-based cryptographic proofs. Our approach provides a systematic and rigorous framework, thus preventing errors from being introduced. We illustrate our technique by proving semantic security of ElGamal.

Category / Keywords: Games, Hoare logic, Programming languages

Publication Info: To appear in ICALP 2006 Track C

Date: received 23 Dec 2005, last revised 26 Apr 2006

Contact author: corin at cs utwente nl

Available formats: PDF | BibTeX Citation

Version: 20060426:185139 (All versions of this report)

Discussion forum: Show discussion | Start new discussion