Automated verification of correctness for masked arithmetic programs

DOI10.1007/978-3-031-37709-9_13MaRDI QIDQ6535686zbMATH OpenFDO

Authors Mingyang Liu, Fu Song, Taolue Chen

Publication date 1 February 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-37709-9_13

Mathematics Subject Classification ID

Cryptography (94A60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Quantitative Verification of Masked Arithmetic Programs Against Side-Channel Attacks
• Verified Proofs of Higher-Order Masking
• Formal verification of side-channel countermeasures via elementary circuit transformations
• Formal verification of arithmetic masking in hardware and software
• Fast verification of masking schemes in characteristic two

Cites work

• scientific article; zbMATH DE number 1682693 (Why is no real title available?)
• scientific article; zbMATH DE number 5613976 (Why is no real title available?)
• scientific article; zbMATH DE number 1504808 (Why is no real title available?)
• scientific article; zbMATH DE number 1418307 (Why is no real title available?)
• scientific article; zbMATH DE number 7378548 (Why is no real title available?)
• A fast and provably secure higher-order masking of AES S-box
• Advances in Cryptology - CRYPTO 2003
• Consolidating masking schemes
• Dafny: an automatic program verifier for functional correctness
• Dijkstra monads for free
• EasyCrypt: a tutorial
• Formal verification of masked hardware implementations in the presence of glitches
• Hardware Private Circuits: From Trivial Composition to Full Verification
• Higher-order masking schemes for S-boxes
• Higher-order side channel security and mask refreshing
• Hoare Logic for Realistically Modelled Machine Code
• How to share a secret
• On theories with a combinatorial definition of 'equivalence'
• PRESENT: An Ultra-Lightweight Block Cipher
• Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model
• Provably secure higher-order masking of AES
• Quantitative Verification of Masked Arithmetic Programs Against Side-Channel Attacks
• Randomness complexity of private circuits for multiplication
• Reconciling \((d+1)\) masking in hardware and software
• Statistical Analysis of Second Order Differential Power Analysis
• The SKINNY Family of Block Ciphers and Its Low-Latency Variant MANTIS
• Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems
• \textsc{SCInfer}: refinement-based verification of software countermeasures against side-channel attacks

Cited in

(2)

• Quantitative Verification of Masked Arithmetic Programs Against Side-Channel Attacks
• Formal verification of arithmetic masking in hardware and software

This page was built for publication: Automated verification of correctness for masked arithmetic programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535686)