Session Date/Time: 17 Mar 2025 10:00

keytrans

Summary

This keytrans session covered recent protocol document changes, focusing on time authentication and its impact on security. A proposal for self-balancing prefix trees to improve efficiency in non-privacy-sensitive applications was discussed. Finally, the session included a presentation on the formal verification efforts of the keytrans protocol.

Key Discussion Points

Time Authentication:
- Discussed issues with the original "clock label" approach to time authentication due to potential forking and misbehavior concealment.
- Introduced the solution of making timestamps a first-class feature of the protocol, associating them directly with log entries.
- Explained the concept of "maximum lifetime" for log entries, enabling provable and secure pruning of the tree.
- Presented the idea of "reasonable monitoring window" and "distinguished log entries" to coordinate label monitoring and reduce state retention requirements.
Self-Balancing Prefix Trees:
- Motivation: Improving efficiency for non-privacy-sensitive applications by avoiding unnecessary VRF usage.
- Problem: Typical balanced search trees store data in intermediate nodes, doubling the size of cryptographic search proofs.
- Solution: Allow multiple starting points (cursors) within a search range, with the transparency log indicating the most efficient cursor to use.
- Data Density: Efficiency depends on data density, not just total range of values
- Debate ensued whether hashing was a better strategy for dealing with tree balance
Formal Verification:
- Goals: Verify the client side of a Go reference implementation, proving that all clients agree on their view of the log.
- Property: For all identical queries, the results of verifyLatest should be the same, independent of the server response.
- Challenges: The specification, while well-written, relies on non-obvious insights into algorithms and graph theory. Efforts are underway to make it less ambiguous.
- Signatures in tree head should include a domain separator
- Extension field should be added for client configuration information

Decisions and Action Items

Action Item: Felix to open issues and pull requests regarding specification ambiguities to facilitate concrete discussions.
Action Item: Collect a list of use cases that would benefit from the self-balancing prefix trees.
Action Item: Engage in a follow-up discussion on the formal analysis effort, particularly focusing on the opened issues and pull requests.

Next Steps

Continue refining the specification based on feedback from implementers and formal verification efforts.
Further explore the use cases and requirements for self-balancing prefix trees.
Advance the formal verification of the key transparency protocol.