Minutes interim-2024-keytrans-01: Tue 17:00
minutes-interim-2024-keytrans-01-202410221700-00
Meeting Minutes | Key Transparency (keytrans) WG | |
---|---|---|
Date and time | 2024-10-22 17:00 | |
Title | Minutes interim-2024-keytrans-01: Tue 17:00 | |
State | Active | |
Other versions | markdown | |
Last updated | 2024-10-22 |
IETF 121 Interim Keytrans 01
Online - 2024-10-22
\?
Agenda
- interim (slides-interim-2024-keytrans-01-sessa-interim)
- draft-keytrans-mcmillion-protocol
(slides-interim-2024-keytrans-01-sessa-draft-keytrans-mcmillion-protocol) - Formal Verification of Transparency Systems
(slides-interim-2024-keytrans-01-sessa-formal-verification-of-transparency-systems) - Updates in witness ecosystem
(slides-interim-2024-keytrans-01-sessa-updates-in-witness-ecosystem)
draft-keytrans-mcmillion-protocol
Presented by Brendan McMillion
Terminology has been updated from "key" of key/value to "label". The
terminology was confusing because we were looking for keys within the
transparency log by key. Now we search for keys by labels.
The slide introduces the Log tree again, which is a left-balanced binary
tree. it's easy to append new data, and easy to provide consistency
proofs.
The prefix tree store key-value pairs. The orders are based on the
binary representation of the key.
Log tree provides consistency proof, prefix tree provide search proofs.
A combined tree is both: a Log tree with prefix trees for leafs.
Why is this different? With this new construction, we can put multiple
label mapping in one tree update! It has the benefit of allowing
efficient preloading with fake/real data. There is only one update.
Batching is useful for PQ signatures which are expensive, and allow for
smaller proofs if batches are large.
From the chat: this is a welcome change, and possibly similar to
OPTIKS
With a third party auditor validating the construction of the tree, you
can quickly skip to the latest version of the tree. This assume the
auditor is honest and non colluding, but allows for faster monitoring
for the client.
To find the most recent version for a label, one can use a "full binary
ladder" process. It allows to quickly find it. The reader is invited to
look at slide 11/23, it explains the process with nice pictures.
Another important check is to inspect different versions of the prefix
tree to see that they're consistent. This allow to confirm the tree is
constructed properly.
Monitoring: when search path grows, clients want to know it does not
change unexpectedly.
Future work:
- Replace the prefix tree with a self-balancing tree. This is useful
for non privacy sensitive applications, for which a VRF would be
wasteful. - Add support for proxy mode, which would allow anonymous
communication - Consider stronger enforcement of time, which could improve searching
and monitoring - Move struct definition to COSE/CBOR
Esha and Kevin: thank you for supporting batching per prefix tree, good
change!
Formal Verification of Transparency Systems
Slides
Presented by Felix Linker
Presentation: is working on protocol verification in the symbolic model.
For instance, formal verification of iMessage PQ3 in Tamarin.
Goal: demonstrate formal verification are the wrong tools for verifying
KT.
Parakeet, while presenting the best security proof for the ecosystem, is
not easy to read, nor to verify. Some people tried to use proverif to
validate transparency protocols, but they did not scale.
Another cool paper presented authenticated data structures generically,
but the exact guarantees are not clear, and the technique do not scale
to all security properties.
Diving in the ProVerif approach. Encryption is defined as a function
with two arguments. And you pass arguments to it. It's hard to prove
relation on terms, such as x is lexicographically smaller than y, which
is a problem when you model a prefix tree.
How do authors do it then? Only considers system where lexicographic
order does not matter.
Diving in Type system approach. Values are either authenticated (root
hash), or unauthenticated (commitment). One implementaion and compiler
generates server and client code, respectivally generating and consuming
proofs. Proofs are stack of hashs (math function calls).
Both approaches have benefits. Ideally, we would use a high-level
language tailored to code verification, with a reference implementation
of KT.
It'd be great to understand how such proofs can be generalised, and
running an audit should give us provable guarantees of the past.
Updates in witness ecosystem
Slides
Presented by Thibault Meunier
Current status of ecosystem: CONIKS, SEEMless, OPTIKS and ELEKTRA (not
implemented yet)
Client -> Application => Client -> Log (Users can monitor changes now)
Attacks: split-view, providing different view of the log to different
clients
Monitoring is important to make sure clients all have verifiable same
views
Current Approaches (arch draft -01)
Out of band verification between clients
3rd Party Auditor (client trusts the auditor, deployed by WhatsApp).
Digging in, you're validating global uniqueness and you also have some
compute
Introduce Witness: signs the timestamp and hash of the tree head.
Felix: how is the Witness independent of the protocol?
Thibault: the message format is protocol-independent.
WhatsApp wanted to ensure the global unique view could be delivered very
fast. "Structure of the tree" is done async, and can be slower.