1. Core Data Types

The DID document data model supports multiple data types. We model this as an inductive type representing JSON-like values.

inductive W3C.DIDValue : Type

Core value types supported in DID documents

• string : String → DIDValue
• int : ℤ → DIDValue
• double : Float → DIDValue
• bool : Bool → DIDValue
• null : DIDValue
• list : List DIDValue → DIDValue
• map : List (String × DIDValue) → DIDValue

instance W3C.instReprDIDValue : Repr DIDValue

Equations

• W3C.instReprDIDValue = { reprPrec := W3C.reprDIDValue✝ }

2. DID Syntax

DID Syntax ABNF:

did                = "did:" method-name ":" method-specific-id
method-name        = 1*method-char
method-char        = %x61-7A / DIGIT  ; lowercase letters (a-z) and digits (0-9)
method-specific-id = *( *idchar ":" ) 1*idchar
idchar             = ALPHA / DIGIT / "." / "-" / "_" / pct-encoded
pct-encoded        = "%" HEXDIG HEXDIG

structure W3C.DID : Type

A DID (Decentralized Identifier) string. Must conform to the syntax: did:method:method-specific-id

• value : String

  The complete DID string

instance W3C.instReprDID : Repr DID

Equations

• W3C.instReprDID = { reprPrec := W3C.reprDID✝ }

instance W3C.instDecidableEqDID : DecidableEq DID

Equations

• W3C.instDecidableEqDID = W3C.decEqDID✝

structure W3C.MethodName : Type

Method name component of a DID

• value : String

instance W3C.instReprMethodName : Repr MethodName

Equations

• W3C.instReprMethodName = { reprPrec := W3C.reprMethodName✝ }

instance W3C.instDecidableEqMethodName : DecidableEq MethodName

Equations

• W3C.instDecidableEqMethodName = W3C.decEqMethodName✝

structure W3C.MethodSpecificId : Type

Method-specific identifier component

• value : String

instance W3C.instReprMethodSpecificId : Repr MethodSpecificId

Equations

• W3C.instReprMethodSpecificId = { reprPrec := W3C.reprMethodSpecificId✝ }

instance W3C.instDecidableEqMethodSpecificId : DecidableEq MethodSpecificId

Equations

• W3C.instDecidableEqMethodSpecificId = W3C.decEqMethodSpecificId✝

structure W3C.DIDURL : Type

DID URL extends DID with optional path, query, and fragment

• did : DID
• path : Option String
• query : Option String
• fragment : Option String

instance W3C.instReprDIDURL : Repr DIDURL

Equations

• W3C.instReprDIDURL = { reprPrec := W3C.reprDIDURL✝ }

instance W3C.instDecidableEqDIDURL : DecidableEq DIDURL

Equations

• W3C.instDecidableEqDIDURL = W3C.decEqDIDURL✝

3. Verification Methods

A verification method expresses verification material and metadata about it.

structure W3C.VerificationMethodType : Type

Verification method type identifier (e.g., Ed25519VerificationKey2020)

• value : String

instance W3C.instReprVerificationMethodType : Repr VerificationMethodType

Equations

• W3C.instReprVerificationMethodType = { reprPrec := W3C.reprVerificationMethodType✝ }

instance W3C.instDecidableEqVerificationMethodType : DecidableEq VerificationMethodType

Equations

• W3C.instDecidableEqVerificationMethodType = W3C.decEqVerificationMethodType✝

structure W3C.PublicKeyJwk : Type

Public key representation in JWK format

• kty : String

  Key type (e.g., "EC", "RSA", "OKP")

• properties : List (String × DIDValue)

  Additional JWK properties

instance W3C.instReprPublicKeyJwk : Repr PublicKeyJwk

Equations

• W3C.instReprPublicKeyJwk = { reprPrec := W3C.reprPublicKeyJwk✝ }

structure W3C.VerificationMethod : Type

A verification method defines cryptographic material for verification

• id : DIDURL

  REQUIRED: Identifier for the verification method (DID URL)

• type_ : VerificationMethodType

  REQUIRED: Type of verification method

• controller : DID

  REQUIRED: DID of the controller

• publicKeyJwk : Option PublicKeyJwk

  OPTIONAL: Public key in JWK format

• publicKeyMultibase : Option String

  OPTIONAL: Public key in multibase format

• additionalProperties : List (String × DIDValue)

  Additional properties specific to the verification method type

instance W3C.instReprVerificationMethod : Repr VerificationMethod

Equations

• W3C.instReprVerificationMethod = { reprPrec := W3C.reprVerificationMethod✝ }

inductive W3C.VerificationRelationship : Type

Verification relationship reference (either embedded or referenced)

• embedded : VerificationMethod → VerificationRelationship
• reference : DIDURL → VerificationRelationship

instance W3C.instReprVerificationRelationship : Repr VerificationRelationship

Equations

• W3C.instReprVerificationRelationship = { reprPrec := W3C.reprVerificationRelationship✝ }

4. Service Endpoints

Service endpoints express ways to interact with the DID subject.

structure W3C.ServiceType : Type

Service type identifier

• value : String

instance W3C.instReprServiceType : Repr ServiceType

Equations

• W3C.instReprServiceType = { reprPrec := W3C.reprServiceType✝ }

instance W3C.instDecidableEqServiceType : DecidableEq ServiceType

Equations

• W3C.instDecidableEqServiceType = W3C.decEqServiceType✝

inductive W3C.ServiceEndpointValue : Type

Service endpoint value (can be URI, map, or set)

• uri : String → ServiceEndpointValue
• map : List (String × DIDValue) → ServiceEndpointValue
• set : List ServiceEndpointValue → ServiceEndpointValue

instance W3C.instReprServiceEndpointValue : Repr ServiceEndpointValue

Equations

• W3C.instReprServiceEndpointValue = { reprPrec := W3C.reprServiceEndpointValue✝ }

structure W3C.ServiceEndpoint : Type

A service endpoint defines how to interact with the DID subject

• id : String

  REQUIRED: Identifier for the service endpoint

• type_ : List ServiceType

  REQUIRED: Type of service

• serviceEndpoint : ServiceEndpointValue

  REQUIRED: Service endpoint URI or structured data

• additionalProperties : List (String × DIDValue)

  Additional service-specific properties

instance W3C.instReprServiceEndpoint : Repr ServiceEndpoint

Equations

• W3C.instReprServiceEndpoint = { reprPrec := W3C.reprServiceEndpoint✝ }

5. DID Document

A DID document contains information about a DID subject.

structure W3C.DIDDocument : Type

A DID document is the core data structure

• id : DID

  REQUIRED: The DID that this document describes

• alsoKnownAs : List String

  OPTIONAL: Alternative identifiers for the DID subject

• controller : List DID

  OPTIONAL: Controllers authorized to make changes

• verificationMethod : List VerificationMethod

  OPTIONAL: Verification methods for the DID subject

• authentication : List VerificationRelationship

  OPTIONAL: Authentication verification relationships

• assertionMethod : List VerificationRelationship

  OPTIONAL: Assertion method verification relationships

• keyAgreement : List VerificationRelationship

  OPTIONAL: Key agreement verification relationships

• capabilityInvocation : List VerificationRelationship

  OPTIONAL: Capability invocation verification relationships

• capabilityDelegation : List VerificationRelationship

  OPTIONAL: Capability delegation verification relationships

• service : List ServiceEndpoint

  OPTIONAL: Service endpoints

• additionalProperties : List (String × DIDValue)

  Additional properties (extensibility)

instance W3C.instReprDIDDocument : Repr DIDDocument

Equations

• W3C.instReprDIDDocument = { reprPrec := W3C.reprDIDDocument✝ }

6. DID Resolution

DID resolution is the process of obtaining a DID document from a DID.

structure W3C.ResolutionMetadata : Type

DID resolution metadata

• contentType : Option String

  MIME type of the DID document representation

• error : Option String

  Error code if resolution failed

• additionalProperties : List (String × DIDValue)

  Additional metadata

instance W3C.instReprResolutionMetadata : Repr ResolutionMetadata

Equations

• W3C.instReprResolutionMetadata = { reprPrec := W3C.reprResolutionMetadata✝ }

structure W3C.DocumentMetadata : Type

DID document metadata

• created : Option String

  Timestamp of DID document creation

• updated : Option String

  Timestamp of last update

• deactivated : Bool

  Whether the DID is deactivated

• versionId : Option String

  Version identifier

• nextUpdate : Option String

  Expected next update time

• nextVersionId : Option String

  Expected next version identifier

• additionalProperties : List (String × DIDValue)

  Additional metadata

instance W3C.instReprDocumentMetadata : Repr DocumentMetadata

Equations

• W3C.instReprDocumentMetadata = { reprPrec := W3C.reprDocumentMetadata✝ }

structure W3C.ResolutionResult : Type

Result of DID resolution

• document : Option DIDDocument

  The resolved DID document (if successful)

• resolutionMetadata : ResolutionMetadata

  Metadata about the resolution process

• documentMetadata : DocumentMetadata

  Metadata about the DID document

instance W3C.instReprResolutionResult : Repr ResolutionResult

Equations

• W3C.instReprResolutionResult = { reprPrec := W3C.reprResolutionResult✝ }

7. Validation Predicates

Predicates for validating DID syntax and structure.

def W3C.isHexDigit (c : Char) : Bool

Check if a character is a hexadecimal digit

Equations

• W3C.isHexDigit c = decide ('0' ≤ c ∧ c ≤ '9' ∨ 'A' ≤ c ∧ c ≤ 'F' ∨ 'a' ≤ c ∧ c ≤ 'f')

def W3C.isMethodChar (c : Char) : Bool

Check if a character is a valid method character (lowercase letter or digit)

Equations

• W3C.isMethodChar c = decide ('a' ≤ c ∧ c ≤ 'z' ∨ '0' ≤ c ∧ c ≤ '9')

def W3C.isIdCharPlain (c : Char) : Bool

Check if a character is a valid idchar (without percent encoding)

Equations

• W3C.isIdCharPlain c = decide ('A' ≤ c ∧ c ≤ 'Z' ∨ 'a' ≤ c ∧ c ≤ 'z' ∨ '0' ≤ c ∧ c ≤ '9' ∨ c = '.' ∨ c = '-' ∨ c = '_')

def W3C.isValidPercentEncoded (chars : List Char) : Bool

Validate percent-encoded sequence at the beginning of a character list. Returns true if the list starts with %HH where H is a hex digit.

Equations

• W3C.isValidPercentEncoded ('%' :: h1 :: h2 :: tail) = decide (W3C.isHexDigit h1 = true ∧ W3C.isHexDigit h2 = true)
• W3C.isValidPercentEncoded chars = false

def W3C.validateIdChars : List Char → Bool

Helper function to validate method-specific-id character sequence

Equations

• W3C.validateIdChars [] = true
• W3C.validateIdChars ('%' :: h1 :: h2 :: rest) = if W3C.isHexDigit h1 = true ∧ W3C.isHexDigit h2 = true then W3C.validateIdChars rest else false
• W3C.validateIdChars (c :: rest) = if W3C.isIdCharPlain c = true then W3C.validateIdChars rest else false

def W3C.isValidMethodName (s : String) : Bool

Check if a string is a valid method name

Equations

• W3C.isValidMethodName s = decide (s.length > 0 ∧ s.all W3C.isMethodChar = true)

def W3C.isValidMethodSpecificId (s : String) : Bool

Check if a string is a valid method-specific-id. Must contain at least one character and only valid idchars or percent-encoded sequences.

Equations

• W3C.isValidMethodSpecificId s = decide (s.length > 0 ∧ W3C.validateIdChars s.data = true)

def W3C.parseDID (s : String) : Option (String × String)

Parse a DID string into its components. Returns (method, method-specific-id) if the string starts with "did:"

Equations

• One or more equations did not get rendered due to their size.

def W3C.validateDIDSyntax (did : DID) : Bool

Decidable validation for DID syntax. Returns true if the DID matches: did:method:method-specific-id

Equations

• W3C.validateDIDSyntax did = match W3C.parseDID did.value with | none => false | some (method, id) => decide (W3C.isValidMethodName method = true ∧ W3C.isValidMethodSpecificId id = true)

def W3C.isValidDIDSyntax (did : DID) : Prop

Basic syntax validation for DID strings (Prop version). A valid DID must match: did:method:method-specific-id

Equations

• One or more equations did not get rendered due to their size.

def W3C.isValidURLChar (c : Char) : Bool

Check if a character is valid in path, query, or fragment components. These can contain unreserved characters, percent-encoded, and some reserved characters.

Equations

• One or more equations did not get rendered due to their size.

def W3C.validateURLComponent : List Char → Bool

Validate URL component (path, query, or fragment) characters

Equations

• W3C.validateURLComponent [] = true
• W3C.validateURLComponent ('%' :: h1 :: h2 :: rest) = if W3C.isHexDigit h1 = true ∧ W3C.isHexDigit h2 = true then W3C.validateURLComponent rest else false
• W3C.validateURLComponent (c :: rest) = if W3C.isValidURLChar c = true then W3C.validateURLComponent rest else false

def W3C.validatePath (path : Option String) : Bool

Validate a path component (must be empty or start with '/')

Equations

• W3C.validatePath none = true
• W3C.validatePath (some p) = if p.isEmpty = true then true else if (p.get? 0 == some '/') = true then W3C.validateURLComponent p.data else false

def W3C.validateQuery (query : Option String) : Bool

Validate a query component

Equations

• W3C.validateQuery none = true
• W3C.validateQuery (some p) = W3C.validateURLComponent p.data

def W3C.validateFragment (fragment : Option String) : Bool

Validate a fragment component

Equations

• W3C.validateFragment none = true
• W3C.validateFragment (some p) = W3C.validateURLComponent p.data

def W3C.validateDIDURL (didurl : DIDURL) : Bool

Decidable validation for DIDURL syntax

Equations

• One or more equations did not get rendered due to their size.

def W3C.isValidDIDURL (didurl : DIDURL) : Prop

Prop version: A DIDURL is valid if all its components are valid

Equations

• W3C.isValidDIDURL didurl = (W3C.isValidDIDSyntax didurl.did ∧ W3C.validatePath didurl.path = true ∧ W3C.validateQuery didurl.query = true ∧ W3C.validateFragment didurl.fragment = true)

def W3C.hasPublicKey (vm : VerificationMethod) : Prop

A verification method must have at least one public key representation. Note: The W3C DID spec requires that verification methods MUST NOT contain private key material. This property is structurally guaranteed by the VerificationMethod type, which only includes public key fields.

Equations

• W3C.hasPublicKey vm = (vm.publicKeyJwk.isSome = true ∨ vm.publicKeyMultibase.isSome = true)

def W3C.verificationRelationshipExists (doc : DIDDocument) (vr : VerificationRelationship) : Prop

Check if a verification relationship reference exists in the document

Equations

• W3C.verificationRelationshipExists doc (W3C.VerificationRelationship.embedded a) = True
• W3C.verificationRelationshipExists doc (W3C.VerificationRelationship.reference a) = ∃ (vm : W3C.VerificationMethod), vm ∈ doc.verificationMethod ∧ vm.id = a

def W3C.allVerificationRelationshipsValid (doc : DIDDocument) : Prop

All verification relationships must be valid

Equations

• One or more equations did not get rendered due to their size.

def W3C.isValidDIDDocument (doc : DIDDocument) : Prop

A DID document is valid if it satisfies all requirements

Equations

• One or more equations did not get rendered due to their size.

8. Core Invariants

Key properties that must hold for DID documents.

def W3C.documentIntegrity (did : DID) (doc : DIDDocument) : Prop

Document Integrity: The DID document's id matches the resolved DID

Equations

• W3C.documentIntegrity did doc = (doc.id = did)

def W3C.controllerAuthority (doc : DIDDocument) : Prop

Controller Authority: A controller must be a valid DID

Equations

• W3C.controllerAuthority doc = ∀ (controller : W3C.DID), controller ∈ doc.controller → W3C.isValidDIDSyntax controller

def W3C.verificationMethodReferenceIntegrity (doc : DIDDocument) : Prop

Verification Method Reference Integrity

Equations

• W3C.verificationMethodReferenceIntegrity doc = W3C.allVerificationRelationshipsValid doc

9. Security Properties

Formal properties related to security and privacy.

def W3C.canAuthenticate (doc : DIDDocument) : Prop

A DID can be authenticated if it has authentication verification methods

Equations

• W3C.canAuthenticate doc = (doc.authentication.length > 0)

def W3C.canIssueCredentials (doc : DIDDocument) : Prop

A DID can issue credentials if it has assertion methods

Equations

• W3C.canIssueCredentials doc = (doc.assertionMethod.length > 0)

def W3C.canEstablishSecureComm (doc : DIDDocument) : Prop

A DID can establish secure communication if it has key agreement methods

Equations

• W3C.canEstablishSecureComm doc = (doc.keyAgreement.length > 0)

def W3C.canInvokeCapabilities (doc : DIDDocument) : Prop

A DID can invoke capabilities if it has capability invocation methods

Equations

• W3C.canInvokeCapabilities doc = (doc.capabilityInvocation.length > 0)

def W3C.canDelegateCapabilities (doc : DIDDocument) : Prop

A DID can delegate capabilities if it has capability delegation methods

Equations

• W3C.canDelegateCapabilities doc = (doc.capabilityDelegation.length > 0)

10. Well-formedness Theorems

theorem W3C.valid_document_has_integrity (did : DID) (doc : DIDDocument) : isValidDIDDocument doc → documentIntegrity did doc → doc.id = did

If a DID document is valid, it maintains document integrity

theorem W3C.valid_document_has_controller_authority (doc : DIDDocument) : isValidDIDDocument doc → controllerAuthority doc

Valid documents satisfy controller authority

theorem W3C.valid_document_has_vm_integrity (doc : DIDDocument) : isValidDIDDocument doc → verificationMethodReferenceIntegrity doc

Valid documents have verification method reference integrity

11. DID Syntax Validation Soundness

These theorems establish the relationship between decidable validation functions and their Prop specifications, ensuring that the computable validators are correct.

instance W3C.instDecidableEqBoolValidateDIDSyntaxTrue (did : DID) : Decidable (validateDIDSyntax did = true)

Decidable instance for DID syntax validation

Equations

• W3C.instDecidableEqBoolValidateDIDSyntaxTrue did = inferInstanceAs (Decidable (W3C.validateDIDSyntax did = true))

theorem W3C.valid_did_has_prefix (did : DID) : validateDIDSyntax did = true → did.value.startsWith "did:" = true

The DID prefix is always "did:" for any valid DID

theorem W3C.valid_method_name_nonempty (s : String) : isValidMethodName s = true → s.length > 0

Valid method names are non-empty

theorem W3C.valid_method_id_nonempty (s : String) : isValidMethodSpecificId s = true → s.length > 0

Valid method-specific IDs are non-empty

theorem W3C.parse_valid_did (did : DID) : validateDIDSyntax did = true → ∃ (method : String), ∃ (id : String), parseDID did.value = some (method, id)

Parsing a valid DID always succeeds

theorem W3C.validate_implies_components_valid (did : DID) : validateDIDSyntax did = true → ∃ (method : String), ∃ (id : String), parseDID did.value = some (method, id) ∧ isValidMethodName method = true ∧ isValidMethodSpecificId id = true

Validation consistency: if the decidable validator succeeds, the components are valid

theorem W3C.didurl_validation_monotonic (didurl : DIDURL) : validateDIDURL didurl = true → validateDIDSyntax didurl.did = true ∧ validatePath didurl.path = true ∧ validateQuery didurl.query = true ∧ validateFragment didurl.fragment = true

DIDURL validation is monotonic in its components

12. Example DIDs and Documents

def W3C.exampleDID : DID

Example DID

Equations

• W3C.exampleDID = { value := "did:example:123456789abcdefghi" }

def W3C.exampleVerificationMethod : VerificationMethod

Example verification method

Equations

• One or more equations did not get rendered due to their size.

def W3C.exampleServiceEndpoint : ServiceEndpoint

Example service endpoint

Equations

• One or more equations did not get rendered due to their size.

def W3C.exampleMinimalDocument : DIDDocument

Example minimal DID document

Equations

• W3C.exampleMinimalDocument = { id := W3C.exampleDID }

def W3C.exampleFullDocument : DIDDocument

Example full DID document

Equations

• One or more equations did not get rendered due to their size.

13. DID Syntax Validation Examples

These examples demonstrate the DID syntax validation functions in action.

def W3C.validDIDExamples : List DID

Valid DID examples

Equations

• One or more equations did not get rendered due to their size.

def W3C.invalidDIDExamples : List DID

Invalid DID examples

Equations

• One or more equations did not get rendered due to their size.

def W3C.testValidDIDs : List (DID × Bool)

Test validation of valid DIDs

Equations

• W3C.testValidDIDs = List.map (fun (did : W3C.DID) => (did, W3C.validateDIDSyntax did)) W3C.validDIDExamples

def W3C.testInvalidDIDs : List (DID × Bool)

Test validation of invalid DIDs

Equations

• W3C.testInvalidDIDs = List.map (fun (did : W3C.DID) => (did, W3C.validateDIDSyntax did)) W3C.invalidDIDExamples

def W3C.exampleDIDURL : DIDURL

Example DIDURL with all components

Equations

• W3C.exampleDIDURL = { did := { value := "did:example:123456789abcdefghi" }, path := some "/path/to/resource", query := some "service=agent&version=1.0", fragment := some "keys-1" }

def W3C.exampleDIDURLFragment : DIDURL

Example DIDURL with only fragment

Equations

• W3C.exampleDIDURLFragment = { did := { value := "did:example:123456789abcdefghi" }, fragment := some "keys-1" }

def W3C.testDIDURL1 : Bool

Test DIDURL validation

Equations

• W3C.testDIDURL1 = W3C.validateDIDURL W3C.exampleDIDURL

def W3C.testDIDURL2 : Bool

Equations

• W3C.testDIDURL2 = W3C.validateDIDURL W3C.exampleDIDURLFragment

def W3C.parseExample1 : Option (String × String)

Parsing examples

Equations

• W3C.parseExample1 = W3C.parseDID "did:example:123456789abcdefghi"

def W3C.parseExample2 : Option (String × String)

Equations

• W3C.parseExample2 = W3C.parseDID "did:web:example.com:user:alice"

def W3C.parseExample3 : Option (String × String)

Equations

• W3C.parseExample3 = W3C.parseDID "invalid:did"

14. Complete Validation Test Suite

This section provides a comprehensive test suite demonstrating all validation capabilities.

def W3C.testMethodNames : List (String × Bool)

Test method name validation

Equations

• One or more equations did not get rendered due to their size.

def W3C.testMethodSpecificIds : List (String × Bool)

Test method-specific-id validation

Equations

• One or more equations did not get rendered due to their size.