06:38:57 <RRSAgent> RRSAgent has joined #did-vc-challenges
06:39:01 <RRSAgent> logging to https://www.w3.org/2025/11/12-did-vc-challenges-irc
06:39:01 <breakout-bot> RRSAgent, do not leave
06:39:02 <breakout-bot> RRSAgent, this meeting spans midnight
06:39:02 <breakout-bot> RRSAgent, make logs public
06:39:03 <breakout-bot> Meeting: A Lean4-Verified Protocol for Smart Cities Addressing the Three Core Challenges of DIDs and VCs
06:39:04 <breakout-bot> Chair: Mitsuhide Matsuda
06:39:04 <breakout-bot> Agenda: https://github.com/w3c/tpac2025-breakouts/issues/73
06:39:04 <Zakim> Zakim has joined #did-vc-challenges
06:39:04 <breakout-bot> Zakim, clear agenda
06:39:05 <Zakim> agenda cleared
06:39:06 <breakout-bot> Zakim, agenda+ Pick a scribe
06:39:06 <Zakim> agendum 1 added
06:39:06 <breakout-bot> Zakim, agenda+ Reminders: code of conduct, health policies, recorded session policy
06:39:07 <Zakim> agendum 2 added
06:39:08 <breakout-bot> Zakim, agenda+ Goal of this session
06:39:08 <Zakim> agendum 3 added
06:39:08 <breakout-bot> Zakim, agenda+ Discussion
06:39:09 <Zakim> agendum 4 added
06:39:09 <breakout-bot> Zakim, agenda+ Next steps / where discussion continues
06:39:09 <Zakim> agendum 5 added
06:39:09 <breakout-bot> Zakim, agenda+ Adjourn / Use IRC command: Zakim, end meeting
06:39:10 <Zakim> agendum 6 added
06:39:10 <breakout-bot> breakout-bot has left #did-vc-challenges
07:02:49 <tantek-projector> tantek-projector has joined #did-vc-challenges
07:06:15 <naomi> naomi has joined #did-vc-challenges
07:07:27 <naomi> chair: Mitsuhide_Matsuda
07:15:14 <naomi> https://docs.google.com/presentation/d/1O2-I_6aJRaEog67Yl0UMTKm2Svx9JxcCKx7gVvLD9dM/edit?usp=sharing
07:16:01 <naomi> [Mitsuhide talks about DID and VC overview]
07:16:18 <tmaruha4> tmaruha4 has joined #did-vc-challenges
07:16:56 <naomi> Mitsuhide: both technolgies will consists to the future smart cities
07:17:34 <naomi> [page 3]
07:17:41 <jkamata> jkamata has joined #did-vc-challenges
07:17:51 <naomi> ... challenges remain unsolved in current implementations
07:18:04 <naomi> ... the first challenge is using blockchain or IPFS
07:18:18 <naomi> ... ID documents in others. Behavioral tracking
07:18:28 <naomi> ... typically, DID documents are stored
07:18:53 <naomi> ... 2nd challenge, selective disclosure of faces exposes a lot of personal information
07:19:03 <naomi> ... for example, selective disclosure mean that
07:19:21 <naomi> .... portion of their driver's license, do a bit wire
07:20:05 <naomi> ... 20 years old is a bar in Jpaan
07:20:16 <naomi> ... your exact age becomes known to the other party to verify
07:20:29 <naomi> ... some systems adopt batch issures as an operational workaround
07:20:39 <naomi> ... they issue hundreds of VCs for single soft kit
07:21:01 <naomi> ... GKP will solve problem
07:21:26 <denkeni> denkeni has joined #did-vc-challenges
07:21:27 <naomi> s/GKP/ZKP/
07:21:55 <naomi> ... ZKP doesn't solve issues @1
07:22:11 <naomi> ... these 3 changes are common problems in Europe, India, Africa and Japan
07:22:29 <naomi> [page 4]
07:22:54 <naomi> Mitsuhide: I invented AMT protocol, it calls Amateras
07:23:09 <naomi> ... it secures personal information protection, not through operations
07:23:17 <naomi> ... it's a cryptographic story
07:23:22 <atsushi> atsushi has joined #did-vc-challenges
07:23:43 <naomi> ... that combines @3
07:24:01 <naomi> ... using blockchain or IPFS. How does the verifier obrain the DID document?
07:24:19 <naomi> ... the empty pressure
07:24:34 <naomi> ... DID document by sending this information into a template
07:24:47 <naomi> ... the number on the public key
07:25:16 <naomi> ... by husing this DID document, according to prescirbed rules, the verifier can obrain a DID in the format DID called AMT
07:25:25 <naomi> ... fixing DID docment makes key notation impossible
07:25:39 <naomi> ... therefore, in the AMT protocol, single for the single holder @4
07:25:51 <naomi> ... and uses over 100 DIDS throw out their lifetime
07:26:07 <naomi> ... the relationship between DIDs and VCs can be proven with@5
07:26:25 <naomi> ... there's no impact on life cycle
07:26:31 <naomi> [page 5]
07:27:01 <naomi> Mitsuhide: we include ZKP, touch generated prompts. Anonymous hash identifier
07:27:27 <naomi> ... from each transaction and the national ID, My Number called in Japan
07:27:52 <naomi> ... if a government discoverd, they could be suspected all fraud
07:28:17 <naomi> ... they can start through the anonymous hash identifire and IDs
07:28:41 <naomi> ... for each event, anonimous hash identifires are assigned for taxation
07:28:51 <naomi> ... this generates different hosts
07:29:52 <naomi> Denkeni: when you issue VC, it's possible to embed it the DID into the VC
07:29:59 <naomi> ... the ID, holder's date
07:30:05 <naomi> ... you can make sure when presenting the VCs
07:30:13 <naomi> ... it's presented by the exact holder
07:31:28 <naomi> @4@: For ownership verification. If a signature is embedded in the Vc, the person presenting it can demonstrate ownership
07:32:28 <naomi> ... There is a DID entity, and we add a DID comment. The sub-DID comment cannot be proven without a link
07:33:10 <naomi> Mitsuhide: probably the relationship between DID comm @6
07:33:37 <naomi> @4@: one proof for connection between the original DID. and the safety ID that is used in the context
07:33:53 <naomi> ... signature to the verified credential shells, the link between the original DID
07:34:35 <naomi> [page 15]
07:35:02 <naomi> [page 16]
07:35:30 <naomi> Mitsuhide: there's also a PDF blueprint, but most important is former code in the lean programming language
07:35:52 <naomi> ... Lean is a @10 proving
07:36:30 <naomi> ... AMT specific protocol implementation is about 2500 rules
07:36:46 <naomi> ... basic data model spec
07:37:22 <naomi> ... AMT claims @11
07:37:41 <naomi> ... you can have protocol codecs to explain the specs to you
07:37:52 <naomi> ... you can check results in github acitions
07:38:05 <naomi> ... verification is possilble using Lean and AI agents
07:38:25 <naomi> ... you may wonder if the innovative-looking AMD protocol
07:38:37 <naomi> ... AMD uses DID, VC, IDCOM and JSON scheme
07:38:40 <atsushi> s/AMD protocol/AMT protocol/
07:38:52 <atsushi> s/AMD uses/AMT uses/
07:39:01 <atsushi> s/IDCOM/DIDComm/
07:39:34 <naomi> ... for JSON scheme, we established and formalized in Lean compared to subset, and JSON's subset
07:39:48 <naomi> [page 19]
07:40:08 <naomi> Mitsuhide: why I was able to solve this fundamental system?
07:40:27 <naomi> ... thru 14 years programming experience, I got @11
07:40:34 <naomi> ... I started Lean this year
07:40:59 <naomi> ... I've succeeded and formalizing unknown valiational principle
07:41:12 <naomi> ... 6000 lines by next year
07:41:23 <naomi> ... is planning to announce about the Lean hypothesis
07:41:25 <atsushi> s/@11/worked for development of administrative system for Japanese government/
07:42:57 <naomi> [page 20]
07:43:16 <naomi> Mitsuhide: ZKP circuit ecosystem is partially under developed
07:43:32 <naomi> ... adopting quantum resistant cryptography,
07:43:40 <naomi> ... considering whether to write specs in Lean
07:43:51 <naomi> ... implement the code and output
07:44:08 <naomi> [page 22]
07:44:21 <naomi> Mitsuhide: we can achieve online election by incorporating secured computation
07:44:36 <naomi> ... it culculates and aggregates results
07:44:41 <naomi> ... while keeping them anonymous
07:44:54 <naomi> ... without the calling ZKP, AMT makes possilbe
07:45:04 <naomi> [page 23]
07:45:25 <naomi> Mitsuhide: AI in economic activities with its own will
07:45:34 <naomi> ... robots weiths highly developed emotions
07:45:41 <naomi> ... equivalent to human rights
07:45:48 <naomi> ... AMT protocol is technology that
07:46:23 <naomi> ... look forward to work
07:46:55 <naomi> @20@: for auditing. the government will brute force. why can't the government just brute force everything?
07:47:29 <naomi> Mitsuhide: about computational complexity
07:48:12 <naomi> ... in Japan 100 million people @15
07:48:22 <naomi> ... at the latest, it will be finised in 1 day
07:48:43 <naomi> ... Japan has 700 local governments
07:49:17 <naomi> ... you don't have to target every citizens but I'm targetting local government at the first stage
07:49:55 <naomi> Jay: Does the computational complexity depend on the number of bits?
07:50:15 <naomi> Mitsuihide: the length hush depends on encryption methos you choose
07:50:22 <naomi> ... we might have to use PQC
07:51:33 <naomi> Jay: limitation of hush
07:52:33 <atsushi> s/limitation of hush/loughly, how long hash are you considering to target for use?/
07:52:34 <naomi> Mitsuhide: from 68 to 128 bites with the current cryptography
07:53:03 <naomi> [Mitsuhide is calculating]
07:53:40 <naomi> s/hush/hash/
07:54:37 <naomi> s/@20@/Markus_Sabadello/
07:55:29 <naomi> [page 24]
07:56:15 <naomi> @21@: you'd rather usee ZKP to prove the link
07:56:34 <naomi> ... what the Taiwan government is doing is rather the batch issuarance
07:56:42 <jkamata> s/Japan has 700 local governments/Japan has 1700 local governments/
07:56:43 <naomi> ... what you are trying to do here
07:58:52 <naomi> @21@: you interact with the VC as the main DID to generate ZKP proof
07:59:00 <naomi> ... then you perform the VC verification
07:59:13 <naomi> ... interesting. That method exists, but EU uses a different approach
07:59:26 <naomi> ... instead of this method, they issue many VCs to create different attrivutes
07:59:30 <naomi> ... this prevents linking
07:59:39 <naomi> ... the Taiwaneese government uses badges
07:59:45 <naomi> ... pls share your thoughts on the design
08:00:10 <naomi> Mitsuhide: if you think about the future, differnt issures, including AI agents for example issue credentials to humans or every industry
08:00:22 <naomi> ... we don't know how many issures are out three
08:00:26 <naomi> s/three/there/
08:00:39 <naomi> ... and also that requires a lot of infrastructure for every issure
08:00:44 <naomi> ... that might not work
08:01:07 <naomi> Mitsushide: I am also considering use cases in conflict zones
08:01:15 <naomi> ... without network even
08:01:23 <naomi> ... we can create ID
08:01:36 <naomi> ... thru bluethooth for example
08:01:51 <atsushi> s/create ID/create DID from locally saved VC/
08:01:53 <naomi> ... in case of earthquake or nature disaster
08:02:22 <naomi> ... the verification system can perform offline verification
08:02:54 <naomi> ... Earth's VC can be used on Mars too
08:03:28 <naomi> @21@: I'm summarizing. there's another reason why he chooses proof system, rather than batch issurance
08:03:38 <naomi> ... like EU, this proof system works even offline
08:03:59 <naomi> ... if we need a batch issuance, if we have one credentials from the issuer at one moment
08:04:07 <naomi> ... and if we use all the credential we have
08:04:27 <naomi> ... we have to ask for the batch
08:05:05 <naomi> ... it may be interesting for you to check out Google Longfeller Library
08:05:18 <naomi> ... they oversell make the proof sytem proof that is smaller
08:05:29 <naomi> ... the proof generalization is easy
08:05:33 <naomi> ... but the verification needs more time
08:05:37 <naomi> ... the model works better
08:05:58 <naomi> ... Google's one has a similar idea
08:06:32 <naomi> ... they apply a similar method to you
08:06:41 <denkeni> present+
08:07:58 <naomi> @21@: Library for mdoc. Creating proofs is easy. Verification is heavy.
08:08:37 <naomi> Mitsuhide: personal cloud. what to d owith the private key
08:08:57 <naomi> ... I see, making the verifier heavier
08:09:37 <atsushi> 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./
08:09:55 <naomi> Mitsuhide: AMT's verifier will also verify close friends and romantic partners. This means the verifier will be assigned to individuals
08:10:55 <naomi> ... I haven't checked how to implement ZKP. I should ask a trusted org which library to use
08:11:48 <tmaruha4> tmaruha4 has joined #did-vc-challenges
08:12:36 <naomi> denkeni: Marcus has been asking questions about contributor to hit resolution
08:12:50 <naomi> ... we have similar research on this
08:13:01 <naomi> ... but not as deep as you did
08:13:08 <denkeni> s/hit resolution/did resolution/
08:13:23 <naomi> Mitsuhide: I'm currently developing by myself and I appreciate to hear the work outside of Japan
08:13:51 <naomi> denkeni: I only knew My Number system in Japan but I'm glad to hear your activity
08:15:08 <naomi> Mitsuhide: I want to AMT protocol to make it standardized one, and implement it to as government system
08:15:27 <naomi> denkeni: standardization of the data method will help a lot for the governemnt ot adopt that
08:15:45 <naomi> ... we can continue the discussion there about your deep methods application
08:16:07 <naomi> ... including security and privacy
08:16:11 <denkeni> s/deep methods/did methods/
08:16:53 <denkeni> s/data method/did method/
08:20:55 <naomi> rrsagent, please draft minutes
08:20:56 <RRSAgent> I have made the request to generate https://www.w3.org/2025/11/12-did-vc-challenges-minutes.html naomi
08:22:44 <naomi> present+ jay_Kishigami, Takimi_Mouri, Hiromu_Ogawa, Ryoya_Kawai, Michael_Wilson, Toru_Mariuhashi, Junko_Kamata, Takahiro_Aritaki, Ryo_Tsuyuki, Atsushi, Will_Abramson, Denken_Chen, Kai_Otsuki, Itoe_Kinjo, naomi
08:38:52 <naomi> naomi has joined #did-vc-challenges
08:58:59 <naomi> present+ Markus_Sabadello
08:59:06 <naomi> rrsagent, please draft minutes
08:59:07 <RRSAgent> I have made the request to generate https://www.w3.org/2025/11/12-did-vc-challenges-minutes.html naomi
09:52:09 <naomi> naomi has joined #did-vc-challenges
11:54:29 <naomi> naomi has joined #did-vc-challenges
12:58:03 <naomi> naomi has joined #did-vc-challenges
13:54:33 <tidoust> tidoust has joined #did-vc-challenges
13:54:36 <tidoust> RRSAgent, bye
13:54:36 <RRSAgent> I see no action items