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

• Upcoming
• Tentative
• Breakout Sessions

We propose the international standardization of the AMT Protocol (Japanese name: AMATELUS) — a Lean4-verified protocol designed to solve the three critical challenges encountered when introducing DIDs and VCs into Japanese municipal systems.
These challenges are not unique to Japan; municipalities and enterprises around the world likely face the same issues.

Three Core Challenges in Implementing DIDs and VCs for Smart Cities

1. Traceability Problem – Resolving DID Documents on blockchains or IPFS makes DIDs inherently traceable.
2. Over-Disclosure Problem – Selective disclosure in VCs still requires revealing excessive personal information and enables cross-linking of identities.
3. Auditability Problem – Using ZKPs can conceal DIDs and personal data but makes legitimate governmental audits impossible.

To move beyond proof-of-concept and enable real-world deployment of decentralized identity systems,
we present the AMT Protocol, a concrete and verifiable solution integrating decentralized identity, privacy preservation, and public accountability.
A detailed Blueprint and formal verification in Lean4 are already publicly available.

Web site: https://amatelus.com
DID method PR: https://github.com/w3c/did-extensions/pull/639
Lean4 code (Japanese): https://github.com/amatelus/amatelus

Agenda

Chairs:
Mitsuhide Matsuda

Description:
We propose the international standardization of the AMT Protocol (Japanese name: AMATELUS) — a Lean4-verified protocol designed to solve the three critical challenges encountered when introducing DIDs and VCs into Japanese municipal systems.
These challenges are not unique to Japan; municipalities and enterprises around the world likely face the same issues.

Three Core Challenges in Implementing DIDs and VCs for Smart Cities

1. Traceability Problem – Resolving DID Documents on blockchains or IPFS makes DIDs inherently traceable.
2. Over-Disclosure Problem – Selective disclosure in VCs still requires revealing excessive personal information and enables cross-linking of identities.
3. Auditability Problem – Using ZKPs can conceal DIDs and personal data but makes legitimate governmental audits impossible.

To move beyond proof-of-concept and enable real-world deployment of decentralized identity systems,
we present the AMT Protocol, a concrete and verifiable solution integrating decentralized identity, privacy preservation, and public accountability.
A detailed Blueprint and formal verification in Lean4 are already publicly available.

Web site: https://amatelus.com
DID method PR: https://github.com/w3c/did-extensions/pull/639
Lean4 code (Japanese): https://github.com/amatelus/amatelus

Goal(s):
This session aims to gather and discuss the challenges faced by municipalities around the world in adopting DIDs and VCs for smart city development, and to explore how the AMT Protocol approach can help address these issues.

Agenda:

1. Share the technical and political challenges of building smart cities using DIDs and VCs.
2. Present the AMT Protocol’s solutions and provide a brief overview of the Lean4 formal verification results.
3. Disclose the constraints observed in Japanese municipalities and discuss the limitations that exist in other countries.
4. Review coexistence and distinctions between the AMT Protocol and related international standards and technologies.

Materials:

• Session proposal on GitHub

Joining Instructions

Instructions are restricted to W3C users . You need to log in to see them.

Export options

Personal Links

Please log in to export this event with all the information you have access to.

Public Links

The following links do not contain any sensitive information and can be shared publicly.

• Download as ics