Skip to content

Network Identities

Types for network identities following the Anoma specification.

{-# OPTIONS --without-K #-}

module RM.Types.Identities where

open import Foundation.BasicTypes
open import RM.Types.Crypto

Basic Identifiers

ObjectId : Set
ObjectId = ℕ

Ciphertext : Set
Ciphertext = String

Plaintext : Set
Plaintext = String

Signable : Set
Signable = String

External and Internal Identities

ExternalId : Set
ExternalId = PublicKey

InternalId : Set
InternalId = PrivateKey

Identity : Set
Identity = ExternalId × InternalId

Commitments

Commitment : Set
Commitment = Signature

Node and Engine Identities

NodeId : Set
NodeId = ExternalId

EngineName : Set
EngineName = String

ExternalIdentity : Set
ExternalIdentity = EngineName

EngineId : Set
EngineId = Maybe NodeId × EngineName

Engine ID Predicates

isLocalEngineID : EngineId → Bool
isLocalEngineID (Maybe.nothing , _) = true
isLocalEngineID (Maybe.just _  , _) = false

isRemoteEngineID : EngineId → Bool
isRemoteEngineID = not ∘ isLocalEngineID

Identity Parameter Types

data IDParams : Set where
  Ed25519   : IDParams
  Secp256k1 : IDParams
  BLS       : IDParams

Backend Connection Types

data Backend : Set where
  localMemory      : Backend
  localConnection  : String → Backend
  remoteConnection : ExternalIdentity → Backend

Identity Capabilities

data Capabilities : Set where
  commit           : Capabilities
  decrypt          : Capabilities
  commitAndDecrypt : Capabilities
Module References

Referenced By

This module is referenced by:

References

This module references: