From 3a7f90b124563f2af49c96b4846c2f8919561034 Mon Sep 17 00:00:00 2001 From: Christoph Fuerst Date: Wed, 5 Apr 2017 21:50:44 +0200 Subject: [PATCH] First revision of discrete-log, added Prime check --- discrete_log.txt | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 discrete_log.txt diff --git a/discrete_log.txt b/discrete_log.txt new file mode 100644 index 0000000..6c9a49e --- /dev/null +++ b/discrete_log.txt @@ -0,0 +1,21 @@ + +val M: ℕ; +val K: ℕ; + +type nat = ℕ[M]; +type prime = ℕ[K]; + +pred divides(m:prime,n:prime) ⇔ ∃p:prime. m⋅p = n; + +pred isPrime(m:prime) ⇔ ∀n:prime. divides(n,m) ⇒ (n ≤ 1 ∨ n = m); + +proc discrete_log(p:prime,g:nat,a:nat): nat + requires p>1 ∧ isPrime(p) ∧ // p is a prime greater than 1 + ∀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 = a; +{ + var loca:nat := a; + + return loca; +} -- 2.1.4