Formalizing Coppersmith's method in Isabelle/HOL
From MaRDI portal
Cites work
- scientific article; zbMATH DE number 3750287 (Why is no real title available?)
- scientific article; zbMATH DE number 1182510 (Why is no real title available?)
- scientific article; zbMATH DE number 1842497 (Why is no real title available?)
- A formalization of the LLL basis reduction algorithm
- A method for obtaining digital signatures and public-key cryptosystems
- A verified efficient implementation of the LLL basis reduction algorithm
- Computer-Aided Security Proofs for the Working Cryptographer
- Critical perspectives on provable security: fifteen years of ``another look papers
- CryptHOL: game-based proofs in higher-order logic
- Factoring polynomials and the knapsack problem
- Finding a small root of a univariate modular equation
- Formalising \(\varSigma\)-protocols and commitment schemes using crypthol
- Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
- Formally verified certificate checkers for hardest-to-round computation
- Locales: a module system for mathematical theories
- Mathematics of public key cryptography.
- The LLL algorithm. Survey and applications
- The foundation of a generic theorem prover
- Verification of NP-Hardness Reduction Functions for Exact Lattice Problems
- Verified cryptographic code for everybody
This page was built for publication: Formalizing Coppersmith's method in Isabelle/HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6648162)
