Identity

The base abstraction of the protocol is a knowledge-based identity interface, where the identity of an agent is defined entirely on the basis of whether or not they know some secret information.

Agents can use private information (likely randomness) to create an internal identity, from which they can derive an external identity to which it corresponds. The external identity can be shared with other parties. The agent who knows the internal identity can sign messages, which any agent who knows the external identity can verify, and any agent who knows the external identity can encrypt messages which the agent with knowledge of the internal identity can decrypt. This identity interface is independent of the particular cryptographic mechanisms, which may vary.

Identity Interface

Internal Identity

An internal identity includes private information necessary for signing and decryption. Formally, an internal identity has 2 parts: a Signer and a Decryptor. We specify both using SML signatures.

Signer SML Signature

A signature describing a type signer that can cryptographically sign (or credibly commit) to something (a signable), forming a commitment. Implementations should ultimately include, for example BLS keys, which should be able to sign anything that can be marshaled into a bitstring.

Properties:

• In general, every S:SIGNER needs a corresponding V:VERIFIER, and every s:S.signer needs a corresponding v:V.verifier, such that:

• For any message m: verify v m x = (x = (sign s m))

• for most cryptosystems, a computationally bounded adversary should not be able to approximate s knowing only v.

signature SIGNER = sig
  type signer
  type signable
  type commitment
  val sign : signer -> signable -> commitment
end

Decryptor SML Signature

A signature describing a type decryptor that can cryptographically decrypt something (a cyphertext), resulting in a plaintext (or NONE, if decryption fails). Implementations should ultimately include, for example, AES-256 keys, which should be able to decrypt bitstrings into anything that can be unmarshaled from a bitstring.

Properties:

• a computationally bounded adversary should not be able to approximate decrypt d without knowledge of d.

• decrypt should take polynomial time (in the size of its inputs)

• Each D:DECRYPTOR should have a corresponding E:ENCRYPTOR, and each d: D.decryptor has a corresponding e: E.encryptor such that:

• for all c : D.cyphertext, p : D.plaintext: D.decrypt d c = Some p iff c = E.encrypt e p

• if d = e, we call this "symmetric encryption," and otherwise it's "asymmetric encryption"

signature DECRYPTOR = sig
  type decryptor
  type plaintext
  type cyphertext
  val decrypt : decryptor -> cyphertext -> plaintext option
end

Internal Identity SML Signature

An Internal Identity structure, then, simply specifies everything specified by both Signer and Decryptor.

An Internal Identity structure specifies the necessary types and functions for both a Signer and a Decryptor. Implementations should ultimately include, for example, RSA private keys, which should be able to decrypt integers into anything that can be unmarshaled from a bitstring, and sign anything which can be marshaled into a bytestring to form an integer.

An internal_identity includes:

• a type signer that can cryptographically sign (or credibly commit) to something (a signable), forming a commitment.

• a type decryptor that can cryptographically decrypt something (a cyphertext), resulting in a plaintext (or NONE, if decryption fails).

Properties are inherited from SIGNER and DECRYPTOR.

signature INTERNAL_IDENTITY = sig
  include SIGNER
  include DECRYPTOR
end

External Identity

An external identity includes only public information. An external identity can verify signatures produced by an internal identity, and encrypt messages the internal identity can then decrypt. Formally, an external identity has 2 parts: a Verifier and an Encryptor. Each is hashable: any structure specifying Verifier and Encryptor types must also specify a hash function, so that external identities can be specified by hash.

Verifier SML Signature

A signature describing a type verifier that can cryptographically verify that a commitment (or cryptographic signature) corresponds to a given message (a signable), and was signed by the signer corresponding to this verifier. A verifier can be hashed (producing a unique identifier), so a structure with signature VERIFIER must specify a VerifierHash structure defining a suitable hash function. Implementations should ultimately include, for example BLS identities.

Properties:

• In general, every V:VERIFIER needs a corresponding S:SIGNER, and every s:S.signer needs a corresponding v:V.verifier, such that:

• For any message m: verify v m x = (x = (sign s m))

• for most cryptosystems, a computationally bounded adversary should not be able to approximate s knowing only v.

signature VERIFIER = sig
  type verifier
  type signable
  type commitment
  val verify : verifier -> signable -> commitment -> bool
  structure VerifierHash : HASH sharing type VerifierHash.hashable = verifier
end

Encryptor SML Signature

A signature describing a type encryptor that can cryptographically encrypt a plaintext (message) to create a ciphertext readable only by the corresponding decryptor. An encryptor can be hashed (producing a unique identifier), so a structure with signature ENCRYPTOR must specify an EncryptorHash structure defining a suitable hash function. Implementations should ultimately include, for example, AES-256 keys, which should be able to decrypt bitstrings into anything that can be unmarshaled from a bitstring.

Properties:

• encrypt should take polynomial time (in the size of its inputs)

• Each E:ENCRYPTOR should have a corresponding D:DECRYPTOR, and each d: D.decryptor has a corresponding e: E.encryptor such that:

• for all c : D.cyphertext, p : D.plaintext: D.decrypt d c = Some p iff c = E.encrypt e p

• if d = e, we call this "symmetric encryption," and otherwise it's "asymmetric encryption." In an asymmetric cryptosystem, a computationally bounded adversary should not be able to approximate d knowing only e.

signature ENCRYPTOR = sig
  type encryptor
  type plaintext
  type ciphertext
  val encrypt : encryptor -> plaintext -> ciphertext
  structure EncryptorHash : HASH sharing type EncryptorHash.hashable = encryptor
end

External Identity SML Signature

An external identity, then, simply specifies everything specified by both Verifier and Encryptor.

An External Identity structure specifies the necessary types and functions for both a Verifier and an Encyrptor. Implementations should ultimately include, for example, RSA public keys.

An external_identity includes:

• a type verifier that can cryptographically verify that a commitment (or cryptographic signature) corresponds to a given message (a signable), and was signed by the signer corresponding to this verifier.

• a type encryptor that can cryptographically encrypt a plaintext (message) to create a cyphertext readable only by the corresponding decryptor.

Properties are inherited from VERIFIER and ENCRYPTOR.

signature EXTERNAL_IDENTITY = sig
  include VERIFIER
  include ENCRYPTOR
end

Identity SML Signature

An Identity structure, formally, specifies all the types for corresponding internal and external identities. So, for a given Identity structure I, I.verifier should be the type of objects that can verify commitments produced by a corresponding object of type I.signer. Likewise, I.decryptor should be the type of objects that can decrypt cyphertexts produced by a corresponding object of type I.encryptor. Implementations should ultimately include, for example, RSA public / private keys sytems.

An Identity includes:

• a type signer that can cryptographically sign (or credibly commit) to something (a signable), forming a commitment.

• a type decryptor that can cryptographically decrypt something (a cyphertext), resulting in a plaintext (or NONE, if decryption fails).

• a type verifier that can cryptographically verify that a commitment (or cryptographic signature) corresponds to a given message (a signable), and was signed by the signer corresponding to this verifier.

• a type encryptor that can cryptographically encrypt a plaintext (message) to create a cyphertext readable only by the corresponding decryptor.

Properties are inherited from VERIFIER, ENCRYPTOR, SIGNER, and DECRYPTOR.

signature IDENTITY = sig
  include  INTERNAL_IDENTITY
  include  EXTERNAL_IDENTITY
end

SignsFor Relation

Some identities may have the authority to sign statements on behalf of other identities. For example, Alice might grant Bob the authority to sign arbitrary messages on her behalf. We write this relationship as Bob signsFor Alice.

In general, signsFor is a partial order over identitites. This means signsFor is transitive: if A signsFor B and B signsFor C, then A signsFor C. The signsFor relation becomes especially useful with regard to composed identities, discussed below.

SignsFor Evidence

We do not specify all the ways one might know if one identity signsFor another. In general, an Identity Engine might accept (and perhaps store) a variety of forms of evidence as proof. As one simple form of evidence, we can specify a format for signed statements from B that proves some specified A signsFor B.

Note that signsFor evidence cannot be revoked, and so a signsFor relation is not stateful: it cannot depend on the current state of, for example, a blockchain.

SignsFor SML Signature

Formally, a signsFor relation requires a type of evidence, and a VERIFIER structure. This codifies a belief about what verifier's commitments are "at least as good as" another verifier's. Evidence can be signed statements, proofs, or even local state about beliefs.

For example, suppose Alice wants to grant authority to Bob to sign on her behalf. Nodes who want to take this into account might accept some sort of e:evidence, perhaps a signed statement from Alice, so that they can recognize that signsFor e (Bob, Alice).

Note that signsFor is not symmetric: signsFor e (x,y) does not imply that any z exists such that signsFor z (y,x).

signature SIGNS_FOR = sig
  structure Verifier : VERIFIER
  type evidence
  val signsFor : evidence -> (Verifier.verifier * Verifier.verifier) -> bool
end

SignsFor Equivalence

We can also define a kind of identity equivalence: A signsSameAs B precisely when A signsFor B and B signsFor A. This means that (in general), if you want to sign a message as A, but for whatever reason it's cheaper to sign a message as B, it's safe to just use B instead, and vice versa.

ReadsFor Relation

Similar to signsFor, it is useful to sometimes note that one identity can read information encrypted to another identity. For example, suppose Alice gives her private decryptor to Bob, and wants to let everyone know that Bob can now read anything encrypted to Alice. Nodes who want to take this into account might accept some sort of evidence, perhaps a signed statement from Alice, so that they can recognize that Bob readsFor Alice.

Like signsFor, readsFor is a partial order over identitites. This means readsFor is transitive: if A readsFor B and B readsFor C, then A readsFor C. The readsFor relation becomes especially useful with regard to composed identities, discussed below.

ReadsFor Evidence

We do not specify all the ways one might know if one identity readsFor another. In general, an Identity Engine might accept (and perhaps store) a variety of forms of evidence as proof. As one simple form of evidence, we can specify a format for signed statements from B that proves A readsFor B.

ReadsFor SML Signature

Formally, a readsFor relation requires a type of evidence, and an ENCRYPTOR structure. This codifies a belief about what DECRYPTORs can read other ENCRYPTORs ciphertext. Evidence can be signed statements, proofs, or even local state about beliefs.

Specifically, if a node expresses a readsFor relation, and readsFor e (x,y), then the node believes that any node knowing the decryptor corresponding to x can decrypt encrypt y p. If there is some plaintext p such that some node knowing a decryptor corresponding to x cannot read encrypt y p, then the node's beliefs, as encoded in the readsFor relation, are incorrect.

For example, suppose Alice gives her private decryptor to Bob, and wants to let everyone know that Bob can now read anything encrypted to Alice. Nodes who want to take this into account might accept some sort of e:evidence, perhaps a signed statement from Alice, so that they can recognize that readsFor e (Bob, Alice).

Note that readsFor is not symmetric: readsFor e (x,y) does not imply that any z exists such that readsFor z (y,x).

signature READS_FOR = sig
  structure Encryptor : ENCRYPTOR
  type evidence
  val readsFor : evidence -> (Encryptor.encryptor * Encryptor.encryptor) -> bool
end

Equivalence

We can also define a kind of identity equivalence: A readsSameAs B precisely when A readsFor B and B readsFor A. This means that, in general, if you want to encrypt a message to A, but for whatever reason it's cheaper to encrypt a message for B, it's safe to just use B instead, and vice versa.

In total, A equivalent B when A readsSameAs B and A signsSameAs B. This means that (in general) A and B can be used interchangeably.

Composition

There are a variety of ways to refer to groups of identities as single, larger identities.

Threshold Composition

Suppose we want an identity M that refers to any majority from a set of shareholders. A signature from M would require that a majority of shareholders participated in signing, and encrypting information for M would require that a majority of shareholders participate in decryption. To construct M, we start with a set of shareholder identities, each paired with a weight (their share), and define a weight threshold which specifies the minimum weight for a "majority."

There are several ways we could imagine constructing Threshold Composition Identities, but without specifying anything about the underlying identities:

• A threshold composition identity signature is a map from (hashes of) external identities, to signatures. To verify a signature for some message x, we verify each signature with x and its external identity, and check that the weights of the external identities sum to at least the threshold.
• A threshold composition identity encrypted message is a map from (hashes of) external identities, to ciphertexts. To decrypt, any subset of internal identitites with weights summing to at least the threshold must decrypt their corresponding ciphertexts, and the resulting plaintexts must be combined using an erasure coding scheme.

Threshold Composition SML Signature (Signer and Verifier)

A ThresholdCompose verifier consists of a threshold (int), and a set of verifiers, each paired with a weight (int). (this set is encoded as a Map.map from hashes of verifiers to int * verifier pairs). commitments are simply Maps from hashes of the underlying identities to commitments signed by that identitity. A commitment verifies iff the set of valid commitments included correspond to a set of verifiers whose weights sum to at least the threshold. Note that this satisfies both signatures VERIFIER and SIGNER.

In general, ThresholdCompose signers and verifiers may not be used much directly. Instead, nodes can make more efficient identities (using cryptographic siganture aggregation techniques), and express their relationship to ThresholdCompose verifiers as a SIGNS_FOR relationship. This will let nodes reason about identities using simple ThresholdCompose verifiers, while actually using more efficient implementations.

Formally, to specify a ThresholdCompose, we need:

• Verifier, the structure of the underlying verifiers.

• Signer, the corresponding structure of the underlying signers.

• Map : ORD_MAP, to be used to encode weights and commitments. (Note that this needs Map.Key to be the hash type of the underlying Verifier)

• ThresholdComposeHash, which specifies a hash function that can hash our composed verifiers (type {threshold:int, weights : ((int * Verifier.verifier) Map.map)}).

A ThresholdCompose structure provides:

• structure Map : ORD_MAP the underlying ORD_MAP used in verifier and commitment

• structure UnderlyingVerifier : VERIFIER the structure describing the types of the underlying verifiers which can be composed.

• structure UnderlyingSigner : SIGNER the structure describing the types of the underlying signers which can be composed.

• structure VerifierHash : HASH describes the hash function for hashing these composed verifiers

• type signer is the type of composed signers. These are just UnderlyingSigner.signer Map.map, meaning each is stored under the hash of the corresponding UnderlyingVerifier.verifier. signer does not need to encode weights or threshold.

• type verifier the type of composed verifiers. These are {threshold:int, weights : ((int * UnderlyingVerifier.verifier) Map.map)}

• type signable the type of message that can be signed. This is exactly the same as what the underlying verifiers can sign (UnderlyingVerifier.signable).

• type commitment describes composed signatures, these are a Map.map from hashes of underlying verifiers (UnderlyingVerifier.VerifierHash.OrdKey.ord_key) to signatures (UnderlyingVerifier.commitment)

• fun sign creates a commitment using all UnderlyingSigner.signers in the composed signer.

• fun verify returns true iff the set of valid commitments included correspond to a set of UnderlyingVerifier.verifiers whose weights sum to at least the threshold.

• fun signerCompose is constructs a composed signer from a list of UnderlyingVerifier.verifier * UnderlyingSigner.signer pairs. Note that each signer must be paired with its correct verifier, or the composed signer will not produce verifiable commitments.

• fun verifierCompose is useful for constructing the composition of a list of verifiers. Returns a composed verifier. Its arguments are:

• the threshold (int)

• a list of weight (int), UnderlyingVerifier.verifier pairs.

• fun verifierAnd creates a composed verifier that is the "&&" of two input verifiers: a signer must encode the information of the signers for both x and y to sign statements verifierAnd x y will verify.

• fun verifierOr creates a composed verifier that is the "||" of two input verifiers: a signer must encode the information of the signers for either x or y to sign statements verifierOr x y will verify.

functor ThresholdCompose (
  structure Verifier:VERIFIER
  structure Signer:SIGNER sharing Signer = Verifier
  structure Map : ORD_MAP sharing Map.Key = Verifier.VerifierHash.OrdKey
  structure ThresholdComposeHash : HASH
    where type hashable = {threshold:int, weights : ((int * Verifier.verifier) Map.map)}
  ) = struct
  structure Map = Map
  structure UnderlyingVerifier = Verifier
  structure UnderlyingSigner = Signer
  structure VerifierHash = ThresholdComposeHash
  type signer = UnderlyingSigner.signer Map.map
  type verifier = VerifierHash.hashable
  type signable = UnderlyingVerifier.signable
  type commitment = UnderlyingVerifier.commitment Map.map
  fun sign s m = Map.map (fn i => UnderlyingSigner.sign i m) s
  fun verify {threshold = t, weights = ws} s c = t <= (Map.foldl op+ 0 (
    Map.intersectWith (fn ((w,v), x) => if UnderlyingVerifier.verify v s x then w else 0) (ws, c)))
  fun signerCompose (l : (UnderlyingVerifier.verifier * UnderlyingSigner.signer) list) : signer =
    foldl (fn ((v,s), m) => Map.insert(m, UnderlyingVerifier.VerifierHash.hash v, s)) Map.empty l
  fun verifierCompose (threshold : int)
                      (weights : (int * UnderlyingVerifier.verifier) list)
                      : verifier =
    {threshold = threshold,
     weights = foldl (fn ((w,v), m) =>
       Map.insert(m, UnderlyingVerifier.VerifierHash.hash v, (w, v))) Map.empty weights}
  fun verifierAnd (x: UnderlyingVerifier.verifier)
                  (y: UnderlyingVerifier.verifier)
                  : verifier = verifierCompose 2 [(1,x), (1,y)]
  fun verifierOr (x: UnderlyingVerifier.verifier)
                 (y: UnderlyingVerifier.verifier)
                 : verifier = verifierCompose 1 [(1,x), (1,y)]
end

While this construction is rather naive, it is general, and crucially, we can reason about equivalence with any number of more interesting schemes:

• We can show that a threshold RSA signature scheme signsSameAs as a Threshold Composition Identity.
• We can show that a secret sharing scheme readsSameAs a Threshold Composition Identity.

By phrasing our discussion in terms of equivalence and Threshold Composition Identities, we can abstract over the actual cryptography used. We can also derive some signsFor and readsFor relations that must hold, by looking at the relations that must hold for Threshold Composition Identities:

signsFor Threshold Composition

Like any identity, Threshold Composition Identities can define any number of ways to delegate signing power, or be delegated signing power. However, some cases should always hold: A signsFor B if every identity in A has no more weight (divided by threshold) than identities it signsFor in B. This implies that any collection of identities that can sign as A can also sign as B.

functor ThresholdComposeSignsFor(structure S:SIGNS_FOR
  structure Signer:SIGNER sharing Signer = S.Verifier
  structure Map : ORD_MAP sharing Map.Key = S.Verifier.VerifierHash.OrdKey
  structure ThresholdComposeHash : HASH
    where type hashable = {threshold:int, weights : ((int * S.Verifier.verifier) Map.map)}
  ) : SIGNS_FOR = struct
  structure UnderlyingSignsFor = S
  structure Verifier : VERIFIER = ThresholdCompose(
    structure Map = Map
    structure Signer = Signer
    structure Verifier = UnderlyingSignsFor.Verifier
    structure ThresholdComposeHash = ThresholdComposeHash)
  type evidence = S.evidence
  fun signsFor e ({threshold = t0, weights = w0}, {threshold = t1, weights = w1}) =
    Map.all (fn (w,v) => w*t1 <= (Map.foldl (fn ((x,v1), s) =>
      if UnderlyingSignsFor.signsFor e (v, v1) then x+s else s) 0 w1)*t0) w0
end

readsFor Threshold Composition

Like any identity, ThresholdCompositionIdentities can have arbitrary readsFor relationships. However, some cases should always hold: A readsFor B if every identity in A has no more weight (divided by threshold) than identities it readsFor in B. This implies that any collection of identities that can read messages encrypted with A can also read messages encrypted as B.

functor ThresholdComposeReadsFor(structure R:READS_FOR
    structure Map : ORD_MAP sharing Map.Key = R.Encryptor.EncryptorHash.OrdKey
    structure ThresholdComposeHash : HASH
      where type hashable = {threshold:int, weights : ((int * R.Encryptor.encryptor) Map.map)}
  ) : READS_FOR = struct
  structure UnderlyingReadsFor = R
  structure Encryptor = ThresholdComposeEncryptor(
    structure Map = Map
    structure Encryptor = UnderlyingReadsFor.Encryptor
    structure ThresholdComposeHash = ThresholdComposeHash)
  type evidence = UnderlyingReadsFor.evidence
  fun readsFor e ({threshold = t0, weights = w0}, {threshold = t1, weights = w1}) =
    Map.all (fn (w,v) => w*t1 <= (Map.foldl (fn ((x,v1), s) =>
      if UnderlyingReadsFor.readsFor e (v, v1) then x+s else s) 0 w1)*t0) w0
end

"And" Identities

We can compose identities with conjunction: A && B is the identity which requires an agent to have both A's internal identity and B's internal identity to sign or decrypt. It represents A and B working together. In practice, A && B can be defined as a special case of Threshold composition (see verifierAnd above).

"Or" Identities

We can compose identities with disjunction as well: A || B requires an agent to have either A's internal identity or B's internal identity. It represents either A or B, without specifying which. In practice, A || B can be defined as a special case of Threshold Composition (see verifierOr above).

In principle, we could define things differently: Threshold Composition could be defined using && and || as primitives, by building a disjunction of every possible conjunction that satisfies the threshold. In several important cases, however, this takes much more space to express, so we use the equally general and more numerically efficient threshold composition abstraction.

Opaque Composition

A group of agents can also compose an opaque identity, s.t. composition information is not available to the outside. One example would be a using distributed key generation and a threshold cryptosystem e.g. Threshold RSA. Here the agents compute one RSA keypair together, with only shares of the private key being generated by each agent. Decryption of messages encrypted to the single public key then requires cooperation of a subset of agents holding key shares, fulfilling the threshold requirements. This group would have a single External Identity based on a regular RSA public key, and it would not necessarily be clear how the identity was composed.

Specific evidence could prove that this threshold cryptosystem identity is equivalent to some ThresholdCompose identity. This kind of proof requires readsFor and signsFor relations tailored to the cryptosystem used. Once equivalence is proven, however, one could use the threshold cryptosystem identity for efficiency, but reason using the ThresholdCompose identity.

Special identities

The following special identities illustrate the generality of our identity abstractions:

"True / All"

Anyone can sign and decrypt (verify returns true and encrypt returns the plaintext). No secret knowledge is required, so all agents can take on this identity.

The true identity preserves structure under conjunction (x && true equivalent x) and forgets structure under disjunction (x || true equivalent true).

"False / None"

No one can sign or decrypt (verify returns false and encrypt returns empty string). No secret knowledge exists that fulfills these requirements, so no agent can take on this identity.

The false identity forgets structure under disjunction (x && false equivalent false) and preserves structure under disjunction (x || false equivalent x).

Identity Names

Sometimes it is useful to have a name for an external identity before the relevant cryptographic values are available. For example, we might refer to "a quorum of validators from chain X at epoch Y". Before epoch Y has begun, chain X may not have yet decided who constitutes a quorum.

It would be possible to build a Verifier, where the evidence that the signers are in fact a quorum of validators from chain X at epoch Y is part of the signature. One might later build a simpler Verifier, which elides this evidence, and then prove that the two signsSameAs using the evidence. However, barring some really exciting cryptography, we'd need to know the quorums from chain X at epoch Y before we could make an Encryptor.

We therefore introduce a new type, Identity Name, which represents a placeholder to be filled in when an appropriate external identity can be found. Specifically, each type of identity name comes with a predicate, which can be satisfied by an external identity, and accompanying evidence. Identity names can also be hashed, like external identities.

Identity names can be described in 2 structures: one for checking that a verifier corresponds with an identityName, and one for checking that an encryptor corresponds with an identityName. The same name can refer to to both a verifier and an encryptor.

Verifier Name SML Signature

An identityName can be mapped to an appropriate Verifier.verifier when suitable evidence is found. Here, checkVerifierName defines what evidence is acceptable for a Verifier.verifier.

Note that identityNames are also hashable: we require a structure VerifierNameHash that details how to hash them.

signature VERIFIER_NAME = sig
  structure Verifier : VERIFIER
  type evidence
  type identityName
  val checkVerifierName : identityName -> Verifier.verifier -> evidence -> bool
  structure VerifierNameHash : HASH sharing type VerifierNameHash.hashable = identityName
end

Encryptor Name SML Signature

An identityName can be mapped to an appropriate Encryptor.encryptor when suitable evidence is found. Here, checkEncryptorName defines what evidence is acceptable for a Encryptor.encryptor. Note that identityNames are also hashable: we require a structure EncryptorNameHash that details how to hash them.

signature ENCRYPTOR_NAME = sig
  structure Encryptor : ENCRYPTOR
  type evidence
  type identityName
  val checkEncryptorName : identityName -> Encryptor.encryptor -> evidence -> bool
  structure EncryptorNameHash : HASH sharing type EncryptorNameHash.hashable = identityName
end

For example, for the identity name "a quorum of validators from chain X at epoch Y", a satisfying external identity would be composed from the validators selected for epoch Y, and the accompanying evidence would be a light-client proof from chain X that these are the correct validators for epoch Y.

Note that multiple identity names can refer to the same external identity, and in principle, multiple external identities could have the same identity name. Usually, multiple external identities only have the same identity name when there is Byzantine behavior, but that is not explicitly part of the identity abstractions at this layer.

Sub-Identities

One particularly common case for identity names is when one party (the super-identity) wants to designate a specific name they use to refer to another identity. Here, the super-identity is acting like a certificate authority: they designate which external identity corresponds with this identity name. This sub-identity is often something the super-identity controls: a specific machine they own, or a process they run on that machine. Such a sub-identity might be associated with a string, such as "acceptor", which might designate the process participating in consensus within a validator. In this case, the predicate should check that the super-identity has signed a statement declaring that the external identity matches the sub-identity.

"." Notation

Because sub-identities using string names are so common, we have a short-cut notation for expressing identity names. Given some identity Alice, for any string "foo", Alice.foo is an identity name. For example, even before they learn anything about Alice, validators might refer to Alice.acceptor to mean the specific process Alice is running to participate in consensus. The identity Alice can sign statements to let people know what external identity they should (immutably) use for Alice.foo or Alice.acceptor. These are left associative, so Alice.foo can designate Alice.foo.bar (shorthand for (Alice.foo).bar) and Alice.foo.bar can designate Alice.foo.bar.baz (shorthand for ((Alice.foo).bar).baz), and so on. These are a special case of sub-identities: X.Y is a sub-identity of X.

Formally, we use (hash(Alice), "foo") as the SML representation of Alice.foo:

A specific kind of identity name, wher ethe evidence is a signed statement from a specified parent saying that it associates this verifier with a specific name.

Here,

• name is the type the parent identifies with a child. For example, for name = string, and some identity Alice, we can specify (hash(Alice),"bob"), or Alice.bob, as the identity that Alice refers to as "bob".

• Child : VERIFIER type that can be identified with a name.

• Parent : VERIFIER type that signs evidence statements.

Crucially, it must be able to sign tuples of the form (string, name, Child's hash type) In our example, where Alice refers to Bob as Alice."bob", Child describes Bob, Parent describes Alice, and name describes "bob".

• Hash Describes what will become the VerifierNameHash. Crucially, it must be able to hash pairs of the form (Parent's hash type, name)

functor SubVerifier (
  type name
  structure Child : VERIFIER
  structure Parent : VERIFIER where type signable = string * name * Child.VerifierHash.OrdKey.ord_key
  structure Hash : HASH where type hashable = Parent.VerifierHash.OrdKey.ord_key * name
  ) : VERIFIER_NAME = struct
  structure Verifier = Child
  structure VerifierNameHash = Hash
  type evidence = Parent.verifier * Parent.commitment
  type identityName = Parent.VerifierHash.OrdKey.ord_key * name
  fun checkVerifierName (ph, n) c (pv, pc)  =
    (Parent.verify pv ("I identify this Verifier with this name: ", n, Child.VerifierHash.hash(c)) pc)
    andalso (Parent.VerifierHash.OrdKey.compare(ph,(Parent.VerifierHash.hash pv)) = EQUAL)
end

In other words, we have a specific, standardized thing an external identity can sign to designate that another external identity corresponds to a "." name.

Note that we can use "." sub-identities for purposes other than identifying identities that the super-identity controls. Alice might have a friend Bob, and designate his external identity as Alice.bob. This is an example a place where "sub-identity-ness" is not transitive: Alice.bob.carol is (Alice.bob).carol, a sub-identity of Alice.bob, so it is up to Bob to designate which external identity he associates with "carol", and Alice has no say: Alice.bob.carol is not a sub-identity of Alice.

Identity Engine

In practice, using Identity Names requires each physical machine to maintain a mapping from identity names to known external identities. The machine does not have to store the accompanying evidence for each, although it might be useful to do so sometimes (for example, in order to present to a third party). When any process on that machine wants to do any operation using an identity name instead of an external identity, it can query this mapping to see if there is a known external identity to use for that operation.

An Identity Engine can also store evidence for known signsFor and readsFor relationships, and help choose which external identity is most efficient for a task. For example, if an agent wants to encrypt a message to "a quorum of validators from chain X at epoch Y", they would first resolving the identity name to an identity (possibly a Threshold Composed Identity), and might then ask if there is some known equivalent identity (such as a threshold encryption identity) with cheaper encryption.

Identity Name Resolution

There is no general mechanism for finding external identities (and accompanying evidence) for arbitrary identity names, with arbitrary forms of evidence. However, for some common types of identity names, such as "." sub-identities, we can establish a standard server and query language, which participating Identity Engines can query to resolve those identity names.