9.3. SPQR🔗

Definition9.3.1

groupuses 1

Used by 2

Reverse dependency previews

Preview

Definition 9.3.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

\todo

send authenticated encapsulation-key header

/-- Generate a KEM key pair and return the successor state, header, and tag. -/
def sendHeader (inc : kem.IncrementalStructure)
    (auth : RatchetedAuthenticator InitKey EpochKey AuthState inc.PKheader (inc.C₁ × inc.C₂) Mac)
    (st : KeysUnsampled AuthState) : m (HeaderSent inc AuthState × inc.PKheader × Mac) := do
  let (pk, sk) ← kem.keygen
  let hdr := inc.toHeader pk
  pure (⟨st.ep, st.authSt, pk, sk⟩, hdr, auth.macHeader st.authSt st.ep hdr)

send encapsulation-key vector

/-- Return the successor state and the vector component of the stored encapsulation key. -/
def sendVector (inc : kem.IncrementalStructure) (st : HeaderSent inc AuthState) :
    EkSent inc AuthState × inc.PKvector :=
  (⟨st.ep, st.authSt, st.sk⟩, inc.toVector st.pk)

receive first ciphertext component

/-- Store the first ciphertext component. -/
def recvCt1 (inc : kem.IncrementalStructure) (st : EkSent inc AuthState)
    (c1 : inc.C₁) : EkSentCt1Received inc AuthState :=
  ⟨st.ep, st.authSt, st.sk, c1⟩

receive second ciphertext component and tag

/-- Decapsulate and authenticate the ciphertext, returning the next role state and epoch key. -/
def recvCt2 (inc : kem.IncrementalStructure)
    (auth : RatchetedAuthenticator InitKey EpochKey AuthState inc.PKheader (inc.C₁ × inc.C₂) Mac)
    (deriveEpochKey : EpochKeyDerivation K EpochKey) (hDet : DeterministicDecaps kem)
    (st : EkSentCt1Received inc AuthState) (c2 : inc.C₂) (tag : Mac) :
    Option (CtSender.NoHeaderReceived AuthState × (ℕ × EpochKey)) :=
  match hDet.decapsDet st.sk (inc.splitC.symm (st.c1, c2)) with
  | none => none
  | some k =>
    let ik := deriveEpochKey k st.ep
    let authSt' := auth.update st.authSt st.ep ik
    if auth.verifyCiphertext authSt' st.ep (st.c1, c2) tag then
      some (⟨st.ep + 1, authSt'⟩, (st.ep, ik))
    else none

uses Definition 6.4.1 · github #252

Lean code for Definition9.3.1●8 definitions

structure(2 fields)defined in SecureMessaging/SCKA/SPQR/Unchunked.lean

complete

structure SPQR.EkSender.KeysUnsampled (AuthState : Type) : Type

structure SPQR.EkSender.KeysUnsampled
  (AuthState : Type) : Type

State before sampling an encapsulation key.

Fields

ep : ℕ

The epoch in progress.

authSt : AuthState

Authenticator state entering the epoch.

structure(4 fields)defined in SecureMessaging/SCKA/SPQR/Unchunked.lean

complete

structure SPQR.EkSender.HeaderSent.{u} {m : Type → Type u} [Monad m]
  {K PK SK C : Type} {kem : KEMScheme m K PK SK C}
  (inc : kem.IncrementalStructure) (AuthState : Type) : Type

structure SPQR.EkSender.HeaderSent.{u}
  {m : Type → Type u} [Monad m]
  {K PK SK C : Type}
  {kem : KEMScheme m K PK SK C}
  (inc : kem.IncrementalStructure)
  (AuthState : Type) : Type

State after sending the authenticated encapsulation-key header.

Fields

ep : ℕ

The epoch in progress.

authSt : AuthState

Authenticator state entering the epoch.

pk : PK

The sampled encapsulation key.

sk : SK

The decapsulation key held for this epoch.

structure(3 fields)defined in SecureMessaging/SCKA/SPQR/Unchunked.lean

complete

structure SPQR.EkSender.EkSent.{u} {m : Type → Type u} [Monad m]
  {K PK SK C : Type} {kem : KEMScheme m K PK SK C}
  (inc : kem.IncrementalStructure) (AuthState : Type) : Type

structure SPQR.EkSender.EkSent.{u}
  {m : Type → Type u} [Monad m]
  {K PK SK C : Type}
  {kem : KEMScheme m K PK SK C}
  (inc : kem.IncrementalStructure)
  (AuthState : Type) : Type

State after sending the encapsulation-key vector.

Fields

ep : ℕ

The epoch in progress.

authSt : AuthState

Authenticator state entering the epoch.

sk : SK

The decapsulation key held for this epoch.

structure(4 fields)defined in SecureMessaging/SCKA/SPQR/Unchunked.lean

complete

structure SPQR.EkSender.EkSentCt1Received.{u} {m : Type → Type u} [Monad m]
  {K PK SK C : Type} {kem : KEMScheme m K PK SK C}
  (inc : kem.IncrementalStructure) (AuthState : Type) : Type

structure SPQR.EkSender.EkSentCt1Received.{u}
  {m : Type → Type u} [Monad m]
  {K PK SK C : Type}
  {kem : KEMScheme m K PK SK C}
  (inc : kem.IncrementalStructure)
  (AuthState : Type) : Type

State after sending the encapsulation key and receiving the first ciphertext component.

Fields

ep : ℕ

The epoch in progress.

authSt : AuthState

Authenticator state entering the epoch.

sk : SK

The decapsulation key held for this epoch.

c1 : inc.C₁

The received first ciphertext component.

defdefined in SecureMessaging/SCKA/SPQR/Unchunked.lean

complete

def SPQR.EkSender.sendHeader.{u} {m : Type → Type u} [Monad m]
  {K PK SK C : Type} {kem : KEMScheme m K PK SK C}
  {InitKey EpochKey AuthState Mac : Type}
  (inc : kem.IncrementalStructure)
  (auth :
    RatchetedAuthenticator InitKey EpochKey AuthState inc.PKheader
      (inc.C₁ × inc.C₂) Mac)
  (st : SPQR.EkSender.KeysUnsampled AuthState) :
  m (SPQR.EkSender.HeaderSent inc AuthState × inc.PKheader × Mac)

def SPQR.EkSender.sendHeader.{u}
  {m : Type → Type u} [Monad m]
  {K PK SK C : Type}
  {kem : KEMScheme m K PK SK C}
  {InitKey EpochKey AuthState Mac : Type}
  (inc : kem.IncrementalStructure)
  (auth :
    RatchetedAuthenticator InitKey
      EpochKey AuthState inc.PKheader
      (inc.C₁ × inc.C₂) Mac)
  (st :
    SPQR.EkSender.KeysUnsampled
      AuthState) :
  m
    (SPQR.EkSender.HeaderSent inc
        AuthState ×
      inc.PKheader × Mac)

Generate a KEM key pair and return the successor state, header, and tag.

defdefined in SecureMessaging/SCKA/SPQR/Unchunked.lean

complete

def SPQR.EkSender.sendVector.{u} {m : Type → Type u} [Monad m]
  {K PK SK C : Type} {kem : KEMScheme m K PK SK C} {AuthState : Type}
  (inc : kem.IncrementalStructure)
  (st : SPQR.EkSender.HeaderSent inc AuthState) :
  SPQR.EkSender.EkSent inc AuthState × inc.PKvector

def SPQR.EkSender.sendVector.{u}
  {m : Type → Type u} [Monad m]
  {K PK SK C : Type}
  {kem : KEMScheme m K PK SK C}
  {AuthState : Type}
  (inc : kem.IncrementalStructure)
  (st :
    SPQR.EkSender.HeaderSent inc
      AuthState) :
  SPQR.EkSender.EkSent inc AuthState ×
    inc.PKvector

Return the successor state and the vector component of the stored encapsulation key.

defdefined in SecureMessaging/SCKA/SPQR/Unchunked.lean

complete

def SPQR.EkSender.recvCt1.{u} {m : Type → Type u} [Monad m]
  {K PK SK C : Type} {kem : KEMScheme m K PK SK C} {AuthState : Type}
  (inc : kem.IncrementalStructure)
  (st : SPQR.EkSender.EkSent inc AuthState) (c1 : inc.C₁) :
  SPQR.EkSender.EkSentCt1Received inc AuthState

def SPQR.EkSender.recvCt1.{u}
  {m : Type → Type u} [Monad m]
  {K PK SK C : Type}
  {kem : KEMScheme m K PK SK C}
  {AuthState : Type}
  (inc : kem.IncrementalStructure)
  (st :
    SPQR.EkSender.EkSent inc AuthState)
  (c1 : inc.C₁) :
  SPQR.EkSender.EkSentCt1Received inc
    AuthState

Store the first ciphertext component.

defdefined in SecureMessaging/SCKA/SPQR/Unchunked.lean

complete

def SPQR.EkSender.recvCt2.{u} {m : Type → Type u} [Monad m]
  {K PK SK C : Type} {kem : KEMScheme m K PK SK C}
  {InitKey EpochKey AuthState Mac : Type}
  (inc : kem.IncrementalStructure)
  (auth :
    RatchetedAuthenticator InitKey EpochKey AuthState inc.PKheader
      (inc.C₁ × inc.C₂) Mac)
  (deriveEpochKey : SPQR.EpochKeyDerivation K EpochKey)
  (hDet : kem.DeterministicDecaps)
  (st : SPQR.EkSender.EkSentCt1Received inc AuthState) (c2 : inc.C₂)
  (tag : Mac) :
  Option (SPQR.CtSender.NoHeaderReceived AuthState × ℕ × EpochKey)

def SPQR.EkSender.recvCt2.{u}
  {m : Type → Type u} [Monad m]
  {K PK SK C : Type}
  {kem : KEMScheme m K PK SK C}
  {InitKey EpochKey AuthState Mac : Type}
  (inc : kem.IncrementalStructure)
  (auth :
    RatchetedAuthenticator InitKey
      EpochKey AuthState inc.PKheader
      (inc.C₁ × inc.C₂) Mac)
  (deriveEpochKey :
    SPQR.EpochKeyDerivation K EpochKey)
  (hDet : kem.DeterministicDecaps)
  (st :
    SPQR.EkSender.EkSentCt1Received inc
      AuthState)
  (c2 : inc.C₂) (tag : Mac) :
  Option
    (SPQR.CtSender.NoHeaderReceived
        AuthState ×
      ℕ × EpochKey)

Decapsulate and authenticate the ciphertext, returning the next role state and epoch key.

Definition9.3.2

groupuses 1

Used by 2

Reverse dependency previews

Preview

Definition 9.3.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

\todo

receive authenticated encapsulation-key header

/-- Verify the header tag and return the successor state on success. -/
def recvHeader (inc : kem.IncrementalStructure)
    (auth : RatchetedAuthenticator InitKey EpochKey AuthState inc.PKheader (inc.C₁ × inc.C₂) Mac)
    (st : NoHeaderReceived AuthState) (hdr : inc.PKheader) (tag : Mac) :
    Option (HeaderReceived inc AuthState) :=
  if auth.verifyHeader st.authSt st.ep hdr tag then some ⟨st.ep, st.authSt, hdr⟩ else none

send first ciphertext component

/-- Run encapsulation stage one and return the successor state, ciphertext, and epoch key. -/
def sendCt1 (inc : kem.IncrementalStructure)
    (auth : RatchetedAuthenticator InitKey EpochKey AuthState inc.PKheader (inc.C₁ × inc.C₂) Mac)
    (deriveEpochKey : EpochKeyDerivation K EpochKey) (st : HeaderReceived inc AuthState) :
    m (Ct1Sent inc AuthState × inc.C₁ × (ℕ × EpochKey)) := do
  let (encapsSt, c1, k) ← inc.encaps1 st.hdr
  let ik := deriveEpochKey k st.ep
  pure (⟨st.ep, auth.update st.authSt st.ep ik, st.hdr, encapsSt, c1⟩, c1, (st.ep, ik))

receive encapsulation-key vector

/-- Validate the encapsulation-key vector and return the successor state on success. -/
def recvVector (inc : kem.IncrementalStructure) (st : Ct1Sent inc AuthState)
    (vec : inc.PKvector) : Option (Ct1SentEkReceived inc AuthState) :=
  if inc.validPK st.hdr vec then
    some ⟨st.ep, st.authSt, st.hdr, st.encapsSt, st.c1, vec⟩
  else none

send second ciphertext component and tag

/-- Run encapsulation stage two and return the successor state, ciphertext, and tag. -/
def sendCt2 (inc : kem.IncrementalStructure)
    (auth : RatchetedAuthenticator InitKey EpochKey AuthState inc.PKheader (inc.C₁ × inc.C₂) Mac)
    (st : Ct1SentEkReceived inc AuthState) : m (Ct2Sent AuthState × inc.C₂ × Mac) := do
  let c2 ← inc.encaps2 st.encapsSt st.hdr st.vec
  pure (⟨st.ep, st.authSt⟩, c2, auth.macCiphertext st.authSt st.ep (st.c1, c2))

advance to the next epoch

/-- Return the encapsulation-key-sender state exactly when `t` is the successor epoch. -/
def recvNextEpoch (st : Ct2Sent AuthState) (t : ℕ) : Option (EkSender.KeysUnsampled AuthState) :=
  if t = st.ep + 1 then some ⟨st.ep + 1, st.authSt⟩ else none

uses Definition 6.4.1 · github #252

Lean code for Definition9.3.2●10 definitions

structure(2 fields)defined in SecureMessaging/SCKA/SPQR/Unchunked.lean

complete

structure SPQR.CtSender.NoHeaderReceived (AuthState : Type) : Type

structure SPQR.CtSender.NoHeaderReceived
  (AuthState : Type) : Type

State before receiving an encapsulation-key header.

Fields

ep : ℕ

The epoch in progress.

authSt : AuthState

Authenticator state entering the epoch.

structure(3 fields)defined in SecureMessaging/SCKA/SPQR/Unchunked.lean

complete

structure SPQR.CtSender.HeaderReceived.{u} {m : Type → Type u} [Monad m]
  {K PK SK C : Type} {kem : KEMScheme m K PK SK C}
  (inc : kem.IncrementalStructure) (AuthState : Type) : Type

structure SPQR.CtSender.HeaderReceived.{u}
  {m : Type → Type u} [Monad m]
  {K PK SK C : Type}
  {kem : KEMScheme m K PK SK C}
  (inc : kem.IncrementalStructure)
  (AuthState : Type) : Type

State after receiving an authenticated encapsulation-key header.

Fields

ep : ℕ

The epoch in progress.

authSt : AuthState

Authenticator state entering the epoch.

hdr : inc.PKheader

Stored encapsulation-key header.

structure(5 fields)defined in SecureMessaging/SCKA/SPQR/Unchunked.lean

complete

structure SPQR.CtSender.Ct1Sent.{u} {m : Type → Type u} [Monad m]
  {K PK SK C : Type} {kem : KEMScheme m K PK SK C}
  (inc : kem.IncrementalStructure) (AuthState : Type) : Type

structure SPQR.CtSender.Ct1Sent.{u}
  {m : Type → Type u} [Monad m]
  {K PK SK C : Type}
  {kem : KEMScheme m K PK SK C}
  (inc : kem.IncrementalStructure)
  (AuthState : Type) : Type

State after deriving the epoch key and sending the first ciphertext component.

Fields

ep : ℕ

The epoch in progress.

authSt : AuthState

Authenticator state after the update with this epoch's key.

hdr : inc.PKheader

Stored encapsulation-key header.

encapsSt : inc.St

The encapsulation state carried from the first stage to the second.

c1 : inc.C₁

The first ciphertext component, kept for the ciphertext tag.

structure(6 fields)defined in SecureMessaging/SCKA/SPQR/Unchunked.lean

complete

structure SPQR.CtSender.Ct1SentEkReceived.{u} {m : Type → Type u} [Monad m]
  {K PK SK C : Type} {kem : KEMScheme m K PK SK C}
  (inc : kem.IncrementalStructure) (AuthState : Type) : Type

structure SPQR.CtSender.Ct1SentEkReceived.{u}
  {m : Type → Type u} [Monad m]
  {K PK SK C : Type}
  {kem : KEMScheme m K PK SK C}
  (inc : kem.IncrementalStructure)
  (AuthState : Type) : Type

State after sending the first ciphertext component and validating the encapsulation key.

Fields

ep : ℕ

The epoch in progress.

authSt : AuthState

Authenticator state after the update with this epoch's key.

hdr : inc.PKheader

Stored encapsulation-key header.

encapsSt : inc.St

The encapsulation state carried from the first stage to the second.

c1 : inc.C₁

The first ciphertext component, kept for the ciphertext tag.

vec : inc.PKvector

Stored encapsulation-key vector.

structure(2 fields)defined in SecureMessaging/SCKA/SPQR/Unchunked.lean

complete

structure SPQR.CtSender.Ct2Sent (AuthState : Type) : Type

structure SPQR.CtSender.Ct2Sent (AuthState : Type) :
  Type

State after sending the second ciphertext component and its tag.

Fields

ep : ℕ

The epoch in progress.

authSt : AuthState

Authenticator state after the update with this epoch's key.

defdefined in SecureMessaging/SCKA/SPQR/Unchunked.lean

complete

def SPQR.CtSender.recvHeader.{u} {m : Type → Type u} [Monad m]
  {K PK SK C : Type} {kem : KEMScheme m K PK SK C}
  {InitKey EpochKey AuthState Mac : Type}
  (inc : kem.IncrementalStructure)
  (auth :
    RatchetedAuthenticator InitKey EpochKey AuthState inc.PKheader
      (inc.C₁ × inc.C₂) Mac)
  (st : SPQR.CtSender.NoHeaderReceived AuthState) (hdr : inc.PKheader)
  (tag : Mac) : Option (SPQR.CtSender.HeaderReceived inc AuthState)

def SPQR.CtSender.recvHeader.{u}
  {m : Type → Type u} [Monad m]
  {K PK SK C : Type}
  {kem : KEMScheme m K PK SK C}
  {InitKey EpochKey AuthState Mac : Type}
  (inc : kem.IncrementalStructure)
  (auth :
    RatchetedAuthenticator InitKey
      EpochKey AuthState inc.PKheader
      (inc.C₁ × inc.C₂) Mac)
  (st :
    SPQR.CtSender.NoHeaderReceived
      AuthState)
  (hdr : inc.PKheader) (tag : Mac) :
  Option
    (SPQR.CtSender.HeaderReceived inc
      AuthState)

Verify the header tag and return the successor state on success.

defdefined in SecureMessaging/SCKA/SPQR/Unchunked.lean

complete

def SPQR.CtSender.sendCt1.{u} {m : Type → Type u} [Monad m]
  {K PK SK C : Type} {kem : KEMScheme m K PK SK C}
  {InitKey EpochKey AuthState Mac : Type}
  (inc : kem.IncrementalStructure)
  (auth :
    RatchetedAuthenticator InitKey EpochKey AuthState inc.PKheader
      (inc.C₁ × inc.C₂) Mac)
  (deriveEpochKey : SPQR.EpochKeyDerivation K EpochKey)
  (st : SPQR.CtSender.HeaderReceived inc AuthState) :
  m (SPQR.CtSender.Ct1Sent inc AuthState × inc.C₁ × ℕ × EpochKey)

def SPQR.CtSender.sendCt1.{u}
  {m : Type → Type u} [Monad m]
  {K PK SK C : Type}
  {kem : KEMScheme m K PK SK C}
  {InitKey EpochKey AuthState Mac : Type}
  (inc : kem.IncrementalStructure)
  (auth :
    RatchetedAuthenticator InitKey
      EpochKey AuthState inc.PKheader
      (inc.C₁ × inc.C₂) Mac)
  (deriveEpochKey :
    SPQR.EpochKeyDerivation K EpochKey)
  (st :
    SPQR.CtSender.HeaderReceived inc
      AuthState) :
  m
    (SPQR.CtSender.Ct1Sent inc AuthState ×
      inc.C₁ × ℕ × EpochKey)

Run encapsulation stage one and return the successor state, ciphertext, and epoch key.

defdefined in SecureMessaging/SCKA/SPQR/Unchunked.lean

complete

def SPQR.CtSender.recvVector.{u} {m : Type → Type u} [Monad m]
  {K PK SK C : Type} {kem : KEMScheme m K PK SK C} {AuthState : Type}
  (inc : kem.IncrementalStructure)
  (st : SPQR.CtSender.Ct1Sent inc AuthState) (vec : inc.PKvector) :
  Option (SPQR.CtSender.Ct1SentEkReceived inc AuthState)

def SPQR.CtSender.recvVector.{u}
  {m : Type → Type u} [Monad m]
  {K PK SK C : Type}
  {kem : KEMScheme m K PK SK C}
  {AuthState : Type}
  (inc : kem.IncrementalStructure)
  (st :
    SPQR.CtSender.Ct1Sent inc AuthState)
  (vec : inc.PKvector) :
  Option
    (SPQR.CtSender.Ct1SentEkReceived inc
      AuthState)

Validate the encapsulation-key vector and return the successor state on success.

defdefined in SecureMessaging/SCKA/SPQR/Unchunked.lean

complete

def SPQR.CtSender.sendCt2.{u} {m : Type → Type u} [Monad m]
  {K PK SK C : Type} {kem : KEMScheme m K PK SK C}
  {InitKey EpochKey AuthState Mac : Type}
  (inc : kem.IncrementalStructure)
  (auth :
    RatchetedAuthenticator InitKey EpochKey AuthState inc.PKheader
      (inc.C₁ × inc.C₂) Mac)
  (st : SPQR.CtSender.Ct1SentEkReceived inc AuthState) :
  m (SPQR.CtSender.Ct2Sent AuthState × inc.C₂ × Mac)

def SPQR.CtSender.sendCt2.{u}
  {m : Type → Type u} [Monad m]
  {K PK SK C : Type}
  {kem : KEMScheme m K PK SK C}
  {InitKey EpochKey AuthState Mac : Type}
  (inc : kem.IncrementalStructure)
  (auth :
    RatchetedAuthenticator InitKey
      EpochKey AuthState inc.PKheader
      (inc.C₁ × inc.C₂) Mac)
  (st :
    SPQR.CtSender.Ct1SentEkReceived inc
      AuthState) :
  m
    (SPQR.CtSender.Ct2Sent AuthState ×
      inc.C₂ × Mac)

Run encapsulation stage two and return the successor state, ciphertext, and tag.

defdefined in SecureMessaging/SCKA/SPQR/Unchunked.lean

complete

def SPQR.CtSender.recvNextEpoch {AuthState : Type}
  (st : SPQR.CtSender.Ct2Sent AuthState) (t : ℕ) :
  Option (SPQR.EkSender.KeysUnsampled AuthState)

def SPQR.CtSender.recvNextEpoch
  {AuthState : Type}
  (st : SPQR.CtSender.Ct2Sent AuthState)
  (t : ℕ) :
  Option
    (SPQR.EkSender.KeysUnsampled
      AuthState)

Return the encapsulation-key-sender state exactly when `t` is the successor epoch.

Definition9.3.3

Statement uses 5

Statement dependency previews

Preview

Definition 4.1.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1XL∃∀N

\todo

LeanLean anchor pending

uses Definition 9.1.1 · Definition 9.3.1 · Definition 9.3.2 · Definition 4.1.2 · Definition 4.1.3 · github #263

Definition9.3.4

Group: Sparse Post-Quantum Ratchet (SPQR) ( ). (2)

Group member previews

Preview

Theorem 9.3.5

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 5

Statement dependency previews

Preview

Definition 4.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Theorem 9.3.5

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

XL∃∀N

\todo

LeanLean anchor pending

uses Definition 9.1.1 · Definition 9.3.1 · Definition 9.3.2 · Definition 9.3.3 · Definition 4.1.1 · github #268

Theorem9.3.5

Group: Sparse Post-Quantum Ratchet (SPQR) ( ). (2)

Group member previews

Preview

Definition 9.3.4

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 3

Statement dependency previews

Preview

Definition 4.1.4

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0XL∃∀N

\todo

LeanLean anchor pending

uses Definition 9.3.4 · Definition 9.1.3 · Definition 4.1.4 · github #269

Theorem9.3.6

Group: Sparse Post-Quantum Ratchet (SPQR) ( ). (2)

Group member previews

Preview

Definition 9.3.4

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 3

Statement dependency previews

Preview

Definition 4.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0XL∃∀N

\todo

LeanLean anchor pending

uses Definition 9.3.4 · Definition 9.1.4 · Definition 4.1.1 · github #270

References: