Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3
Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3
复制标题
密码标准的机器检查证明：海绵的不可区分性和 SHA-3 的安全高保证实现
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Pierre
中科院分区：
文献类型：
--
作者：
J. Almeida;Cécile Baritel;M. Barbosa;G. Barthe;François Dupressoir;B. Grégoire;Vincent Laporte;Tiago Oliveira;Alley Stoughton;Pierre
我们提出了一个高保证和高速实现的SHA-3哈希函数。我们的实现是用Jasmin编程语言编写的，并在EasyCrypt证明助手中正式验证了功能正确性，可证明安全性和抗定时攻击性。我们的实现是第一个同时实现四个理想的属性（效率，正确性，可证明的安全性和侧通道保护）的一个非平凡的密码原语。具体来说，我们的机械化证明表明：1）SHA-3哈希函数与随机预言机不可区分，因此可以抵抗碰撞，第一和第二原像攻击; 2）SHA-3哈希函数可以通过矢量化的x86实现正确实现。此外，在一个理想化的时间泄漏模型中，该实现可证明地免受时间攻击。证明包括新的EasyCrypt库的独立利益的可编程随机预言机和模块不可微性证明。
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.
影响因子：
6.9
作者：
J. Almeida;M. Barbosa;G. Barthe;François Dupressoir;M. Emmi
通讯作者：
J. Almeida;M. Barbosa;G. Barthe;François Dupressoir;M. Emmi