Automated verification of correctness for masked arithmetic programs
From MaRDI portal
Publication:6535686
DOI10.1007/978-3-031-37709-9_13zbMATH Open1547.68126MaRDI QIDQ6535686FDOQ6535686
Taolue Chen, Mingyang Liu, Fu Song
Publication date: 1 February 2024
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)
Cites Work
- Dafny: An Automatic Program Verifier for Functional Correctness
- EasyCrypt: A Tutorial
- How to share a secret
- Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems
- Title not available (Why is that?)
- Statistical Analysis of Second Order Differential Power Analysis
- Title not available (Why is that?)
- PRESENT: An Ultra-Lightweight Block Cipher
- On theories with a combinatorial definition of 'equivalence'
- Randomness Complexity of Private Circuits for Multiplication
- Advances in Cryptology - CRYPTO 2003
- Title not available (Why is that?)
- Provably Secure Higher-Order Masking of AES
- Title not available (Why is that?)
- The SKINNY Family of Block Ciphers and Its Low-Latency Variant MANTIS
- Higher-Order Side Channel Security and Mask Refreshing
- Consolidating Masking Schemes
- Higher-Order Masking Schemes for S-Boxes
- Title not available (Why is that?)
- Reconciling $$d+1$$ Masking in Hardware and Software
- Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model
- Formal verification of masked hardware implementations in the presence of glitches
- Quantitative Verification of Masked Arithmetic Programs Against Side-Channel Attacks
- Hoare Logic for Realistically Modelled Machine Code
- A Fast and Provably Secure Higher-Order Masking of AES S-Box
- Hardware Private Circuits: From Trivial Composition to Full Verification
- Dijkstra monads for free
- \textsc{SCInfer}: refinement-based verification of software countermeasures against side-channel attacks
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)
