Boston University Libraries OpenBU
    JavaScript is disabled for your browser. Some features of this site may not work without it.
    View Item 
    •   OpenBU
    • BU Open Access Articles
    • BU Open Access Articles
    • View Item
    •   OpenBU
    • BU Open Access Articles
    • BU Open Access Articles
    • View Item

    Machine-checked proofs for cryptographic standards

    Thumbnail
    Date Issued
    2019-11-06
    Publisher Version
    10.1145/3319535.3363211
    Author(s)
    Almeida, José Bacelar
    Baritel-Ruet, Cécile
    Barbosa, Manuel
    Barthe, Gilles
    Dupressoir, François
    Grégoire, Benjamin
    Laporte, Vincent
    Oliveira, Tiago
    Stoughton, Alley
    Strub, Pierre-Yves
    Share to FacebookShare to TwitterShare by Email
    Export Citation
    Download to BibTex
    Download to EndNote/RefMan (RIS)
    Metadata
    Show full item record
    Permanent Link
    https://hdl.handle.net/2144/40690
    Version
    Accepted manuscript
    Citation (published version)
    José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub. 2019. "Machine-checked proofs for cryptographic standards." Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. CCS '19: 2019 ACM SIGSAC Conference on Computer and Communications Security. https://doi.org/10.1145/3319535.3363211
    Abstract
    We present a high-assurance and high-speed implementation of the SHA-3 hash function. Our implementation is written in the Jasmin programming language, and is formally verified for functional correctness, provable security and timing attack resistance in the EasyCrypt proof assistant. Our implementation is the first to achieve simultaneously the four desirable properties (efficiency, correctness, provable security, and side-channel protection) for a non-trivial cryptographic primitive. Concretely, our mechanized proofs show that: 1) the SHA-3 hash function is indifferentiable from a random oracle, and thus is resistant against collision, first and second preimage attacks; 2) the SHA-3 hash function is correctly implemented by a vectorized x86 implementation. Furthermore, the implementation is provably protected against timing attacks in an idealized model of timing leaks.The proofs include new EasyCrypt libraries of independent interest for programmable random oracles and modular indifferentiability proofs.
    Rights
    This work was determined by OpenBU staff to be the final author draft submitted using a template provided by the Association for Computing Machinery. It appears in OpenBU under the auspices of Boston University's Open Access Policy. Please write to open-help@bu.edu with any questions.
    Collections
    • CAS: Computer Science: Scholarly Papers [187]
    • BU Open Access Articles [3730]


    Boston University
    Contact Us | Send Feedback | Help
     

     

    Browse

    All of OpenBUCommunities & CollectionsIssue DateAuthorsTitlesSubjectsThis CollectionIssue DateAuthorsTitlesSubjects

    Deposit Materials

    LoginNon-BU Registration

    Statistics

    Most Popular ItemsStatistics by CountryMost Popular Authors

    Boston University
    Contact Us | Send Feedback | Help