Documentation

Complexity.Crypto.Computational.SIS.Basic

The short integer solution problem with power-of-two moduli #

A short integer solution ([Ajt96]) for a matrix A ∈ ℤ_q^{n×ι} and a bound β is a nonzero integer vector z with every coordinate in [-β, β] and A z ≡ 0 (mod q) (SIS.IsSolution). It is a predicate for any modulus and index types, so that protocols can extract solutions for matrices such as [A | T].

The SIS experiment draws a uniform A ∈ ℤ_q^{n×m} with q = 2 ^ w, and gives a program the unary security parameter and the row-major binary word of A, as for DecisionLWE. The program answers with m residues of w bits each, read through their centered representatives in (-q/2, q/2] (SIS.decode), and wins when these form a short integer solution. SIS n m w β asserts that every uniform strict PPT program wins with negligible probability.

The centered reading loses nothing when 2 β < q: every short integer solution is decoded from the word of its own residues (SIS.decode_toBinary). For positive width w > 0, bounds at least 2 ^ (w - 1) make the experiment easy once m > n: every centered nonzero kernel vector modulo q then qualifies, and 2 ^ (w - 1) times a nonzero kernel vector modulo 2 is one. At width zero the decoder always returns the zero integer vector, so the experiment always rejects, even when nonzero integer SIS solutions exist modulo 1.

SIS is an explicit computational hardness hypothesis against uniform classical strict PPT programs, not a theorem. It asserts hardness for no particular parameters, and no worst-case lattice reduction is formalized. Moduli that are not powers of two and module SIS need other encodings and are not covered.

Main definitions #

Main results #

References #

source
def Cslib.Crypto.SIS.IsSolution {q : ℕ} {ρ : Type u_1} {ι : Type u_2} [Fintype ι] (A : Matrix ρ ι (ZMod q)) (β : ℕ) (z : ι → ℤ) :
Prop

z is a short integer solution for A: it is nonzero, every coordinate lies in [-β, β], and A z ≡ 0 (mod q).

Instances For
    source
    @[instance_reducible]
    instance Cslib.Crypto.SIS.instDecidableIsSolutionOfFintype {q : ℕ} {ρ : Type u_1} {ι : Type u_2} [Fintype ρ] [Fintype ι] (A : Matrix ρ ι (ZMod q)) (β : ℕ) (z : ι → ℤ) :
    Decidable (IsSolution A β z)
    source
    def Cslib.Crypto.SIS.decode (m w : ℕ) (word : List Bool) :
    Fin m → ℤ

    Read a word as m residues modulo 2 ^ w, of w low-order-first bits each, lifted to their centered representatives. Missing bits are false, and excess bits are ignored.

    Instances For
      source
      theorem Cslib.Crypto.SIS.decode_toBinary {m w β : ℕ} (hβ : 2 * β < 2 ^ w) {z : Fin m → ℤ} (hz : ∀ (i : Fin m), |z i| ≤ ↑β) :
      decode m w (Matrix.toBinary (Matrix.of fun (x : Fin 1) (i : Fin m) => ↑(z i))) = z

      When 2 β < 2 ^ w, a vector with coordinates in [-β, β] is decoded from the word of its residues. In particular the SIS experiment loses no integer solution for such bounds.

      source
      noncomputable def Cslib.Crypto.SIS.game (n m w β : ℕ → ℕ) (adversary : ℕ → List Bool → ProbComp (List Bool)) (security : ℕ) :
      Game

      The SIS experiment: draw a uniform A ∈ ℤ_q^{n×m} with q = 2 ^ w, give the adversary the unary security parameter and the binary word of A, and accept when its answer decodes to a short integer solution with bound β.

      Instances For
        source
        def Cslib.Crypto.SIS (n m w β : ℕ → ℕ) :
        Prop

        The SIS hardness hypothesis for the exact dimension, number of columns, binary modulus width and bound: every uniform strict PPT program, given the unary security parameter and the encoded uniform matrix, finds a short integer solution with negligible probability. This is a hypothesis against classical adversaries, not a theorem of hardness.

        Instances For