Version 1 is an explicit two-key profile. Version 0 and its hash input remain unchanged. This adds no directory or endpoint requirement. The public information pair is [1, {signingKey, agreementKey}]. No Ed25519-to-X25519 conversion is assumed.

structure AMT.DIDComm.Input : Type

• version : ℕ
• signingKey : PublicKey
• agreementKey : PublicKey

instance AMT.DIDComm.instReprInput : Repr Input

Equations

• AMT.DIDComm.instReprInput = { reprPrec := AMT.DIDComm.reprInput✝ }

def AMT.DIDComm.base64url (bytes : List UInt8) : String

Equations

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

def AMT.DIDComm.template (input : Input) : String

JCS of fixed Version 1 template; only public keys vary.

Equations

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

def AMT.DIDComm.keyId (did : W3C.DID) (fragment : String) : W3C.DIDURL

Equations

• AMT.DIDComm.keyId did fragment = { did := did, fragment := some fragment }

def AMT.DIDComm.method (did : W3C.DID) (fragment curve : String) (key : PublicKey) : W3C.VerificationMethod

Equations

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

def AMT.DIDComm.finalize (input : Input) (did : W3C.DID) : W3C.DIDDocument

Equations

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

def AMT.DIDComm.methodMatches (vm : W3C.VerificationMethod) (did : W3C.DID) (fragment curve : String) (key : PublicKey) : Bool

Canonical W3C model ordering; JSON parser normalizes object member order and checks the two exact context entries, duplicates, sizes and unknown fields.

Equations

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

def AMT.DIDComm.referenceMatches (rels : List W3C.VerificationRelationship) (id : W3C.DIDURL) : Bool

Equations

• AMT.DIDComm.referenceMatches [W3C.VerificationRelationship.reference r] id = (r == id)
• AMT.DIDComm.referenceMatches rels id = false

def AMT.DIDComm.documentMatches (doc : W3C.DIDDocument) (input : Input) (did : W3C.DID) : Bool

Equations

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

def AMT.DIDComm.derive (sha3512 : List UInt8 → Hash) (input : Input) : Option W3C.DID

Equations

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

structure AMT.DIDComm.Peer : Type

• input : Input
• did : W3C.DID
• document : W3C.DIDDocument

def AMT.DIDComm.verifyPeer (sha3512 : List UInt8 → Hash) (peer : Peer) : Bool

Equations

• AMT.DIDComm.verifyPeer sha3512 peer = match AMT.DIDComm.derive sha3512 peer.input with | none => false | some did => peer.did == did && AMT.DIDComm.documentMatches peer.document peer.input did

def AMT.DIDComm.selectAgreementKeys (sha3512 : List UInt8 → Hash) (sender recipient : Peer) (senderKid recipientKid : W3C.DIDURL) : Option (PublicKey × PublicKey)

Authcrypt key selection. Agreement keys come exclusively from the locally reconstructed keyAgreement relationship; never substitute the signing key.

Equations

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

def AMT.DIDComm.encrypt (sha3512 : List UInt8 → Hash) (sender recipient : Peer) (senderKid recipientKid : W3C.DIDURL) (plaintext : List UInt8) (budget : ResourceBudget) (pack : Peer → Peer → W3C.DIDURL → W3C.DIDURL → List UInt8 → Option (List UInt8)) : Option (List UInt8)

Backend implements DIDComm authcrypt, validates X25519 keys (including all-zero shared-secret rejection), binds protected headers and authenticated from/to, and checks that its private-key handle matches the selected local agreement key.

Equations

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

def AMT.DIDComm.decrypt (sha3512 : List UInt8 → Hash) (sender recipient : Peer) (senderKid recipientKid : W3C.DIDURL) (ciphertext : List UInt8) (budget : ResourceBudget) (unpack : ResourceBudget → Peer → Peer → W3C.DIDURL → W3C.DIDURL → List UInt8 → Option (List UInt8)) : Option (List UInt8)

Unpack authenticates the protected skid/kid, from/to and context before return; its decompression/parser must enforce the budget during work, not only at the end.

Equations

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