Spqr.lean🔗

Tier 2 · definitions used by the symbolic proof 13 headline theorems depend on it 154 of 261 lines trusted source ↗

Read the definitions shown. Only the declarations that the headline statements use are shown, with the namespace, section, open and variable commands needed to read them. The collapsed runs are theorems, which Lean checks, and definitions that no headline statement uses.

Declarations on this page (57)

SPQR V1 Post-Quantum Ratchet Equational Theory

DyLean term algebra, send/receive operations, and attacker deduction rules for the SPQR V1 ratchet. On fresh initial states (InitState), keys come from the epoch-0 chain (ChainKey) so honest first-message send and receive agree definitionally; subsequent transitions use opaque constructors (SendState, SendKey, SendMsg, RecvState, RecvKey).

namespace DY.Spqr

@[expose] public section Directions

inductive DirectionL29–32 ↗#

Session direction (A_2_B = 0 for initiator Alice, B_2_A = 1 for responder Bob).

inductive Direction where
  | a2b
  | b2a

def Direction.toByteL34–36 ↗#

def Direction.toByte: Direction → UInt8
  | .a2b => 0
  | .b2a => 1

def Direction.flipL38–40 ↗#

def Direction.flip: Direction → Direction
  | .a2b => .b2a
  | .b2a => .a2b

end Directions

@[expose] public section Literals

variable [BytesFunctor] [BytesFunctor.Has Literal.SubF]

open Literal

def encodeSpqrDirectionParamsL50–51 ↗#

Single-byte literal encoding the SPQR direction parameter.

def encodeSpqrDirectionParams (dir: Direction): Bytes := literalToBytes ⟨#[dir.toByte]⟩

def spqrParamsDir?L53–60 ↗#

Decodes a direction from an encodeSpqrDirectionParams literal, returning none otherwise.

def spqrParamsDir? (params: Bytes): Option Direction :=
  match bytesToLiteral params with
  | some b =>
    if b.data = #[0] then some .a2b
    else if b.data = #[1] then some .b2a
    else none
  | none => none

def encodeSpqrIndexTermL62–64 ↗#

4-byte little-endian literal encoding the u32 message index i.

def encodeSpqrIndexTerm (i: UInt32): Bytes :=
  literalToBytes ⟨#[i.toUInt8, (i >>> 8).toUInt8, (i >>> 16).toUInt8, (i >>> 24).toUInt8]⟩

def zeroKeyL66–67 ↗#

32-byte all-zero default HKDF salt returned at message index 0 on a fresh state.

def zeroKey: Bytes := literalToBytes ⟨Array.replicate 32 0⟩

def spqrEmptyMsgL69–73 ↗#

Whether msg is the empty literal (SPQR version 0, rejected by spqrRecv).

def spqrEmptyMsg (msg: Bytes): Bool :=
  match bytesToLiteral msg with
  | some b => b.size == 0
  | none => false

end Literals

namespace InitState

structure SubFL78–80 ↗#

public structure SubF (Bytes: Type) where
  authKey: Bytes
  params: Bytes

instanceL81 ↗#

public instance: ALaCarte.FunctorSizeOf SubF := .binary SubF.authKey SubF.params

instanceL82 ↗#

public instance: SubBytesFunctor SubF := .binary SubF.authKey SubF.params SubF.mk

def SubF.lengthL83 ↗#

public def SubF.length [BytesFunctor]: Bytes.PartialLength SubF := fun ⟨a, b⟩ rec => rec a + rec b

end InitState

namespace ChainKey

structure SubFL87–90 ↗#

public structure SubF (Bytes: Type) where
  authKey: Bytes
  params: Bytes
  idx: Bytes

instanceL91 ↗#

public instance: ALaCarte.FunctorSizeOf SubF := .ternary SubF.authKey SubF.params SubF.idx

instanceL92 ↗#

public instance: SubBytesFunctor SubF := .ternary SubF.authKey SubF.params SubF.idx SubF.mk

def SubF.lengthL93 ↗#

public def SubF.length [BytesFunctor]: Bytes.PartialLength SubF := fun _ _ => 32

end ChainKey

namespace SendState

structure SubFL97–99 ↗#

public structure SubF (Bytes: Type) where
  st: Bytes
  coins: Bytes

instanceL100 ↗#

public instance: ALaCarte.FunctorSizeOf SubF := .binary SubF.st SubF.coins

instanceL101 ↗#

public instance: SubBytesFunctor SubF := .binary SubF.st SubF.coins SubF.mk

def SubF.lengthL102 ↗#

public def SubF.length [BytesFunctor]: Bytes.PartialLength SubF := fun ⟨a, b⟩ rec => rec a + rec b

end SendState

namespace SendKey

structure SubFL106–108 ↗#

public structure SubF (Bytes: Type) where
  st: Bytes
  coins: Bytes

instanceL109 ↗#

public instance: ALaCarte.FunctorSizeOf SubF := .binary SubF.st SubF.coins

instanceL110 ↗#

public instance: SubBytesFunctor SubF := .binary SubF.st SubF.coins SubF.mk

def SubF.lengthL111 ↗#

public def SubF.length [BytesFunctor]: Bytes.PartialLength SubF := fun _ _ => 32

end SendKey

namespace SendMsg

structure SubFL115–117 ↗#

public structure SubF (Bytes: Type) where
  st: Bytes
  coins: Bytes

instanceL118 ↗#

public instance: ALaCarte.FunctorSizeOf SubF := .binary SubF.st SubF.coins

instanceL119 ↗#

public instance: SubBytesFunctor SubF := .binary SubF.st SubF.coins SubF.mk

def SubF.lengthL120 ↗#

public def SubF.length [BytesFunctor]: Bytes.PartialLength SubF := fun ⟨a, b⟩ rec => rec a + rec b

end SendMsg

namespace RecvState

structure SubFL124–126 ↗#

public structure SubF (Bytes: Type) where
  st: Bytes
  msg: Bytes

instanceL127 ↗#

public instance: ALaCarte.FunctorSizeOf SubF := .binary SubF.st SubF.msg

instanceL128 ↗#

public instance: SubBytesFunctor SubF := .binary SubF.st SubF.msg SubF.mk

def SubF.lengthL129 ↗#

public def SubF.length [BytesFunctor]: Bytes.PartialLength SubF := fun ⟨a, b⟩ rec => rec a + rec b

end RecvState

namespace RecvKey

structure SubFL133–135 ↗#

public structure SubF (Bytes: Type) where
  st: Bytes
  msg: Bytes

instanceL136 ↗#

public instance: ALaCarte.FunctorSizeOf SubF := .binary SubF.st SubF.msg

instanceL137 ↗#

public instance: SubBytesFunctor SubF := .binary SubF.st SubF.msg SubF.mk

def SubF.lengthL138 ↗#

public def SubF.length [BytesFunctor]: Bytes.PartialLength SubF := fun _ _ => 32

end RecvKey

#combineL141–148 ↗#

#combine into BytesFunctor, BytesLength from
  InitState,
  SendState,
  SendKey,
  SendMsg,
  RecvState,
  RecvKey,
  ChainKey,

@[expose] public section Constructors

variable [BytesFunctor] [BytesFunctor.Has SubF]

abbrev InitState.SubF.packL154 ↗#

abbrev InitState.SubF.pack (x: InitState.SubF Bytes) := BytesView.pack x

abbrev ChainKey.SubF.packL155 ↗#

abbrev ChainKey.SubF.pack (x: ChainKey.SubF Bytes) := BytesView.pack x

abbrev SendState.SubF.packL156 ↗#

abbrev SendState.SubF.pack (x: SendState.SubF Bytes) := BytesView.pack x

abbrev SendKey.SubF.packL157 ↗#

abbrev SendKey.SubF.pack (x: SendKey.SubF Bytes) := BytesView.pack x

abbrev SendMsg.SubF.packL158 ↗#

abbrev SendMsg.SubF.pack (x: SendMsg.SubF Bytes) := BytesView.pack x

abbrev RecvState.SubF.packL159 ↗#

abbrev RecvState.SubF.pack (x: RecvState.SubF Bytes) := BytesView.pack x

abbrev RecvKey.SubF.packL160 ↗#

abbrev RecvKey.SubF.pack (x: RecvKey.SubF Bytes) := BytesView.pack x

def spqrInitL162–164 ↗#

Initial SPQR state InitState{authKey, params}.

def spqrInit (authKey params: Bytes): Bytes :=
  ({authKey, params}: InitState.SubF Bytes).pack

def spqrChainKeyL166–168 ↗#

Epoch-0 chain key at idx under authKey and params.

def spqrChainKey (authKey params idx: Bytes): Bytes :=
  ({authKey, params, idx}: ChainKey.SubF Bytes).pack

end Constructors

@[expose] public section Functions

variable [BytesFunctor] [BytesFunctor.Has SubF] [BytesFunctor.Has Literal.SubF]

def spqrSendL176–182 ↗#

SPQR send step returning (state', key, msg). On InitState{authKey, params} the key is spqrChainKey authKey params (encodeSpqrIndexTerm 1); otherwise it is SendKey{st, coins}.

def spqrSend (st coins: Bytes): Bytes × Bytes × Bytes :=
  let key := match st.view? InitState.SubF with
    | some ⟨authKey, params⟩ => spqrChainKey authKey params (encodeSpqrIndexTerm 1)
    | none => ({st, coins}: SendKey.SubF Bytes).pack
  (({st, coins}: SendState.SubF Bytes).pack, key, ({st, coins}: SendMsg.SubF Bytes).pack)

def spqrRecvL184–197 ↗#

SPQR receive step at message index idx returning some (state', key), or none on an empty message or malformed InitState parameters.

def spqrRecv (st msg: Bytes) (idx: UInt32): Option (Bytes × Bytes) :=
  if spqrEmptyMsg msg then none
  else
    let st' := ({st, msg}: RecvState.SubF Bytes).pack
    match st.view? InitState.SubF with
    | some ⟨authKey, params⟩ =>
      match spqrParamsDir? params with
      | some dir =>
        some (st', if idx = 0 then zeroKey
          else spqrChainKey authKey (encodeSpqrDirectionParams dir.flip) (encodeSpqrIndexTerm idx))
      | none => none
    | none => some (st', ({st, msg}: RecvKey.SubF Bytes).pack)

end Functions

section AttackerKnowledgeBuild

variable [BytesFunctor] [BytesFunctor.Has SubF]

def spqrInit.attackerKnowledgeL205–207 ↗#

@[expose] public
def spqrInit.attackerKnowledge: SubAttackerKnowledge SubF where
  pred p out := ∃ authKey params, out = spqrInit authKey params ∧ p authKey ∧ p params

def spqrChainKey.attackerKnowledgeL209–212 ↗#

@[expose] public
def spqrChainKey.attackerKnowledge: SubAttackerKnowledge SubF where
  pred p out :=
    ∃ authKey params idx, out = spqrChainKey authKey params idx ∧ p authKey ∧ p params ∧ p idx

def spqrStateArg.attackerKnowledgeL214–221 ↗#

Projects arguments from a known SPQR state (InitState, SendState, or RecvState), modeling unencrypted pq_ratchet_state storage.

@[expose] public
def spqrStateArg.attackerKnowledge: SubAttackerKnowledge SubF where
  pred p out :=
    (∃ x: InitState.SubF Bytes, p x.pack ∧ (out = x.authKey ∨ out = x.params)) ∨
    (∃ x: SendState.SubF Bytes, p x.pack ∧ (out = x.st ∨ out = x.coins)) ∨
    (∃ x: RecvState.SubF Bytes, p x.pack ∧ (out = x.st ∨ out = x.msg))

end AttackerKnowledgeBuild

section AttackerKnowledgeRun

variable [BytesFunctor] [BytesFunctor.Has SubF] [BytesFunctor.Has Literal.SubF]

def spqrSendState.attackerKnowledgeL229–231 ↗#

@[expose] public
def spqrSendState.attackerKnowledge: SubAttackerKnowledge SubF where
  pred p out := ∃ st coins, out = (spqrSend st coins).1 ∧ p st ∧ p coins

def spqrSendKey.attackerKnowledgeL233–235 ↗#

@[expose] public
def spqrSendKey.attackerKnowledge: SubAttackerKnowledge SubF where
  pred p out := ∃ st coins, out = (spqrSend st coins).2.1 ∧ p st ∧ p coins

def spqrSendMsg.attackerKnowledgeL237–239 ↗#

@[expose] public
def spqrSendMsg.attackerKnowledge: SubAttackerKnowledge SubF where
  pred p out := ∃ st coins, out = (spqrSend st coins).2.2 ∧ p st ∧ p coins

def spqrRecvState.attackerKnowledgeL241–243 ↗#

@[expose] public
def spqrRecvState.attackerKnowledge: SubAttackerKnowledge SubF where
  pred p out := ∃ st msg idx r, spqrRecv st msg idx = some r ∧ out = r.1 ∧ p st ∧ p msg

def spqrRecvKey.attackerKnowledgeL245–247 ↗#

@[expose] public
def spqrRecvKey.attackerKnowledge: SubAttackerKnowledge SubF where
  pred p out := ∃ st msg idx r, spqrRecv st msg idx = some r ∧ out = r.2 ∧ p st ∧ p msg

end AttackerKnowledgeRun

#combineL251–262 ↗#

#combine [BytesFunctor.Has SubF] [BytesFunctor.Has Literal.SubF] into attackerKnowledge' from
  spqrInit,
  spqrChainKey,
  spqrSendState,
  spqrSendKey,
  spqrSendMsg,
  spqrRecvState,
  spqrRecvKey,
  spqrStateArg,

end DY.Spqr