Dijkstra Cryptographic Primitives

Leios (CIP-164) adds a second signature scheme beside the payment scheme of the core Crypto module; specifically, an epoch's voting committee signs endorser-block announcements with registered voting keys, and a certificate encodes a quorum of votes as one aggregate signature.

This module defines the record LeiosCryptoStructure, an extension of CryptoStructure that adds what Leios needs. An inhabitant of LeiosCryptoStructure is added as a new field of GovStructure.

{-# OPTIONS --safe #-}
module Ledger.Dijkstra.Specification.Crypto where

open import Ledger.Prelude
open import Relation.Binary using (DecTotalOrder; IsDecTotalOrder)
open import Ledger.Core.Specification.Crypto

Abstract Cryptography Types

We represent the cryptographic structures of the Leios voting scheme using abstract types to encode verification keys, signatures, and proofs of possession.

record LeiosCryptoStructure (cs : CryptoStructure) : Type₁ where
  open CryptoStructure cs

  field
    BlsVKey BlsSig BlsPoP  : Type
    isValidPoP             : BlsVKey → BlsPoP → Type
    isSignedByAggregate    : ℙ BlsVKey → Ser → BlsSig → Type

• isValidPoP checks a voting key's proof of possession (PoP), which every registration carries (Key Registration and Rotation) because aggregation is otherwise open to rogue-key attacks.¹
• isSignedByAggregate verifies a certificate's aggregate signature over a message, given in serialized form, against the keys of the seats that signed.

The keys form a set rather than a list. A voting key can be registered by at most one pool, which is a premise of the registration rule (see POOL); so no two seats share a key, and an aggregate signature is determined by which keys signed, not by how often or in what order.

Pool Ordering

The committee of an epoch consists of a subset of pools, which includes those pools with the most active stake, with ties broken by pool id in ascending order (Committee Structure; the procedure in Committee Selection). Since type of pool id, KeyHash, is abstract, we augment it with a total ordering relation.

  field
    _≤ᵏʰ_      : KeyHash → KeyHash → Type

    ≤ᵏʰ-isDTO  : IsDecTotalOrder _≡_ _≤ᵏʰ_

Leios Hashes

Leios names its objects by hash.

• EBHash identifies an endorser block;
• TxRefHash identifies a referenced transaction by the hash of its complete bytes, not by its transaction id;
• RBHeaderHash identifies the announcing ranking-block header, the message a certificate is verified against (Certificate Validation);
• hashEBRefs encodes an endorser block's identifier from its reference list;
• rbHeaderHashBytes serializes a header hash into the message the aggregate verifier takes, just as txidBytes does for transaction ids.

All of these are abstract, and the Leios.Types module explains why the identifier's byte-exact preimage is deliberately unpinned.

  field
    EBHash TxRefHash RBHeaderHash  : Type
    hashEBRefs                     : List (TxRefHash × ℕ) → EBHash
    rbHeaderHashBytes              : RBHeaderHash → Ser

  field
    ⦃ DecEq-BlsVKey ⦄            : DecEq BlsVKey
    ⦃ DecEq-BlsSig  ⦄            : DecEq BlsSig
    ⦃ DecEq-BlsPoP  ⦄            : DecEq BlsPoP
    ⦃ Dec-isValidPoP ⦄           : isValidPoP ⁇²
    ⦃ Dec-isSignedByAggregate ⦄  : isSignedByAggregate ⁇³
    ⦃ DecEq-EBHash ⦄             : DecEq EBHash
    ⦃ DecEq-TxRefHash ⦄          : DecEq TxRefHash
    ⦃ DecEq-RBHeaderHash ⦄       : DecEq RBHeaderHash

  DTO-KeyHash : DecTotalOrder 0ℓ 0ℓ 0ℓ
  DTO-KeyHash = record { Carrier = KeyHash ; _≈_ = _≡_ ; _≤_ = _≤ᵏʰ_ ; isDecTotalOrder = ≤ᵏʰ-isDTO }

---

---

1. A key crafted relative to someone else's key could make the aggregate appear as if it includes a voter who never signed. ↩