Forward Secrecy Proof Script

.py

import random
field = 2**31 - 1
 
# Modular inverse via egcd
def mod_inv(a):
  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
 
assert ((2 * mod_inv(2)) % field) == 1
 
def rand():
  return random.randint(0, field - 1)
 
# Generators in the originally proposed F-S FCMP
G = rand() # Current G
T = rand() # New system-wide generator
U = rand()  # New system-wide generator
V = rand() # New system-wide generator
 
# Original key image generator
I = rand()
 
# Witness variables
x = rand() # Current private spend key
a = rand() # Key blinding factor
b = rand() # Key image generator blinding factor
c = rand() # Key image generator blinding factor blinding factor
r = rand() # BP+ blinding factor
xb = (x * b) % field
rac = (r + field + field - a - c) % field
 
# Re-randomized key
K_ = ((x * G) + (a * T)) % field
# Re-randomized key image generator
I_ = (I + (b * U)) % field
# Randomness commitment
B = ((b * V) + (c * T)) % field

"""
We want to calculate x * I, the key image. If we do x * I_, xI + xbU.
Accordingly, we need to prove x * I_ and remove xbU.
BP+ will gives P = xG bV xbU rT, calculating the xb term for us.
If we then subtract K' (xG + aT), we get bV xbU r-aT.
If we then subtract B' (bV + cT), we get xbU r-a-cT.
If the prover can open this over U/T, they removed the G/V terms (by using a consistent x/b, as expected).
That leaves us with a Pedersen commitment to xb.
"""

# BP+ output
def calc_P(this_x, this_b, this_r):
  this_xb = this_x * this_b
  return ((this_x * G) + (this_b * V) + (this_xb * U) + (this_r * T)) % field
P = calc_P(x, b, r)
# Key image
L = (x * I) % field
 
# Nonces
 
# The BP+ samples the following 4 nonces
bp_r = rand()
bp_s = rand()
bp_delta = rand()
bp_mu = rand()
 
# The GSP has a witness of [x, a, xb, rac], and selects a nonce for each
# It then publishes the multiexp of the row of nonces by each row in the matrix
# (the commitments)
# And a Schnorr signature for each member of the witness (r + chl x)
rx = rand()
ra = rand()
rxb = rand()
rrac = rand()
 
# Challenges
chl = rand()
bp_chl = rand()
 
# Solutions
def solution(nonce, witness):
  return (nonce + (chl * witness)) % field
 
def dlog(point, generator):
  return (point * mod_inv(generator)) % field
 
# Solutions
# GSP solutions
sx = solution(rx, x)
sa = solution(ra, a)
sxb = solution(rxb, xb)
srac = solution(rrac, rac)

# BP+ solutions
bp_rs = (bp_r + (x * bp_chl)) % field
bp_ss = (bp_s + (b * bp_chl)) % field
bp_sdelta = (bp_mu + (bp_delta * bp_chl) + (r * bp_chl * bp_chl)) % field
 
# We now select a J randomly, representing a distinct output's key image generator
# If there is a consistent solution for the above variables, one can not prove it wasn't J used
# If every output could be a potential output, one cannot determine the original output
J = rand()
 
# Extract the would-be x (x')
assert dlog(L, I) == x # Sanity check
x_ = dlog(L, J)
 
# Extract the would-be a (a')
def extract_a(this_x):
  # K = x G + a T
  x_term = (this_x * G) % field
  a_term = K_ + field - x_term
  return dlog(a_term, T)
assert a == extract_a(x) # Sanity check
a_= extract_a(x_)
 
# Extract the would-be b (b')
def extract_b(this_I):
  # I' = I + bU
  b_term = I_ + field - this_I
  return dlog(b_term, U)
assert b == extract_b(I) # Sanity check
b_ = extract_b(J)
 
# Extract the would-be c (c')
def extract_c(this_b):
  # B = bV + cT
  b_term = (this_b * V) % field
  return dlog(B + field - b_term, T)
assert c == extract_c(b) # Sanity check
c_ = extract_c(b_)
 
# Calculate the would-be xb (xb')
xb_ = x_ * b_
 
# We can now rebuild P and extract the (would-be) randomness used for it
def extract_r(this_x, this_b):
  return dlog(P + field - calc_P(this_x, this_b, 0), T)
assert r == extract_r(x, b) # Sanity check
r_ = extract_r(x_, b_)
assert P == calc_P(x_, b_, r_) # Sanity check
 
# With the would-be a, c, r, variables, we can calculate the would-be r-a-c
rac_ = (r_ + field + field - a_ - c_) % field
 
# We have now opened L (extracting x), K' (extracting a), I' (extracting b),
# B (extracting c), and P (extracting r)
# Since we know there's openings for those, check they're consistent
# We recover the nonces used from the solutions then check the nonces recovered
# align with the commitments
 
def extract_nonce(solution, witness):
  return (solution + field - ((chl * witness) % field)) % field
 
# Extract rx with x
assert rx == extract_nonce(sx, x)
rx_ = extract_nonce(sx, x_)
 
# Extract ra with a
assert ra == extract_nonce(sa, a)
ra_ = extract_nonce(sa, a_)
 
# Extract rxb with xb
assert rxb == extract_nonce(sxb, xb)
rxb_ = extract_nonce(sxb, xb_)
 
# Extract rrac with rac
assert rrac == extract_nonce(srac, rac)
rrac_ = extract_nonce(srac, rac_)
 
# Assert all the nonce commitments are consistent
# Nonces for opening the key
def nonce_commit_K(this_rx, this_ra):
  return ((this_rx * G) + (this_ra * T)) % field
assert nonce_commit_K(rx, ra) == nonce_commit_K(rx_, ra_)
 
# Nonces for opening the key image
def nonce_commit_L(this_rx, this_rxb):
  return ((this_rx * I_) + (this_rxb * (field - U))) % field
assert nonce_commit_L(rx, rxb) == nonce_commit_L(rx_, rxb_)
 
# Nonces for opening P'
def nonce_commit_P(this_rxb, this_rrac):
  return ((this_rxb * U) + (this_rrac * T)) % field
assert nonce_commit_P(rxb, rrac) == nonce_commit_P(rxb_, rrac_)
 
# Now extract/verify for the BP
def extract_bp_r(witness):
  return (bp_rs + field - ((witness * bp_chl) % field)) % field
assert bp_r == extract_bp_r(x)
bp_r_ = extract_bp_r(x_)
 
def extract_bp_s(witness):
  return (bp_ss + field - ((witness * bp_chl) % field)) % field
assert bp_s == extract_bp_s(b)
bp_s_ = extract_bp_s(b_)
 
# Since we have r_, s_, we can extract mu_ from the BP+ B
def commit_bp_B(this_r, this_s, this_mu):
  return ((this_r * this_s * U) + (this_mu * T)) % field
bp_B = commit_bp_B(bp_r, bp_s, bp_mu)
def extract_bp_mu(this_r, this_s):
  return dlog((bp_B + field - ((this_r * this_s * U) % field)) % field, T)
assert bp_mu == extract_bp_mu(bp_r, bp_s)
bp_mu_ = extract_bp_mu(bp_r_, bp_s_)
 
# Now we can extract delta_ from bp_sdelta
def extract_bp_delta(this_bp_mu, this_r):
  without_mu = bp_sdelta + field - this_bp_mu
  without_mu_r = without_mu + field - ((bp_chl * bp_chl * this_r) % field)
  return without_mu_r * mod_inv(bp_chl) % field
assert bp_delta == extract_bp_delta(bp_mu, r)
bp_delta_ = extract_bp_delta(bp_mu_, r_)
 
# Verify the A commitment lines up
def commit_bp_A(this_r, this_s, this_b, this_a, this_delta):
  return ((this_r * G) + (this_s * V) + (((this_r * this_b) + (this_s * this_a)) * U) + (this_delta * T)) % field
assert commit_bp_A(bp_r, bp_s, b, x, bp_delta) == commit_bp_A(bp_r_, bp_s_, b_, x_, bp_delta_)