Certifying assembly with formal security proofs: the case of BBS

DOI10.1016/j.scico.2011.07.003zbMath1243.68146OpenAlexW2080143965MaRDI QIDQ436406

Kiyoshi Yamada, Reynald Affeldt, David E. Nowak

Publication date: 20 July 2012

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2011.07.003

zbMATH Keywords

provable securityHoare logicCoqassembly languagePRNG

Mathematics Subject Classification ID

Related Items (6)

Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory ⋮ Transfinite Constructions in Classical Type Theory ⋮ Unnamed Item ⋮ Certifying assembly with formal security proofs: the case of BBS ⋮ A Calculus for Game-Based Security Proofs ⋮ Formal security proofs with minimal fuss: implicit computational complexity at work

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Certifying assembly with formal security proofs: the case of BBS
• Introduction to cryptography. Principles and applications.
• A compositional natural semantics and Hoare logic for low-level languages
• Proving pointer programs in higher-order logic
• Modular Multiplication Without Trial Division
• Formal Proof of Provable Security by Game-Playing in a Proof Assistant
• A Simple Unpredictable Pseudo-Random Number Generator
• Formal certification of code-based cryptographic proofs
• A Formal Language for Cryptographic Pseudocode
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Certifying assembly with formal security proofs: the case of BBS