1. Core Value Types

Reuse DIDValue from W3C.DID for representing JSON-like values.

2. Context and Type Definitions

Credentials use JSON-LD contexts and types for semantic meaning.

structure W3C.Context : Type

JSON-LD context URI or object

• value : String

instance W3C.instReprContext : Repr Context

Equations

• W3C.instReprContext = { reprPrec := W3C.reprContext✝ }

instance W3C.instDecidableEqContext : DecidableEq Context

Equations

• W3C.instDecidableEqContext = W3C.decEqContext✝

structure W3C.CredentialType : Type

Credential or presentation type

• value : String

instance W3C.instReprCredentialType : Repr CredentialType

Equations

• W3C.instReprCredentialType = { reprPrec := W3C.reprCredentialType✝ }

instance W3C.instDecidableEqCredentialType : DecidableEq CredentialType

Equations

• W3C.instDecidableEqCredentialType = W3C.decEqCredentialType✝

3. Temporal Properties

Credentials have temporal validity constraints.

structure W3C.DateTime : Type

XML datetime string (ISO 8601)

• value : String

instance W3C.instReprDateTime : Repr DateTime

Equations

• W3C.instReprDateTime = { reprPrec := W3C.reprDateTime✝ }

instance W3C.instDecidableEqDateTime : DecidableEq DateTime

Equations

• W3C.instDecidableEqDateTime = W3C.decEqDateTime✝

DateTime Parsing and Comparison

ISO 8601 datetime parsing and comparison functions. Supports simplified format: YYYY-MM-DDTHH:MM:SSZ

structure W3C.DateTimeComponents : Type

Parsed datetime components

• year : ℕ
• month : ℕ
• day : ℕ
• hour : ℕ
• minute : ℕ
• second : ℕ

instance W3C.instReprDateTimeComponents : Repr DateTimeComponents

Equations

• W3C.instReprDateTimeComponents = { reprPrec := W3C.reprDateTimeComponents✝ }

instance W3C.instDecidableEqDateTimeComponents : DecidableEq DateTimeComponents

Equations

• W3C.instDecidableEqDateTimeComponents = W3C.decEqDateTimeComponents✝

def W3C.parseNat (s : String) : Option ℕ

Parse a string to natural number

Equations

• W3C.parseNat s = String.foldl (fun (acc : Option ℕ) (c : Char) => acc.bind fun (n : ℕ) => if '0' ≤ c ∧ c ≤ '9' then some (n * 10 + (c.toNat - '0'.toNat)) else none) (some 0) s

def W3C.parseDateTime (dt : DateTime) : Option DateTimeComponents

Parse ISO 8601 datetime string (simplified format: YYYY-MM-DDTHH:MM:SSZ)

Equations

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

def W3C.dateTimeToSeconds (dtc : DateTimeComponents) : ℕ

Convert datetime components to comparable value (seconds since epoch approximation)

Equations

• W3C.dateTimeToSeconds dtc = (dtc.year * 365 + dtc.month * 31 + dtc.day) * 86400 + (dtc.hour * 3600 + dtc.minute * 60 + dtc.second)

def W3C.dateTimeBefore (dt1 dt2 : DateTime) : Bool

Compare two DateTimes (returns true if dt1 < dt2)

Equations

• W3C.dateTimeBefore dt1 dt2 = match W3C.parseDateTime dt1, W3C.parseDateTime dt2 with | some c1, some c2 => decide (W3C.dateTimeToSeconds c1 < W3C.dateTimeToSeconds c2) | x, x_1 => false

def W3C.dateTimeAfter (dt1 dt2 : DateTime) : Bool

Compare two DateTimes (returns true if dt1 > dt2)

Equations

• W3C.dateTimeAfter dt1 dt2 = match W3C.parseDateTime dt1, W3C.parseDateTime dt2 with | some c1, some c2 => decide (W3C.dateTimeToSeconds c1 > W3C.dateTimeToSeconds c2) | x, x_1 => false

def W3C.dateTimeBeforeOrEqual (dt1 dt2 : DateTime) : Bool

Compare two DateTimes (returns true if dt1 ≤ dt2)

Equations

• W3C.dateTimeBeforeOrEqual dt1 dt2 = match W3C.parseDateTime dt1, W3C.parseDateTime dt2 with | some c1, some c2 => decide (W3C.dateTimeToSeconds c1 ≤ W3C.dateTimeToSeconds c2) | x, x_1 => false

def W3C.dateTimeAfterOrEqual (dt1 dt2 : DateTime) : Bool

Compare two DateTimes (returns true if dt1 ≥ dt2)

Equations

• W3C.dateTimeAfterOrEqual dt1 dt2 = match W3C.parseDateTime dt1, W3C.parseDateTime dt2 with | some c1, some c2 => decide (W3C.dateTimeToSeconds c1 ≥ W3C.dateTimeToSeconds c2) | x, x_1 => false

4. Issuer

The issuer can be a URI or an object with additional properties.

inductive W3C.Issuer : Type

Issuer representation

• uri : String → Issuer
• object : String → List (String × DIDValue) → Issuer

instance W3C.instReprIssuer : Repr Issuer

Equations

• W3C.instReprIssuer = { reprPrec := W3C.reprIssuer✝ }

def W3C.Issuer.getId (issuer : Issuer) : String

Extract issuer ID from Issuer

Equations

• (W3C.Issuer.uri a).getId = a
• (W3C.Issuer.object a a_1).getId = a

5. Credential Subject

The subject of the credential (entity about which claims are made).

structure W3C.CredentialSubject : Type

Credential subject with optional id and claims

• id : Option String

  OPTIONAL: Identifier of the subject (often a DID)

• claims : List (String × DIDValue)

  REQUIRED: Claims about the subject (at least one)

instance W3C.instReprCredentialSubject : Repr CredentialSubject

Equations

• W3C.instReprCredentialSubject = { reprPrec := W3C.reprCredentialSubject✝ }

6. Credential Status

Information about the credential's revocation or suspension status.

structure W3C.CredentialStatus : Type

Credential status entry

• id : String

  REQUIRED: URI identifying the status information

• type_ : String

  REQUIRED: Status mechanism type

• additionalProperties : List (String × DIDValue)

  Additional status-specific properties

instance W3C.instReprCredentialStatus : Repr CredentialStatus

Equations

• W3C.instReprCredentialStatus = { reprPrec := W3C.reprCredentialStatus✝ }

7. Credential Schema

Reference to a schema for validating credential structure.

structure W3C.CredentialSchema : Type

Credential schema reference

• id : String

  REQUIRED: URI identifying the schema

• type_ : String

  REQUIRED: Schema type

• additionalProperties : List (String × DIDValue)

  Additional schema-specific properties

instance W3C.instReprCredentialSchema : Repr CredentialSchema

Equations

• W3C.instReprCredentialSchema = { reprPrec := W3C.reprCredentialSchema✝ }

8. Evidence

Supporting evidence for the claims in a credential.

structure W3C.Evidence : Type

Evidence entry

• id : Option String

  OPTIONAL: Identifier for the evidence

• type_ : List String

  REQUIRED: Type of evidence

• additionalProperties : List (String × DIDValue)

  Additional evidence-specific properties

instance W3C.instReprEvidence : Repr Evidence

Equations

• W3C.instReprEvidence = { reprPrec := W3C.reprEvidence✝ }

9. Terms of Use

Defines terms under which the credential can be used.

structure W3C.TermsOfUse : Type

Terms of use entry

• id : Option String

  OPTIONAL: Identifier for the terms

• type_ : String

  REQUIRED: Type of terms

• additionalProperties : List (String × DIDValue)

  Additional terms-specific properties

instance W3C.instReprTermsOfUse : Repr TermsOfUse

Equations

• W3C.instReprTermsOfUse = { reprPrec := W3C.reprTermsOfUse✝ }

10. Refresh Service

Mechanism for refreshing the credential.

structure W3C.RefreshService : Type

Refresh service entry

• id : String

  REQUIRED: URI of the refresh service

• type_ : String

  REQUIRED: Service type

• additionalProperties : List (String × DIDValue)

  Additional service-specific properties

instance W3C.instReprRefreshService : Repr RefreshService

Equations

• W3C.instReprRefreshService = { reprPrec := W3C.reprRefreshService✝ }

11. Proof

Cryptographic proof that makes credentials and presentations verifiable.

inductive W3C.ProofPurpose : Type

Proof purpose (why the proof was created)

• authentication : ProofPurpose
• assertionMethod : ProofPurpose
• keyAgreement : ProofPurpose
• capabilityInvocation : ProofPurpose
• capabilityDelegation : ProofPurpose

instance W3C.instReprProofPurpose : Repr ProofPurpose

Equations

• W3C.instReprProofPurpose = { reprPrec := W3C.reprProofPurpose✝ }

instance W3C.instDecidableEqProofPurpose : DecidableEq ProofPurpose

Equations

• W3C.instDecidableEqProofPurpose x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

structure W3C.Proof : Type

Cryptographic proof (embedded or enveloping)

• type_ : String

  REQUIRED: Proof type

• cryptosuite : Option String

  OPTIONAL: Cryptosuite identifier

• created : Option DateTime

  OPTIONAL: Timestamp of proof creation

• verificationMethod : Option String

  OPTIONAL: Verification method URI

• proofPurpose : Option String

  OPTIONAL: Purpose of the proof

• proofValue : Option String

  OPTIONAL: The cryptographic proof value

• challenge : Option String

  OPTIONAL: Challenge for preventing replay attacks

• domain : Option String

  OPTIONAL: Domain for binding to specific verifier

• additionalProperties : List (String × DIDValue)

  Additional proof-specific properties

instance W3C.instReprProof : Repr Proof

Equations

• W3C.instReprProof = { reprPrec := W3C.reprProof✝ }

12. Credential

A credential is a set of claims made by an issuer about a subject. This is the base structure before securing with proof.

structure W3C.Credential : Type

Credential (before securing with proof)

• context : List Context

  REQUIRED: JSON-LD context (first must be v2 context)

• type_ : List CredentialType

  REQUIRED: Credential type (must include "VerifiableCredential")

• id : Option String

  OPTIONAL: Credential identifier

• name : Option String

  OPTIONAL: Human-readable name

• description : Option String

  OPTIONAL: Human-readable description

• issuer : Issuer

  REQUIRED: Issuer of the credential

• validFrom : Option DateTime

  OPTIONAL: When credential becomes valid

• validUntil : Option DateTime

  OPTIONAL: When credential expires

• credentialSubject : List CredentialSubject

  REQUIRED: Subject(s) of the credential

• credentialStatus : Option CredentialStatus

  OPTIONAL: Status information

• credentialSchema : Option CredentialSchema

  OPTIONAL: Schema reference

• evidence : List Evidence

  OPTIONAL: Supporting evidence

• termsOfUse : List TermsOfUse

  OPTIONAL: Terms of use

• refreshService : Option RefreshService

  OPTIONAL: Refresh service

• additionalProperties : List (String × DIDValue)

  Additional properties (extensibility)

instance W3C.instReprCredential : Repr Credential

Equations

• W3C.instReprCredential = { reprPrec := W3C.reprCredential✝ }

13. Credential with Proof

A credential with proofs attached, but not yet verified. This is an intermediate structure before verification.

structure W3C.CredentialWithProof : Type

Credential with attached proofs (not yet verified)

• credential : Credential

  The underlying credential

• proof : List Proof

  REQUIRED: One or more proofs

instance W3C.instReprCredentialWithProof : Repr CredentialWithProof

Equations

• W3C.instReprCredentialWithProof = { reprPrec := W3C.reprCredentialWithProof✝ }

14. Valid and Invalid Verifiable Credentials

structure W3C.ValidVC : Type

Valid Verifiable Credential

A credential whose cryptographic proof has been successfully verified. The issuer's signature is valid and the credential has not been tampered with.

Abstraction:

• Does not expose cryptographic details (Ed25519, BBS+, etc.)
• Protocol-level abstraction: "cryptographically valid credential"
• Construction implies successful verification

• credentialWithProof : CredentialWithProof

  The credential with verified proof

instance W3C.instReprValidVC : Repr ValidVC

Equations

• W3C.instReprValidVC = { reprPrec := W3C.reprValidVC✝ }

structure W3C.InvalidVC : Type

Invalid Verifiable Credential

A credential whose cryptographic proof verification has failed. Reasons include:

• Signature verification failure
• Tampered credential content
• Invalid issuer key
• Malformed proof

• credentialWithProof : CredentialWithProof

  The credential with invalid proof

• reason : Option String

  OPTIONAL: Reason for invalidity (for debugging)

instance W3C.instReprInvalidVC : Repr InvalidVC

Equations

• W3C.instReprInvalidVC = { reprPrec := W3C.reprInvalidVC✝ }

inductive W3C.VerifiableCredential : Type

Verifiable Credential

Sum type of valid and invalid credentials. Represents the result of cryptographic verification.

Design Pattern:

• valid: Proof verification succeeded
• invalid: Proof verification failed
• Verification function is a simple pattern match
• Enables formal verification of protocol properties

• valid : ValidVC → VerifiableCredential
• invalid : InvalidVC → VerifiableCredential

instance W3C.instReprVerifiableCredential : Repr VerifiableCredential

Equations

• W3C.instReprVerifiableCredential = { reprPrec := W3C.reprVerifiableCredential✝ }

def W3C.VerifiableCredential.getCredentialWithProof : VerifiableCredential → CredentialWithProof

Get the underlying credential with proof

Equations

• (W3C.VerifiableCredential.valid a).getCredentialWithProof = a.credentialWithProof
• (W3C.VerifiableCredential.invalid a).getCredentialWithProof = a.credentialWithProof

def W3C.VerifiableCredential.getCredential (vc : VerifiableCredential) : Credential

Get the underlying credential (without proof)

Equations

• vc.getCredential = vc.getCredentialWithProof.credential

def W3C.VerifiableCredential.getIssuer (vc : VerifiableCredential) : Issuer

Get the issuer of the credential

Equations

• vc.getIssuer = vc.getCredential.issuer

def W3C.VerifiableCredential.getIssuerId (vc : VerifiableCredential) : String

Get the issuer ID

Equations

• vc.getIssuerId = vc.getIssuer.getId

def W3C.VerifiableCredential.getSubjects (vc : VerifiableCredential) : List CredentialSubject

Get the subjects of the credential

Equations

• vc.getSubjects = vc.getCredential.credentialSubject

def W3C.VerifiableCredential.verifySignature : VerifiableCredential → Bool

Verify cryptographic signature

Design Core:

• valid: Always returns true (proof already verified at construction)
• invalid: Always returns false (proof verification failed)

This simple definition enables formal reasoning about verification without exposing cryptographic implementation details.

Equations

• (W3C.VerifiableCredential.valid a).verifySignature = true
• (W3C.VerifiableCredential.invalid a).verifySignature = false

def W3C.VerifiableCredential.isValid (vc : VerifiableCredential) : Prop

Check if a verifiable credential is valid

Equations

• vc.isValid = (vc.verifySignature = true)

def W3C.VerifiableCredential.hasExpired (vc : VerifiableCredential) (now : DateTime) : Prop

Check if a verifiable credential has expired

Equations

• vc.hasExpired now = match vc.getCredential.validUntil with | none => False | some validUntil => W3C.dateTimeAfter now validUntil = true

def W3C.VerifiableCredential.notYetValid (vc : VerifiableCredential) (now : DateTime) : Prop

Check if a verifiable credential is not yet valid

Equations

• vc.notYetValid now = match vc.getCredential.validFrom with | none => False | some validFrom => W3C.dateTimeBefore now validFrom = true

15. Holder

Entity that possesses and presents credentials.

inductive W3C.Holder : Type

Holder representation (similar to Issuer)

• uri : String → Holder
• object : String → List (String × DIDValue) → Holder

instance W3C.instReprHolder : Repr Holder

Equations

• W3C.instReprHolder = { reprPrec := W3C.reprHolder✝ }

def W3C.Holder.getId (holder : Holder) : String

Extract holder ID from Holder

Equations

• (W3C.Holder.uri a).getId = a
• (W3C.Holder.object a a_1).getId = a

16. Presentation

A presentation is data derived from credentials for a specific verifier.

structure W3C.Presentation : Type

Presentation (before securing with proof)

• context : List Context

  REQUIRED: JSON-LD context

• type_ : List CredentialType

  REQUIRED: Presentation type (must include "VerifiablePresentation")

• id : Option String

  OPTIONAL: Presentation identifier

• holder : Option Holder

  OPTIONAL: Holder of the credentials

• verifiableCredential : List VerifiableCredential

  OPTIONAL: Verifiable credentials being presented

• additionalProperties : List (String × DIDValue)

  Additional properties (extensibility)

instance W3C.instReprPresentation : Repr Presentation

Equations

• W3C.instReprPresentation = { reprPrec := W3C.reprPresentation✝ }

17. Presentation with Proof

A presentation with proofs attached, but not yet verified.

structure W3C.PresentationWithProof : Type

Presentation with attached proofs (not yet verified)

• presentation : Presentation

  The underlying presentation

• proof : List Proof

  REQUIRED: One or more proofs

instance W3C.instReprPresentationWithProof : Repr PresentationWithProof

Equations

• W3C.instReprPresentationWithProof = { reprPrec := W3C.reprPresentationWithProof✝ }

18. Valid and Invalid Verifiable Presentations

structure W3C.ValidVP : Type

Valid Verifiable Presentation

A presentation whose cryptographic proof has been successfully verified. The holder's signature is valid and the presentation has not been tampered with.

• presentationWithProof : PresentationWithProof

  The presentation with verified proof

instance W3C.instReprValidVP : Repr ValidVP

Equations

• W3C.instReprValidVP = { reprPrec := W3C.reprValidVP✝ }

structure W3C.InvalidVP : Type

Invalid Verifiable Presentation

A presentation whose cryptographic proof verification has failed.

• presentationWithProof : PresentationWithProof

  The presentation with invalid proof

• reason : Option String

  OPTIONAL: Reason for invalidity (for debugging)

instance W3C.instReprInvalidVP : Repr InvalidVP

Equations

• W3C.instReprInvalidVP = { reprPrec := W3C.reprInvalidVP✝ }

inductive W3C.VerifiablePresentation : Type

Verifiable Presentation

Sum type of valid and invalid presentations. Same design pattern as VerifiableCredential.

• valid : ValidVP → VerifiablePresentation
• invalid : InvalidVP → VerifiablePresentation

instance W3C.instReprVerifiablePresentation : Repr VerifiablePresentation

Equations

• W3C.instReprVerifiablePresentation = { reprPrec := W3C.reprVerifiablePresentation✝ }

def W3C.VerifiablePresentation.getPresentationWithProof : VerifiablePresentation → PresentationWithProof

Get the underlying presentation with proof

Equations

• (W3C.VerifiablePresentation.valid a).getPresentationWithProof = a.presentationWithProof
• (W3C.VerifiablePresentation.invalid a).getPresentationWithProof = a.presentationWithProof

def W3C.VerifiablePresentation.getPresentation (vp : VerifiablePresentation) : Presentation

Get the underlying presentation (without proof)

Equations

• vp.getPresentation = vp.getPresentationWithProof.presentation

def W3C.VerifiablePresentation.getHolder (vp : VerifiablePresentation) : Option Holder

Get the holder of the presentation

Equations

• vp.getHolder = vp.getPresentation.holder

def W3C.VerifiablePresentation.getCredentials (vp : VerifiablePresentation) : List VerifiableCredential

Get the credentials in the presentation

Equations

• vp.getCredentials = vp.getPresentation.verifiableCredential

def W3C.VerifiablePresentation.verifySignature : VerifiablePresentation → Bool

Verify cryptographic signature

Equations

• (W3C.VerifiablePresentation.valid a).verifySignature = true
• (W3C.VerifiablePresentation.invalid a).verifySignature = false

def W3C.VerifiablePresentation.isValid (vp : VerifiablePresentation) : Prop

Check if a verifiable presentation is valid

Equations

• vp.isValid = (vp.verifySignature = true)

19. Constants

W3C defined constants.

def W3C.requiredContextV2 : String

The required v2 context URI

Equations

• W3C.requiredContextV2 = "https://www.w3.org/ns/credentials/v2"

def W3C.requiredCredentialType : String

The required credential type

Equations

• W3C.requiredCredentialType = "VerifiableCredential"

def W3C.requiredPresentationType : String

The required presentation type

Equations

• W3C.requiredPresentationType = "VerifiablePresentation"

20. Structural Validation Predicates

Validation checks that don't depend on cryptography.

def W3C.hasValidContext (contexts : List Context) : Prop

Check if context list has the required v2 context as first element

Equations

• W3C.hasValidContext [] = False
• W3C.hasValidContext (ctx :: tail) = (ctx.value = W3C.requiredContextV2)

def W3C.hasRequiredType (types : List CredentialType) (requiredType : String) : Prop

Check if type list includes required type

Equations

• W3C.hasRequiredType types requiredType = ∃ (t : W3C.CredentialType), t ∈ types ∧ t.value = requiredType

def W3C.hasAtLeastOneClaim (subject : CredentialSubject) : Prop

Check if credential subject has at least one claim

Equations

• W3C.hasAtLeastOneClaim subject = (subject.claims.length > 0)

def W3C.allSubjectsHaveClaims (subjects : List CredentialSubject) : Prop

All credential subjects must have at least one claim

Equations

• W3C.allSubjectsHaveClaims subjects = (subjects.length > 0 ∧ ∀ (s : W3C.CredentialSubject), s ∈ subjects → W3C.hasAtLeastOneClaim s)

def W3C.hasValidCredentialStatus (status : Option CredentialStatus) : Prop

Credential status must have id and type if present

Equations

• W3C.hasValidCredentialStatus none = True
• W3C.hasValidCredentialStatus (some s) = (s.id.length > 0 ∧ s.type_.length > 0)

def W3C.hasValidCredentialSchema (schema : Option CredentialSchema) : Prop

Credential schema must have id and type if present

Equations

• W3C.hasValidCredentialSchema none = True
• W3C.hasValidCredentialSchema (some s) = (s.id.length > 0 ∧ s.type_.length > 0)

def W3C.isStructurallyValidCredential (cred : Credential) : Prop

A credential is structurally valid if it satisfies all MUST requirements

Equations

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

def W3C.hasProofs (cwp : CredentialWithProof) : Prop

A credential with proof must have at least one proof

Equations

• W3C.hasProofs cwp = (cwp.proof.length > 0)

def W3C.isStructurallyValidPresentation (pres : Presentation) : Prop

A presentation is structurally valid if it satisfies all MUST requirements

Equations

• W3C.isStructurallyValidPresentation pres = (W3C.hasValidContext pres.context ∧ W3C.hasRequiredType pres.type_ W3C.requiredPresentationType)

def W3C.hasPresentationProofs (pwp : PresentationWithProof) : Prop

A presentation with proof must have at least one proof

Equations

• W3C.hasPresentationProofs pwp = (pwp.proof.length > 0)

21. Complete Validation and Verification

Combines structural validation with cryptographic verification.

def W3C.isValidCredential (vc : VerifiableCredential) : Prop

Complete validation of a verifiable credential

Equations

• W3C.isValidCredential vc = (W3C.isStructurallyValidCredential vc.getCredential ∧ W3C.hasProofs vc.getCredentialWithProof ∧ vc.isValid)

def W3C.isValidPresentation (vp : VerifiablePresentation) : Prop

Complete validation of a verifiable presentation

Equations

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

22. Temporal Validity

Check if credentials are within their validity period.

structure W3C.VerificationTime : Type

Abstract notion of current time (to be provided by verification context)

• now : DateTime

instance W3C.instReprVerificationTime : Repr VerificationTime

Equations

• W3C.instReprVerificationTime = { reprPrec := W3C.reprVerificationTime✝ }

def W3C.isTemporallyValid (vc : VerifiableCredential) (time : VerificationTime) : Prop

Check if a credential is temporally valid at a given time

Equations

• W3C.isTemporallyValid vc time = (¬vc.hasExpired time.now ∧ ¬vc.notYetValid time.now)

23. Security Properties

def W3C.issuerBinding (vc : VerifiableCredential) : Prop

Issuer Binding: A valid credential is cryptographically bound to its issuer

Equations

• W3C.issuerBinding vc = (vc.isValid → ∃ (issuer : W3C.Issuer), issuer = vc.getIssuer)

def W3C.holderBinding (vp : VerifiablePresentation) : Prop

Holder Binding: A valid presentation is cryptographically bound to its holder

Equations

• W3C.holderBinding vp = (vp.isValid → vp.getHolder ≠ none)

def W3C.nonRepudiation (vc : VerifiableCredential) : Prop

Non-Repudiation: An issuer cannot deny issuing a valid credential

Equations

• W3C.nonRepudiation vc = (vc.isValid → W3C.issuerBinding vc)

def W3C.credentialIntegrity (vc : VerifiableCredential) : Prop

Credential Integrity: Valid credentials maintain their integrity

Equations

• W3C.credentialIntegrity vc = (W3C.isValidCredential vc → W3C.issuerBinding vc)

def W3C.presentationIntegrity (vp : VerifiablePresentation) : Prop

Presentation Integrity: Valid presentations maintain their integrity

Equations

• W3C.presentationIntegrity vp = (W3C.isValidPresentation vp → ∀ (vc : W3C.VerifiableCredential), vc ∈ vp.getCredentials → W3C.credentialIntegrity vc)

24. Privacy Properties

Formal privacy properties for credentials and presentations.

def W3C.supportsSelectiveDisclosure (vc : VerifiableCredential) : Prop

Selective Disclosure: Ability to reveal only specific claims

Equations

• W3C.supportsSelectiveDisclosure vc = ∃ (proof : W3C.Proof), proof ∈ vc.getCredentialWithProof.proof ∧ (proof.cryptosuite = some "bbs-2023" ∨ proof.type_ = "DataIntegrityProof")

def W3C.supportsUnlinkability (vc : VerifiableCredential) : Prop

Unlinkability: Credentials should not be trivially linkable across uses

Equations

• W3C.supportsUnlinkability vc = W3C.supportsSelectiveDisclosure vc

25. DateTime Comparison Properties

theorem W3C.dateTime_refl (dt : DateTime) : parseDateTime dt ≠ none → dateTimeBeforeOrEqual dt dt = true

DateTime comparison is reflexive for valid datetimes

theorem W3C.dateTime_before_after (dt1 dt2 : DateTime) : dateTimeBefore dt1 dt2 = true → dateTimeAfter dt2 dt1 = true

If dt1 is before dt2, then dt2 is after dt1

theorem W3C.dateTime_trans (dt1 dt2 dt3 : DateTime) : dateTimeBefore dt1 dt2 = true → dateTimeBefore dt2 dt3 = true → dateTimeBefore dt1 dt3 = true

Transitivity of dateTimeBefore

26. Core Theorems

theorem W3C.valid_vc_passes_verification (vvc : ValidVC) : (VerifiableCredential.valid vvc).isValid

Valid credentials always pass signature verification

theorem W3C.invalid_vc_fails_verification (ivc : InvalidVC) : ¬(VerifiableCredential.invalid ivc).isValid

Invalid credentials always fail signature verification

theorem W3C.valid_vp_passes_verification (vvp : ValidVP) : (VerifiablePresentation.valid vvp).isValid

Valid presentations always pass signature verification

theorem W3C.invalid_vp_fails_verification (ivp : InvalidVP) : ¬(VerifiablePresentation.invalid ivp).isValid

Invalid presentations always fail signature verification

theorem W3C.valid_vc_has_issuer_binding (vc : VerifiableCredential) : vc.isValid → issuerBinding vc

Valid credentials satisfy issuer binding

theorem W3C.valid_vp_has_holder_binding (vp : VerifiablePresentation) : vp.isValid → vp.getHolder ≠ none → holderBinding vp

Valid presentations satisfy holder binding (if holder present)

26. Example Credentials and Presentations

def W3C.exampleContext : Context

Example context

Equations

• W3C.exampleContext = { value := W3C.requiredContextV2 }

def W3C.exampleCredentialType : CredentialType

Example credential type

Equations

• W3C.exampleCredentialType = { value := W3C.requiredCredentialType }

def W3C.exampleSubject : CredentialSubject

Example credential subject

Equations

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

def W3C.exampleProof : Proof

Example proof

Equations

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

def W3C.exampleCredential : Credential

Example credential

Equations

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

def W3C.exampleCredentialWithProof : CredentialWithProof

Example credential with proof

Equations

• W3C.exampleCredentialWithProof = { credential := W3C.exampleCredential, proof := [W3C.exampleProof] }

def W3C.exampleValidVC : ValidVC

Example valid verifiable credential

Equations

• W3C.exampleValidVC = { credentialWithProof := W3C.exampleCredentialWithProof }

def W3C.exampleVerifiableCredential : VerifiableCredential

Example verifiable credential

Equations

• W3C.exampleVerifiableCredential = W3C.VerifiableCredential.valid W3C.exampleValidVC

def W3C.examplePresentation : Presentation

Example presentation

Equations

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

def W3C.examplePresentationWithProof : PresentationWithProof

Example presentation with proof

Equations

• W3C.examplePresentationWithProof = { presentation := W3C.examplePresentation, proof := [W3C.exampleProof] }

def W3C.exampleValidVP : ValidVP

Example valid verifiable presentation

Equations

• W3C.exampleValidVP = { presentationWithProof := W3C.examplePresentationWithProof }

def W3C.exampleVerifiablePresentation : VerifiablePresentation

Example verifiable presentation

Equations

• W3C.exampleVerifiablePresentation = W3C.VerifiablePresentation.valid W3C.exampleValidVP

27. DateTime Comparison Examples

These examples demonstrate the DateTime parsing and comparison functions.

def W3C.dt1 : DateTime

Example DateTime values

Equations

• W3C.dt1 = { value := "2023-01-01T00:00:00Z" }

def W3C.dt2 : DateTime

Equations

• W3C.dt2 = { value := "2023-06-15T12:30:45Z" }

def W3C.dt3 : DateTime

Equations

• W3C.dt3 = { value := "2024-01-01T00:00:00Z" }

def W3C.dtInvalid : DateTime

Equations

• W3C.dtInvalid = { value := "invalid" }

def W3C.testCredentialWithDates : Credential

Test credential with validFrom and validUntil

Equations

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

def W3C.testCredentialWithProof : CredentialWithProof

Equations

• W3C.testCredentialWithProof = { credential := W3C.testCredentialWithDates, proof := [W3C.exampleProof] }

def W3C.testValidVC : ValidVC

Equations

• W3C.testValidVC = { credentialWithProof := W3C.testCredentialWithProof }

def W3C.testVerifiableCredential : VerifiableCredential

Equations

• W3C.testVerifiableCredential = W3C.VerifiableCredential.valid W3C.testValidVC

def W3C.dateTimeComparisonTests : List (String × Bool)

Test cases for DateTime comparison

Equations

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

def W3C.dateTimeParseTests : List (String × Bool)

Test cases for DateTime parsing

Equations

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