A Probabilistic Hoare-style logic for game-based cryptographic proofs

被引:0
|
作者
Gorin, Ricardo
den Hartog, Jerry
机构
来源
关键词
D O I
暂无
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
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.
引用
收藏
页码:252 / 263
页数:12
相关论文
共 31 条
  • [1] Probabilistic Modal Kleene Algebra and Hoare-style Logic
    Qiao, Rui
    Wu, Jinzhao
    Gao, Xinyan
    ICNC 2008: FOURTH INTERNATIONAL CONFERENCE ON NATURAL COMPUTATION, VOL 3, PROCEEDINGS, 2008, : 652 - +
  • [2] Towards mechanized correctness proofs for cryptographic algorithms Axiomatization of a probabilistic Hoare style logic
    den Hartog, Jerry
    SCIENCE OF COMPUTER PROGRAMMING, 2008, 74 (1-2) : 52 - 63
  • [3] Hoare-Style Logic for Unstructured Programs
    Lundberg, Didrik
    Guanciale, Roberto
    Lindner, Andreas
    Dam, Mads
    SOFTWARE ENGINEERING AND FORMAL METHODS, SEFM 2020, 2020, 12310 : 193 - 213
  • [4] Game-Based Automated Security Proofs for Cryptographic Protocols
    Gu Chunxiang
    Guang Yan
    Zhu Yuefei
    CHINA COMMUNICATIONS, 2011, 8 (04) : 50 - 57
  • [5] Unifying Refinement and Hoare-Style Reasoning in a Logic for Higher-Order Concurrency
    Turon, Aaron
    Dreyer, Derek
    Birkedal, Lars
    ACM SIGPLAN NOTICES, 2013, 48 (09) : 377 - 390
  • [6] Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs
    Nagy, Shaan
    Kim, Jinwoo
    Reps, Thomas
    D'Antoni, Loris
    Proceedings of the ACM on Programming Languages, 2024, 8 (OOPSLA2) : 113 - 139
  • [7] CryptHOL: Game-Based Proofs in Higher-Order Logic
    David A. Basin
    Andreas Lochbihler
    S. Reza Sefidgar
    Journal of Cryptology, 2020, 33 : 494 - 566
  • [8] CryptHOL: Game-Based Proofs in Higher-Order Logic
    Basin, David A.
    Lochbihler, Andreas
    Sefidgar, S. Reza
    JOURNAL OF CRYPTOLOGY, 2020, 33 (02) : 494 - 566
  • [9] A Calculus for Game-Based Security Proofs
    Nowak, David
    Zhang, Yu
    PROVABLE SECURITY, 2010, 6402 : 35 - +
  • [10] A framework for game-based security proofs
    Nowak, David
    INFORMATION AND COMMUNICATIONS SECURITY, PROCEEDINGS, 2007, 4681 : 319 - 333