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

Ricardo Corin; Jerry den Hartog

Paper 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.

Metadata

Available format(s): PDF
Publication info: Published elsewhere. To appear in ICALP 2006 Track C
Keywords: Games Hoare logic Programming languages
Contact author(s): corin @ cs utwente nl
History: 2006-04-26: last of 3 revisions; 2005-12-31: received; See all versions
Short URL: https://ia.cr/2005/467
License: CC BY

BibTeX

@misc{cryptoeprint:2005/467,
      author = {Ricardo Corin and Jerry den Hartog},
      title = {A Probabilistic Hoare-style logic for Game-based Cryptographic Proofs (Extended Version)},
      howpublished = {Cryptology {ePrint} Archive, Paper 2005/467},
      year = {2005},
      url = {https://eprint.iacr.org/2005/467}
}