Formalizing the hidden number problem in Isabelle/HOL
From MaRDI portal
Cites work
- A tale of three signatures: practical attack of ECDSA with wNAF
- A verified efficient implementation of the LLL basis reduction algorithm
- Biased nonce sense: lattice attacks against weak ECDSA signatures in cryptocurrencies
- Constructive cryptography -- a new paradigm for security definitions and proofs
- CryptAttackTester: high-assurance attack analysis
- CryptHOL: game-based proofs in higher-order logic
- Extended Hidden Number Problem and Its Cryptanalytic Applications
- Formal certification of code-based cryptographic proofs
- Formalising \(\varSigma\)-protocols and commitment schemes using crypthol
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
- From Indifferentiability to Constructive Cryptography (and Back)
- Hardness of computing the most significant bits of secret keys in Diffie-Hellman and related schemes
- scientific article; zbMATH DE number 1588483 (Why is no real title available?)
- scientific article; zbMATH DE number 3750287 (Why is no real title available?)
- scientific article; zbMATH DE number 2081057 (Why is no real title available?)
- scientific article; zbMATH DE number 1842493 (Why is no real title available?)
- Isabelle/HOL. A proof assistant for higher-order logic
- Locales: a module system for mathematical theories
- On Lovász' lattice reduction and the nearest lattice point problem
- The hidden number problem with small unknown multipliers: cryptanalyzing MEGA in six queries and other applications
- The insecurity of the digital signature algorithm with partially known nonces
- The insecurity of the elliptic curve digital signature algorithm with partially known nonces
- Verification of NP-Hardness Reduction Functions for Exact Lattice Problems
This page was built for publication: Formalizing the hidden number problem in Isabelle/HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7323673)
