NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library BBS_Asm_CryptoProof

This file contains the proof of unpredictability of the implementation in Assembly of the Blum-Blum-Shub (BBS) pseudorandom bit generator. Security is based on the intractability of the quadratic residuosity problem.

Require Import Euclid List Znumtheory Zpow_facts Rbase.
Require Import ssreflect ssrbool.
Require Import ZArith_ext.
Require Import listbit.
Add LoadPath "./toolbox".
Require MiscLists BBS.
Add LoadPath "../cryptoasm".
Require bbs_encode_decode.

Local Close Scope Z_scope.

Lemma euclid_unique : forall m n q r q' r',
  0 < n -> m = q * n + r -> m = q' * n + r' -> n > r -> n > r' -> q = q' /\ r = r'.

Definition ceiling_div (m n : nat) (H : 0 < n) :=
  if eq_nat_dec (proj1_sig (modulo n H m)) O then
    proj1_sig (quotient n H m)
  else
    S (proj1_sig (quotient n H m)).

Lemma lt_0_ceiling_div : forall m n, 0 < m ->
  forall H : 0 < n, 0 < ceiling_div m n H.

Lemma le_mult_ceiling_div : forall m n (H:0<n), m <= n * ceiling_div m n H.

Local Open Scope Z_scope.

Lemma Zmult_le_lt : forall m n p, 1 < m -> 0 < n -> m * n <= p -> n < p.

Lemma lt_0_N_digits : forall n, 1 < n -> 0 < N_digits n.

Local Open Scope zarith_ext_scope.

We show that the restrictions are decidable.

Lemma Restrictions_dec : forall nn nk modu seed,
  {bbs_encode_decode.Implem.Restrictions nn nk modu seed} +
  {~ bbs_encode_decode.Implem.Restrictions nn nk modu seed}.

Section BBS.

Variables p q : Z.

Lemma gt_32_0 : (32 > 0)%nat.

Lemma tech1 : p * q < 2 ^^ (32 * (ceiling_div (S (Zabs_nat (N_digits (p * q)))) 32 gt_32_0)).

Hypothesis p_prime : prime p.

Hypothesis q_prime : prime q.

Lemma firstn_bbs : forall len1 len2 seed, (len1 <= len2)%nat ->
  firstn len1 (BBS.bbs p q p_prime q_prime len2 seed) = BBS.bbs p q p_prime q_prime len1 seed.

Implem.bbs_fun and BBS.bbs return equal results when the seed seed is restricted to the multiplicative group pf integers modulo p*q.

Lemma bbs_fun_bbs : forall len seed,
  bbs_fun len (proj1_sig seed) (p * q) = BBS.bbs p q p_prime q_prime len seed.

The semantics of bbs_asm:

Require Import Group.
Definition bbs_asm_sem (len : nat)
  (seed : Zstar.Zstar _ (Zstar.pq_gt_1 _ _ p_prime q_prime) ) : list bool :=
  let nn := ceiling_div len 32 gt_32_0 in
  let nk := ceiling_div (S (Zabs_nat (N_digits (p * q)))) 32 gt_32_0 in
  let modu := p * q in
  let seed' := proj1_sig seed in
  match Restrictions_dec nn nk modu seed' with
  | left H => firstn len
    (bbs_encode_decode.Implem.decode (proj1_sig (bbs_encode_decode.Implem.exec_bbs_asm nn nk modu seed' H)))
  | right _ => nil
  end.

Hypothesis p_odd : Zodd p.

Hypothesis q_odd : Zodd q.

The assembly code Implem.bbs_asm implements BBS.bbs. We need a technical lemma tech1.

Lemma bbs_semop : forall (len : nat) (seed : Zstar.Zstar (p * q) (Zstar.pq_gt_1 p q p_prime q_prime)) final_state,
  let nn := ceiling_div (S len) 32 gt_32_0 in
  let nk := ceiling_div (S (Zabs_nat (N_digits (p * q)))) 32 gt_32_0 in
  let modu := p * q in
  let seed' := proj1_sig seed in
  4 * (Z_of_nat (4 * nk + nn + 2)) < 2^^32 ->
  bbs_encode_decode.Implem.exec_sgoto bbs_encode_decode.Implem.bbs_asm
    (Some (O, bbs_encode_decode.Implem.encode nn nk seed' modu)) (Some (240%nat, final_state)) ->
  bbs_encode_decode.Implem.decode final_state =
  BBS.bbs _ _ p_prime q_prime (nn * 32) seed.

Lemma bbs_asm_sem_bbs : forall seed len,
  let nn := ceiling_div (S len) 32 gt_32_0 in
  let nk := ceiling_div (S (Zabs_nat (N_digits (p * q)))) 32 gt_32_0 in
  4 * Z_of_nat (4 * nk + nn + 2) < 2 ^^ 32 ->
  bbs_asm_sem (S len) seed = BBS.bbs p q p_prime q_prime (S len) seed.

Under the quadratic residuosity assumption qra, the assembly code Implem.bbs_asm is unpredictable.

Hypothesis distinct : p <> q.

Hypothesis p_blum : p mod 4 = 3 mod 4.

Hypothesis q_blum : q mod 4 = 3 mod 4.

Variable epsilon : R.

Hypothesis qra : HardProblem.QR _ _ p_prime q_prime epsilon.

Theorem unpredictable : forall len,
  let nn := ceiling_div (S len) 32 gt_32_0 in
  let nk := ceiling_div (S (Zabs_nat (N_digits (p * q)))) 32 gt_32_0 in
  4 * Z_of_nat (4 * nk + nn + 2) < 2 ^^ 32 ->
  Security.left_unpredictability _ (Zstar.Zstar_listNE _ (Zstar.pq_gt_1 _ _ p_prime q_prime)) bbs_asm_sem len epsilon.

End BBS.