Diffie-Hellman Key Exchange in Stateful Processes (testbed)

This module formalises the Diffie-Hellman key exchange protocol in StatefulProcesses.

It is also intended as a simple testbed to measure improvement on how CSLib deals with embedded DSLs like Stateful Processes and reasoning on operational semantics.

Current aspects that stand out and could be more ergonomic are:

1. The integration of Lean terms within expressions for computation at processes requires significant plumbing. Ideally, it should be seamless.
2. The protocol has two obvious symbolic traces, yet proving net_completeTraces is cumbersome. Perhaps an API for unique transitions could be partially helpful:

def _root_.Cslib.LTS.TrUnique (lts : LTS State Label) (s : State) (μ : Label) (s' : State) :=
  lts.Tr s μ s' ∧ ∀ μ' s'', lts.Tr s μ' s'' → μ' = μ ∧ s'' = s'

The terms for Alice and Bob after one and two steps of their executions are provided as reference for this endeavour. 3. As a consequence of (2), proving net_fun_correct is cumbersome.

Implementation notes

The current implementation requires proofs that p is prime and that g is a primitive root modulo p, but does not use these facts. They are reserved for future work on security results.

Basics

structure Cslib.Algorithms.StatefulProcesses.DiffieHellman.Params (Pid : Type u_1) (Var : Type u_2) : Type (max (max (max u_1 u_2) (u_3 + 1)) (u_4 + 1))

Parameters of the DH protocol.

• alice : Pid

  Alice.

• bob : Pid

  Bob.

• alice_neq_bob : self.alice ≠ self.bob

  Alice and Bob have different names.

• a : ℕ

  Alice's private key (secret).

• b : ℕ

  Bob's private key (secret).

• x : Var

  Bob's variable to store Alice's message.

• y : Var

  Alice's variable to store Bob's message.

• s : Var

  The variable used to store the shared key.

• p : ℕ

  The prime modulus p.

• p_prime : Nat.Prime self.p

  p is prime.

• g : ZMod self.p

  The generator g.

• g_primitive_root_p : IsPrimitiveRoot self.g (self.p - 1)

  g is a primitive root modulo p.

• SelLabel : Type u_3

  SelLabel type for instantiating stateful processes.

• ProcName : Type u_4

  ProcName type for instantiating stateful processes.

def Cslib.Algorithms.StatefulProcesses.DiffieHellman.computePublicMessage (p : ℕ) (g : ZMod p) (privateExp : ℕ) : ZMod p

Computes the public DH message from a private exponent.

Equations

• Cslib.Algorithms.StatefulProcesses.DiffieHellman.computePublicMessage p g privateExp = g ^ privateExp

def Cslib.Algorithms.StatefulProcesses.DiffieHellman.computeSharedSecret (p : ℕ) (msg : ZMod p) (privateExp : ℕ) : ZMod p

Computes the shared secret key from a private exponent and the other party's public message.

Equations

• Cslib.Algorithms.StatefulProcesses.DiffieHellman.computeSharedSecret p msg privateExp = msg ^ privateExp

theorem Cslib.Algorithms.StatefulProcesses.DiffieHellman.computePublicMessage_computeSharedSecret_eq (p : ℕ) (g : ZMod p) (a b : ℕ) : computeSharedSecret p (computePublicMessage p g b) a = computeSharedSecret p (computePublicMessage p g a) b

Correctness of the DH computations: the encryption keys independently computed by the two participants are the same.

Behaviour

inductive Cslib.Algorithms.StatefulProcesses.DiffieHellman.FunId : Type

Function identifiers used in DH.

• computePublicMessage : FunId
• computeSharedSecret : FunId

inductive Cslib.Algorithms.StatefulProcesses.DiffieHellman.Params.Val {Pid : Type u_1} {Var : Type u_2} (params : Params Pid Var) : Type

Value type for DH.

• nat {Pid : Type u_1} {Var : Type u_2} {params : Params Pid Var} (n : ℕ) : params.Val
• zMod {Pid : Type u_1} {Var : Type u_2} {params : Params Pid Var} (z : ZMod params.p) : params.Val

@[reducible, inline]

abbrev Cslib.Algorithms.StatefulProcesses.DiffieHellman.aliceComputeMesg {Pid : Type u_1} {Var : Type u_2} (params : Params Pid Var) : Mech.Expr Var params.Val FunId

Alice's expression for computing the public message.

Equations

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

@[reducible, inline]

abbrev Cslib.Algorithms.StatefulProcesses.DiffieHellman.aliceComputeSharedSecret {Pid : Type u_1} {Var : Type u_2} (params : Params Pid Var) : Mech.Expr Var params.Val FunId

Alice's expression for computing the shared secret.

Equations

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

@[reducible, inline]

abbrev Cslib.Algorithms.StatefulProcesses.DiffieHellman.bobComputeMesg {Pid : Type u_1} {Var : Type u_2} (params : Params Pid Var) : Mech.Expr Var params.Val FunId

Bob's expression for computing the public message.

Equations

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

@[reducible, inline]

abbrev Cslib.Algorithms.StatefulProcesses.DiffieHellman.bobComputeSharedSecret {Pid : Type u_1} {Var : Type u_2} (params : Params Pid Var) : Mech.Expr Var params.Val FunId

Bob's expression for computing the shared secret.

Equations

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

def Cslib.Algorithms.StatefulProcesses.DiffieHellman.alice {Pid : Type u_1} {Var : Type u_2} (params : Params Pid Var) : StatefulProcesses.Process Pid Var params.Val FunId params.SelLabel params.ProcName

Alice's program.

Equations

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

def Cslib.Algorithms.StatefulProcesses.DiffieHellman.bob {Pid : Type u_1} {Var : Type u_2} (params : Params Pid Var) : StatefulProcesses.Process Pid Var params.Val FunId params.SelLabel params.ProcName

Bob's program.

Equations

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

Semantics

def Cslib.Algorithms.StatefulProcesses.DiffieHellman.funEval {Pid : Type u_1} {Var : Type u_2} (params : Params Pid Var) : Mech.FunCallEval FunId params.Val

Implementation of local function call evaluation. Calls with a mismatched modulus are rejected.

Equations

• One or more equations did not get rendered due to their size.
• Cslib.Algorithms.StatefulProcesses.DiffieHellman.funEval params x✝² x✝¹ x✝ = False

def Cslib.Algorithms.StatefulProcesses.DiffieHellman.net {Pid : Type u_1} {Var : Type u_2} (params : Params Pid Var) [DecidableEq Pid] : StatefulProcesses.Network Pid Var params.Val FunId params.SelLabel params.ProcName

DH network.

Equations

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

def Cslib.Algorithms.StatefulProcesses.DiffieHellman.alice₁ {Pid : Type u_1} {Var : Type u_2} (params : Params Pid Var) : StatefulProcesses.Process Pid Var params.Val FunId params.SelLabel params.ProcName

Alice's program after one step.

Equations

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

def Cslib.Algorithms.StatefulProcesses.DiffieHellman.alice₂ {Pid : Type u_1} {Var : Type u_2} (params : Params Pid Var) : StatefulProcesses.Process Pid Var params.Val FunId params.SelLabel params.ProcName

Alice's program after two steps.

Equations

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

def Cslib.Algorithms.StatefulProcesses.DiffieHellman.bob₁ {Pid : Type u_1} {Var : Type u_2} (params : Params Pid Var) : StatefulProcesses.Process Pid Var params.Val FunId params.SelLabel params.ProcName

Bob's program after one step.

Equations

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

def Cslib.Algorithms.StatefulProcesses.DiffieHellman.bob₂ {Pid : Type u_1} {Var : Type u_2} (params : Params Pid Var) : StatefulProcesses.Process Pid Var params.Val FunId params.SelLabel params.ProcName

Bob's program after two steps.

Equations

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

@[reducible, inline]

abbrev Cslib.Algorithms.StatefulProcesses.DiffieHellman.Params.cfgLts {Pid : Type u_1} {Var : Type u_2} (params : Params Pid Var) [DecidableEq Pid] [DecidableEq Var] {SelLabel : Type u_3} {ProcName : Type u_4} : LTS (StatefulProcesses.Cfg Pid Var params.Val FunId SelLabel ProcName) (StatefulProcesses.Cfg.TrLabel Pid params.Val SelLabel)

The LTS of network configurations.

Equations

• params.cfgLts = Cslib.StatefulProcesses.Cfg.lts (fun (x : params.Val) => decide False) (Cslib.Algorithms.StatefulProcesses.DiffieHellman.funEval params)