Forward Secrecy Proof Script

.py

import random
# 2**31 - 1 is prime, making this a prime field
field = 2**31 - 1
 
# Modular inverse via egcd
def mod_inv(a):
  a = a % field
  t = 0
  new_t = 1
  r = field
  new_r = a % field
  while new_r != 0:
    q = r // new_r
    (t, new_t) = (new_t, (t - (q * new_t)) % field)
    (r, new_r) = (new_r, (r - (q * new_r)) % field)
  if r > 1:
    assert False
  if t < 0:
    t = t + n
  return t
 
# Random field element
def rand():
  return random.randint(0, field - 1)
 
for _ in range(10):
  a = rand()
  assert ((a * mod_inv(a)) % field) == 1
 
# Generators in the F-S FCMP++ system
G = rand()
T = rand()
U = rand()
V = rand()
 
# We now define an output as O, I
# We don't model C as its forward secrecy is trivial
x = rand()
y = rand()
O = ((x * G) + (y * T)) % field
 
# We use a random field element to model the hash-to-point
I = rand()
 
# Sent values
# Every time a new public value is created, we add it to this dict
# Every time we open a public value successfully, we remove it
# If the dict is empty at the end, we didn't forget to open any variables
sent = {}
 
# Form the linking tag L
L = (x * I) % field
sent["L"] = 1
 
# We re-randomize O and blind I
r_o = rand() # O re-randomization
r_i = rand() # I blind
r_j = rand() # Blind for the commitment to the I blind
 
O_tilde = (O + (r_o * T)) % field
sent["O_tilde"] = 1
I_tilde = (I + (r_i * U)) % field
sent["I_tilde"] = 1
R = ((r_i * V) + (r_j * T)) % field
sent["R"] = 1
 
# y_apo = y' = y + r_o
y_apo = y + r_o
 
# With the output tuple, re-randomizations/blinds, and input tuple, perform the SA+L proof
r_p = rand()
P = ((x * G) + (r_i * V) + (x * r_i * U) + (r_p * T)) % field
sent["P"] = 1
 
# Sanity check P
assert (P - O_tilde - R) % field == ((x * r_i * U) + (r_p - y_apo - r_j) * T) % field
 
# r_p_apo = r''p = r_p - y_apo - r_j
r_p_apo = r_p - y_apo - r_j
 
alpha = rand()
beta = rand()
delta = rand()
mu = rand()
r_y = rand()
r_z = rand()
r_r_p = rand()
 
A = (((alpha * G) + (beta * V)) + (((alpha * r_i) + (beta * x)) * U) + (delta * T)) % field
sent["A"] = 1
B = ((alpha * beta * U) + (mu * T)) % field
sent["B"] = 1
R_o = ((alpha * G) + (r_y * T)) % field
sent["R_o"] = 1
R_p = ((r_z * U) + (r_r_p * T)) % field
sent["R_p"] = 1
R_l = ((alpha * I_tilde) - (r_z * U)) % field
sent["R_l"] = 1
 
e = rand()
 
s_alpha = (alpha + (e * x)) % field
sent["s_alpha"] = 1
s_beta = (beta + (e * r_i)) % field
sent["s_beta"] = 1
s_delta = (mu + (e * delta) + (e * e * r_p)) % field
sent["s_delta"] = 1
s_y = (r_y + (e * y_apo)) % field
sent["s_y"] = 1
s_z = (r_z + (e * (x * r_i))) % field
sent["s_z"] = 1
s_r_p = (r_r_p + (e * r_p_apo)) % field
sent["s_r_p"] = 1
 
# Verify the proof
assert ((e * e * P) + (e * A) + B) % field == ((s_alpha * e * G) + (s_beta * e * V) + (s_alpha * s_beta * U) + (s_delta * T)) % field
assert (R_o + (e * O_tilde)) % field == ((s_alpha * G) + (s_y * T)) % field
assert (R_p + (e * (P - O_tilde - R))) % field == ((s_z * U) + (s_r_p * T)) % field
assert (R_l + (e * L)) % field == ((s_alpha * I_tilde) - (s_z * U)) % field
 
# Now, run an extractor from a random output/key image generator and verify we can't find an inconsistency
# Since we demonstrate how anyone with a discrete log oracle can find an opening for any output, no output can be found definitively
O_candidate = rand()
I_candidate = rand()
 
# The discrete log oracle
def dlog(point, generator):
  dlog = (point * mod_inv(generator)) % field
  assert (dlog * generator) % field == point % field
  return dlog
 
# Solve for x as the discrete logarithm of L over I_candidate
x_candidate = dlog(L, I_candidate)
# Solve for y
y_candidate = dlog(O_candidate - (x_candidate * G), T)
assert ((x_candidate * G) + (y_candidate * T)) % field == O_candidate
assert (x_candidate * I_candidate) % field == L
del sent["L"]
 
# Calculate r_o, r_i, r_j in that order
r_o_candidate = dlog(O_tilde - O_candidate, T)
r_i_candidate = dlog(I_tilde - I_candidate, U)
r_j_candidate = dlog(R - (r_i_candidate * V), T)
 
assert ((x_candidate * G) + ((y_candidate + r_o_candidate) * T)) % field == O_tilde
del sent["O_tilde"]
assert (I_candidate + (r_i_candidate * U)) % field == I_tilde
del sent["I_tilde"]
assert ((r_i_candidate * V) + (r_j_candidate * T)) % field == R
del sent["R"]
 
y_apo_candidate = y_candidate + r_o_candidate
 
r_p_candidate = dlog(P - ((x_candidate * G) + (r_i_candidate * V) + (x_candidate * r_i_candidate * U)), T)
assert P == ((x_candidate * G) + (r_i_candidate * V) + (x_candidate * r_i_candidate * U) + (r_p_candidate * T)) % field
del sent["P"]
 
r_p_apo_candidate = (r_p_candidate - y_apo_candidate - r_j_candidate) % field
 
# Recover alpha, beta, r_y, r_z, r_r_p
alpha_candidate = (s_alpha - (e * x_candidate)) % field
beta_candidate = (s_beta - (e * r_i_candidate)) % field
r_y_candidate = (s_y - (e * y_apo_candidate)) % field
r_z_candidate = (s_z - (e * (x_candidate * r_i_candidate))) % field
r_r_p_candidate = (s_r_p - (e * r_p_apo_candidate)) % field
 
# Recover delta and mu
delta_candidate = dlog(A - ((alpha_candidate * G) + (beta_candidate * V) + (((alpha_candidate * r_i_candidate) + (beta_candidate * x_candidate)) * U)), T)
mu_candidate = dlog(B - (alpha_candidate * beta_candidate * U), T)
 
# Verify A, B, R_o, R_p, R_l, s_alpha, s_beta, s_delta, s_y, s_z, s_r_p
assert A == (((alpha_candidate * G) + (beta_candidate * V)) + (((alpha_candidate * r_i_candidate) + (beta_candidate * x_candidate)) * U) + (delta_candidate * T)) % field
del sent["A"]
assert B == ((alpha_candidate * beta_candidate * U) + (mu_candidate * T)) % field
del sent["B"]
assert R_o == ((alpha_candidate * G) + (r_y_candidate * T)) % field
del sent["R_o"]
assert R_p == ((r_z_candidate * U) + (r_r_p_candidate * T)) % field
del sent["R_p"]
assert R_l == ((alpha_candidate * I_tilde) - (r_z_candidate * U)) % field
del sent["R_l"]
 
assert s_alpha == (alpha_candidate + (e * x_candidate)) % field
del sent["s_alpha"]
assert s_beta == (beta_candidate + (e * r_i_candidate)) % field
del sent["s_beta"]
assert s_delta == (mu_candidate + (e * delta_candidate) + (e * e * r_p_candidate)) % field
del sent["s_delta"]
assert s_y == (r_y_candidate + (e * y_apo_candidate)) % field
del sent["s_y"]
assert s_z == (r_z_candidate + (e * (x_candidate * r_i_candidate))) % field
del sent["s_z"]
assert s_r_p == (r_r_p_candidate + (e * r_p_apo_candidate)) % field
del sent["s_r_p"]
 
assert len(sent) == 0
 
print("Done")