W3C

– DRAFT –
A Lean4-Verified Protocol for Smart Cities Addressing the Three Core Challenges of DIDs and VCs

12 November 2025

Attendees

Present
Atsushi, Denken_Chen, denkeni, Hiromu_Ogawa, Itoe_Kinjo, jay_Kishigami, Junko_Kamata, Kai_Otsuki, Markus_Sabadello, Michael_Wilson, naomi, Ryo_Tsuyuki, Ryoya_Kawai, Takahiro_Aritaki, Takimi_Mouri, Toru_Mariuhashi, Will_Abramson
Regrets
-
Chair
Mitsuhide_Matsuda
Scribe
naomi

Meeting minutes

https://docs.google.com/presentation/d/1O2-I_6aJRaEog67Yl0UMTKm2Svx9JxcCKx7gVvLD9dM/edit?usp=sharing

[Mitsuhide talks about DID and VC overview]

Mitsuhide: both technolgies will consists to the future smart cities

[page 3]
… challenges remain unsolved in current implementations
… the first challenge is using blockchain or IPFS
… ID documents in others. Behavioral tracking
… typically, DID documents are stored
… 2nd challenge, selective disclosure of faces exposes a lot of personal information
… for example, selective disclosure mean that
… portion of their driver's license, do a bit wire
… 20 years old is a bar in Jpaan
… your exact age becomes known to the other party to verify
… some systems adopt batch issures as an operational workaround
… they issue hundreds of VCs for single soft kit
… ZKP will solve problem
… ZKP doesn't solve issues @1
… these 3 changes are common problems in Europe, India, Africa and Japan

[page 4]

Mitsuhide: I invented AMT protocol, it calls Amateras
… it secures personal information protection, not through operations
… it's a cryptographic story
… that combines @3
… using blockchain or IPFS. How does the verifier obrain the DID document?
… the empty pressure
… DID document by sending this information into a template
… the number on the public key
… by husing this DID document, according to prescirbed rules, the verifier can obrain a DID in the format DID called AMT
… fixing DID docment makes key notation impossible
… therefore, in the AMT protocol, single for the single holder @4
… and uses over 100 DIDS throw out their lifetime
… the relationship between DIDs and VCs can be proven with@5
… there's no impact on life cycle

[page 5]

Mitsuhide: we include ZKP, touch generated prompts. Anonymous hash identifier
… from each transaction and the national ID, My Number called in Japan
… if a government discoverd, they could be suspected all fraud
… they can start through the anonymous hash identifire and IDs
… for each event, anonimous hash identifires are assigned for taxation
… this generates different hosts

Denkeni: when you issue VC, it's possible to embed it the DID into the VC
… the ID, holder's date
… you can make sure when presenting the VCs
… it's presented by the exact holder

@4@: For ownership verification. If a signature is embedded in the Vc, the person presenting it can demonstrate ownership
… There is a DID entity, and we add a DID comment. The sub-DID comment cannot be proven without a link

Mitsuhide: probably the relationship between DID comm @6

@4@: one proof for connection between the original DID. and the safety ID that is used in the context
… signature to the verified credential shells, the link between the original DID

[page 15]

[page 16]

Mitsuhide: there's also a PDF blueprint, but most important is former code in the lean programming language
… Lean is a @10 proving
… AMT specific protocol implementation is about 2500 rules
… basic data model spec
… AMT claims @11
… you can have protocol codecs to explain the specs to you
… you can check results in github acitions
… verification is possilble using Lean and AI agents
… you may wonder if the innovative-looking AMT protocol
… AMT uses DID, VC, DIDComm and JSON scheme
… for JSON scheme, we established and formalized in Lean compared to subset, and JSON's subset

[page 19]

Mitsuhide: why I was able to solve this fundamental system?
… thru 14 years programming experience, I got worked for development of administrative system for Japanese government
… I started Lean this year
… I've succeeded and formalizing unknown valiational principle
… 6000 lines by next year
… is planning to announce about the Lean hypothesis

[page 20]

Mitsuhide: ZKP circuit ecosystem is partially under developed
… adopting quantum resistant cryptography,
… considering whether to write specs in Lean
… implement the code and output

[page 22]

Mitsuhide: we can achieve online election by incorporating secured computation
… it culculates and aggregates results
… while keeping them anonymous
… without the calling ZKP, AMT makes possilbe

[page 23]

Mitsuhide: AI in economic activities with its own will
… robots weiths highly developed emotions
… equivalent to human rights
… AMT protocol is technology that
… look forward to work

Markus_Sabadello: for auditing. the government will brute force. why can't the government just brute force everything?

Mitsuhide: about computational complexity
… in Japan 100 million people @15
… at the latest, it will be finised in 1 day
… Japan has 1700 local governments
… you don't have to target every citizens but I'm targetting local government at the first stage

Jay: Does the computational complexity depend on the number of bits?

Mitsuihide: the length hash depends on encryption methos you choose
… we might have to use PQC

Jay: loughly, how long hash are you considering to target for use?

Mitsuhide: from 68 to 128 bites with the current cryptography

[Mitsuhide is calculating]

[page 24]

@21@: you'd rather usee ZKP to prove the link
… what the Taiwan government is doing is rather the batch issuarance
… what you are trying to do here

@21@: you interact with the VC as the main DID to generate ZKP proof
… then you perform the VC verification
… interesting. That method exists, but EU uses a different approach
… instead of this method, they issue many VCs to create different attrivutes
… this prevents linking
… the Taiwaneese government uses badges
… pls share your thoughts on the design

Mitsuhide: if you think about the future, differnt issures, including AI agents for example issue credentials to humans or every industry
… we don't know how many issures are out there
… and also that requires a lot of infrastructure for every issure
… that might not work

Mitsushide: I am also considering use cases in conflict zones
… without network even
… we can create DID from locally saved VC
… thru bluethooth for example
… in case of earthquake or nature disaster
… the verification system can perform offline verification
… Earth's VC can be used on Mars too

@21@: I'm summarizing. there's another reason why he chooses proof system, rather than batch issurance
… like EU, this proof system works even offline
… if we need a batch issuance, if we have one credentials from the issuer at one moment
… and if we use all the credential we have
… we have to ask for the batch
… it may be interesting for you to check out Google Longfeller Library
… they oversell make the proof sytem proof that is smaller
… the proof generalization is easy
… but the verification needs more time
… the model works better
… Google's one has a similar idea
… they apply a similar method to you

@21@: Library for mdoc. Changing concept where heavy load is placed, light pipeline placed at creating proofs, and verification turnes into heavy.

Mitsuhide: personal cloud. what to d owith the private key
… I see, making the verifier heavier

Mitsuhide: AMT's verifier will also verify close friends and romantic partners. This means the verifier will be assigned to individuals
… I haven't checked how to implement ZKP. I should ask a trusted org which library to use

denkeni: Marcus has been asking questions about contributor to did resolution
… we have similar research on this
… but not as deep as you did

Mitsuhide: I'm currently developing by myself and I appreciate to hear the work outside of Japan

denkeni: I only knew My Number system in Japan but I'm glad to hear your activity

Mitsuhide: I want to AMT protocol to make it standardized one, and implement it to as government system

denkeni: standardization of the did method will help a lot for the governemnt ot adopt that
… we can continue the discussion there about your did methods application
… including security and privacy

Minutes manually created (not a transcript), formatted by scribe.perl version 248 (Mon Oct 27 20:04:16 2025 UTC).

Diagnostics

Succeeded: s/GKP/ZKP/

Succeeded: s/AMD protocol/AMT protocol/

Succeeded: s/AMD uses/AMT uses/

Succeeded: s/IDCOM/DIDComm/

Succeeded: s/@11/worked for development of administrative system for Japanese government/

Succeeded: s/limitation of hush/loughly, how long hash are you considering to target for use?/

Succeeded: s/hush/hash/

Succeeded: s/@20@/Markus_Sabadello/

Succeeded: s/Japan has 700 local governments/Japan has 1700 local governments/

Succeeded: s/three/there/

Succeeded: s/create ID/create DID from locally saved VC/

Succeeded: s/Creating proofs is easy. Verification is heavy./Changing concept where heavy load is placed, light pipeline placed at creating proofs, and verification turnes into heavy./

Succeeded: s/hit resolution/did resolution/

Succeeded: s/deep methods/did methods/

Succeeded: s/data method/did method/

No scribenick or scribe found. Guessed: naomi

Maybe present: @21@, @4@, Jay, Mitsuhide, Mitsuihide, Mitsushide

All speakers: @21@, @4@, Denkeni, Jay, Markus_Sabadello, Mitsuhide, Mitsuihide, Mitsushide

Active on IRC: breakout-bot, denkeni, naomi