pred isPrime(m:prime) ⇔ ∀n:prime. divides(n,m) ⇒ (n ≤ 1 ∨ n = m);
-proc discrete_log(p:prime,g:nat,a:nat): nat
+proc InvModP(a:ℕ[K^2],p:prime): prime
+ requires p>1 ∧ isPrime(p) ∧
+ 0 < a ∧ a < p;
+ ensures (a*result) % p = 1;
+{
+ var ainv:prime := 0;
+ var i:ℕ[K^2];
+
+ if a = 1 then
+ {
+ ainv = 1;
+ }
+ else
+ {
+ for i=1;i<p;i=i+1 do
+ if a*i % p = 1 then
+ ainv = i;
+ }
+ return ainv;
+}
+
+proc discrete_log(p:prime,g:nat,a:nat,m: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
+ ∀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;
+ ensures (g^result)%p = a;
{
- var loca:nat := a;
+ var ret:Nat[K^2] := 0;
+ var A:Array[20,nat];
+ var b:Array[20,nat];
+ var gim:prime := g;
+
+ A = Array[20,nat](0);
+ b = Array[20,nat](0);
- return loca;
+ A[0] := 1;
+ b[0] := a;
+
+ var gi:prime = InvModP(g,p);
+
+ for var i:nat=1;i<m;i=i+1 do
+ {
+ A[i] = A[i-1]*g%p;
+ gim = gim*gi % p;
+ print A[i];
+ }
+ print gim;
+
+ for var i:nat=0;i<m;i=i+1 do
+ {
+ for var j:nat=0;j<m;j=j+1 do
+ {
+ if A[j] = b[i] then
+ {
+ ret = i*m + j;
+ }
+ }
+ b[i+1] = b[i]*gim % p;
+ }
+ print ret;
+ return ret;
+}
+
+proc main(): ()
+{
+ print discrete_log(11,2,10,10);
}