From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Thu, 6 Apr 2017 19:32:04 +0000 (+0200)
Subject: Further Pre-Conditions for Discrete Logarithm
X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=d6d0d3c3817b0109d4cccf64f21404946d8b68c9;p=cfuerst%2Fformal-numbers.git

Further Pre-Conditions for Discrete Logarithm
---

diff --git a/discrete_log.txt b/discrete_log.txt
index 047ffb9..c64a129 100644
--- a/discrete_log.txt
+++ b/discrete_log.txt
@@ -33,7 +33,10 @@ proc InvModP(a:ℕ[K^2],p:prime): prime
 }
 
 proc discrete_log(p:prime,g:nat,a:nat,m:nat): res
-   requires p>1 ∧ isPrime(p) ∧ // p is a prime greater than 1
+   requires 1 < p ∧ isPrime(p) ∧ // p is a prime greater than 1
+            1 < g ∧ g < p ∧ 
+            1 < a ∧ ¬divides(p,a) ∧
+            8 < m ∧ 
             ∀b:nat. (0 < b ∧ b < p-1) ⇒ (g^b % p ≠ 1) ∧  g^(p-1)%p = 1 ∧ // g has order p-1
             0 ≤ a ∧ a < p; // a is in ℤ/pℤ
    ensures (g^result)%p = a;