From b333fe3f394e6b98e0aa49cfc97cd3f2dee79d80 Mon Sep 17 00:00:00 2001 From: Christoph Fuerst Date: Sun, 7 May 2017 10:27:55 +0200 Subject: [PATCH] Assertion of result --- discrete_log.txt | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/discrete_log.txt b/discrete_log.txt index 32613be..b2e6535 100644 --- a/discrete_log.txt +++ b/discrete_log.txt @@ -53,6 +53,7 @@ proc IntegerRoot(a:nat): nat theorem InverseExists() ⇔ ∀a:nat. ∀p:prime. isPrime(p) ∧ 0 < a ∧ a < p ⇒ ∃r:nat. 0 < r ∧ r < p ∧ (a*r)%p = 1; + theorem DiscreteLogExists(p:prime, g:nat,a:nat) ⇔ (isPrime(p) ∧ 1 < g ∧ g < p ∧ ∀b:prime. (0 < b ∧ b < p-1) ⇒ (g^b % p ≠ 1) ∧ g^(p-1)%p = 1 ∧ // g has order p-1 0 < a ∧ a < p) ⇒ (∃k:res with 0 < k ∧ k ≤ (IntegerRoot(p-1)+1)^2. g^k%p = a); @@ -113,10 +114,12 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res b[i+1] = b[i]*gim % p; // Giant-Step } - assert(solFound = true ⇔ ∃r:nat with r < m. ∃s:nat with s < m. A[r] = b[s]); + assert(solFound = true ∧ ∃r:nat with r < m. ∃s:nat with s < m. A[r] = b[s]); +//// overflow in result... assert(∃r:nat with r < m. ∃s:nat with s < m. A[r] = b[s] ∧ (g^(s*m)%p * (g^r%p) = a)); // solFound = false should never be the case (see theorem DiscreteLogExists) - assert(solFound = false ⇔ ∀r:nat with r < m. ∀s:nat with s < m. A[r] ≠ b[s]); return ret; } + + -- 2.1.4