Formalizing Coppersmith's method in Isabelle/HOL
type: Item
instance of: scholarly article
title: Formalizing Coppersmith's method in Isabelle/HOL
DOI: 10.1007/978-3-031-66997-2_8
author: Katherine Kosaian
author: Yong Kiam Tan
author: Kristin Yvonne Rozier
publication date: 2024-12-04T00:00:00Z
Mathematics Subject Classification ID: 68Vxx
zbMATH DE Number: 7953762
zbMATH Keywords: Coppersmith's method
zbMATH Keywords: theorem proving
zbMATH Keywords: LLL basis reduction
zbMATH Keywords: cryptography
MaRDI profile type: Publication
cites work: Locales: a module system for mathematical theories
cites work: Computer-Aided Security Proofs for the Working Cryptographer
cites work: CryptHOL: game-based proofs in higher-order logic
cites work: Q4783731
cites work: Verified cryptographic code for everybody
cites work: A Verified Efficient Implementation of the LLL Basis Reduction Algorithm
cites work: Formalising \(\varSigma\)-protocols and commitment schemes using crypthol
cites work: Finding a Small Root of a Univariate Modular Equation
cites work: A formalization of the LLL basis reduction algorithm
cites work: Mathematics of public key cryptography.
cites work: Q4400575
cites work: Critical perspectives on provable security: fifteen years of ``another look'' papers
cites work: Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started
cites work: Verification of NP-Hardness Reduction Functions for Exact Lattice Problems
cites work: Q3933739
cites work: Formally verified certificate checkers for hardest-to-round computation
cites work: The LLL algorithm. Survey and applications
cites work: The foundation of a generic theorem prover
cites work: A method for obtaining digital signatures and public-key cryptosystems
cites work: Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
cites work: Factoring polynomials and the knapsack problem
description: scientific article; zbMATH DE number 7953762