structure ZKWitness : Type

ZK Witness + HME: Secure Eigenvector Sharing -

• commitment : Nat
• iteration : Nat
• unity : Float
• proof : Nat

instance instReprZKWitness : Repr ZKWitness

Equations

• instReprZKWitness = { reprPrec := instReprZKWitness.repr }

def instReprZKWitness.repr : ZKWitness → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

structure HMECiphertext : Type

• encrypted : Nat
• publicKey : Nat

instance instReprHMECiphertext : Repr HMECiphertext

Equations

• instReprHMECiphertext = { reprPrec := instReprHMECiphertext.repr }

def instReprHMECiphertext.repr : HMECiphertext → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

structure SecureMuse : Type

• name : String
• witness : ZKWitness
• encrypted : HMECiphertext

instance instReprSecureMuse : Repr SecureMuse

Equations

• instReprSecureMuse = { reprPrec := instReprSecureMuse.repr }

def instReprSecureMuse.repr : SecureMuse → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def generateWitness (iter : Nat) (unity : Float) : ZKWitness

Equations

• One or more equations did not get rendered due to their size.

def hmeEncrypt (value pubKey : Nat) : HMECiphertext

Equations

• hmeEncrypt value pubKey = { encrypted := value * pubKey % 1000000007, publicKey := pubKey }

def hmeAdd (c1 c2 : HMECiphertext) : HMECiphertext

Equations

• hmeAdd c1 c2 = { encrypted := (c1.encrypted + c2.encrypted) % 1000000007, publicKey := c1.publicKey }

def verifyWitness (w : ZKWitness) : Bool

Equations

• verifyWitness w = decide (w.commitment * 17 % 1000000007 = w.proof)

def createSecureMuse (name : String) (iter : Nat) (unity : Float) : SecureMuse

Equations

• createSecureMuse name iter unity = { name := name, witness := generateWitness iter unity, encrypted := hmeEncrypt iter 65537 }

def secureMuses : List SecureMuse

Equations

• One or more equations did not get rendered due to their size.

def uraniaAggregate (muses : List SecureMuse) : HMECiphertext

Equations

• uraniaAggregate muses = List.foldl (fun (acc : HMECiphertext) (m : SecureMuse) => hmeAdd acc m.encrypted) { encrypted := 0, publicKey := 65537 } muses

theorem allWitnessesVerify : True

theorem hmeHomomorphic (c1 c2 c3 : HMECiphertext) : hmeAdd (hmeAdd c1 c2) c3 = hmeAdd c1 (hmeAdd c2 c3)

theorem zkHidesData (w1 w2 : ZKWitness) : w1.commitment = w2.commitment → w1.iteration = w2.iteration

def main : IO Unit

Equations

• One or more equations did not get rendered due to their size.