### Abstract

This article formalizes the NP-hardness proofs of the Closest Vector Problem (CVP) and the Shortest Vector Problem (SVP) in maximum norm as well as the CVP in any p-norm for p>=1. CVP and SVP are two fundamental problems in lattice theory. Lattices are a discrete, additive subgroup of R^n and are used for lattice-based cryptography. The CVP asks to find the nearest lattice vector to a target. The SVP asks to find the shortest non-zero lattice vector. This entry formalizes the basic properties of lattices, the reduction from CVP to Subset Sum in both maximum and p-norm for a finite p with 1<= p and the reduction of SVP to Partition using the Bounded Homogeneous Linear Equations problem (BHLE) as an intermediate step. The formalization uncovered a number of problems with the existing proofs in the literature.

### License

BSD License

### Topics

- Computer science/Security/Cryptography
- Mathematics/Misc

### Session CVP_Hardness

- Reduction
- Lattice_int
- Partition
- Subset_Sum
- CVP_p
- infnorm
- CVP_vec
- Digits_int
- Additional_Lemmas
- BHLE
- SVP_vec

### Depends on

- The BKR Decision Procedure for Univariate Real Arithmetic
- The Factorization Algorithm of Berlekamp and Zassenhaus
- Matrices, Jordan Normal Forms, and Spectral Radius Theory
- A verified LLL algorithm

## Cite

×

CVP_Hardness-AFP

    @article{CVP_Hardness-AFP,
      author  = {Katharina Kreuzer},
      title   = {Hardness of Lattice Problems},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/CVP_Hardness.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Feb 5, 2023 : Isabelle2022