Session Date/Time: 05 Nov 2025 21:00

KEYTRANS

Summary

The KEYTRANS working group met to review the status of the architecture and protocol documents, and hear an update on formal verification efforts. Key discussions focused on proposed changes to the protocol document, including consolidating search algorithms, adding an explicit update algorithm, clarifying owner monitoring, introducing a formal credential type, and implementing auditor hot-swapping. The architecture document was deemed close to Working Group Last Call after minor additions. Formal verification efforts have gained momentum with a new team member and a refined approach. A significant call for volunteers to review both documents, especially for cryptographic aspects of the protocol, was made.

Key Discussion Points

Architecture Document Update (Brendan):
- No major changes have occurred.
- Proposed Editorial Changes: Update references to protocol details that have changed, and add clarifications/common questions.
- Proposed Substantive Addition: Include the concept of "maximum lifetime," an important protocol feature enabling verifiable deletion of old log entries for pruning and privacy compliance, which was previously missing from the architecture document.
- The document is expected to be ready for Working Group Last Call after these additions, to be published as an informational document.
Protocol Document Update (Brendan):
- Fixed Version Search: Consolidated the previously distinct "fixed version search ladder" and "greatest version search ladder" into a single "search ladder." The new algorithm performs a binary search but can stop early if the target version is found to be the greatest existing version. This change improves security reasoning by simplifying interaction paths without significantly impacting efficiency.
- Update Algorithm: Introduced a new, explicit algorithm for users to verify that a label's value was updated correctly. This addresses scenarios where service providers make offline updates (e.g., timestamps) or multiple new versions are created simultaneously in a single log entry.
- Owner Monitoring: The previously underspecified "check each distinguished log entry" was replaced with an explicit depth-first search algorithm, making it implementable and specifying how owners should initialize their state.
- Credentials: Added an explicit credential type, moving away from simple serialization of search responses. This allows for smaller credentials (by omitting redundant, pre-distributed information) and specifies correct verification, including sandboxing verification state to preserve anonymity. Two types were introduced: standard (for existing state) and provisional (for new state).
- Hot Swapping Auditors: Implemented a mechanism allowing secure changes to the third-party auditor while the transparency log is operational. This is achieved by verifying that the new auditor's "start position" overlaps with the previous auditor's "stop position."
Discussion on Credentials: Questions were raised about whether the explicit credential type should be standardized within the protocol or handled at the application layer. Brendan argued for standardization to reduce redundancy and define specific verification rules, particularly for long-lived, offline-verified credentials (e.g., for anonymous communication) which may have different validity windows than direct online lookups.
Overlap with DMSC/DAIN: A question was posed regarding potential overlap or integration with DMSC or DAIN (related to DNSSEC/DANE). Brendan indicated no specific work in this area but expressed openness if there's community interest.
Implementation GitHub: Brendan clarified his GitHub repository contains implementation code, not the draft documents. The chair suggested considering a working group GitHub repository for shared code.
Target Audience for Specification: Discussion touched on whether the specification is intended for existing deployments of Key Transparency or future ones. Ideally both, but historically, new specifications often drive new implementations unless there's a strong motivation (like an IETF standard) for existing ones to converge.
Formal Verification Update (Felix):
- No definitive quantitative progress to announce yet.
- Team Expansion: Kwok Wai Louis, a Master's student at ETH Zurich, has joined the team, dedicating significant time to formal verification.
- New Direction: The team has adopted a new technical approach to the problem after initial challenges.
- Outlook: Optimistic that parts of a second independent implementation, referenced by the next WG meeting, will be available for verification efforts.
- Scope of Verification: Felix clarified that his formal verification focuses on the overall protocol flow, the relationships between steps, and the state transition systems of different parties using a symbolic model. It does not cover cryptographic primitives like hash function construction or collision resistance, which would require separate cryptographic review.

Decisions and Action Items

Decision: The architecture document will proceed to Working Group Last Call after minor edits to include the "maximum lifetime" concept and update cross-references to the protocol document.
Action Item: The chairs will initiate the Working Group Last Call for the architecture document once the specified edits are complete.
Action Item: The chairs will seek a cryptographic review for the protocol document, initially within the working group. If sufficient expertise is not found, referral to CFRG may be considered.
Action Item: Thibault volunteered to review the protocol document for general flow and implementability.
Action Item: Deb volunteered to re-read the architecture document in preparation for its Working Group Last Call.
Action Item: Jonathan volunteered to provide a list of unclear sections or ambiguities in the protocol document based on his implementation attempts.
Action Item: Brendan will continue to work on a complete implementation of the draft and gather deployment experience.

Next Steps

The chairs will follow up on the architecture document edits and initiate its Working Group Last Call.
The chairs will facilitate the cryptographic review of the protocol document.
Brendan will continue implementation and seek deployment experience.
The formal verification team will continue their work with the new team member and approach, aiming for a referenced implementation by the next meeting.