Decentralized Internet Infrastructure Proposed Research Group (dinrg) Date: Friday 20 July, 9:30 - 11:30 Room: Centre Ville Chairs: Dirk Kutscher and Melinda Shore Minutes: Melinda Shore Welcome and Agenda Bashing -------------------------- Slides: https://datatracker.ietf.org/meeting/102/materials/slides-102-dinrg-chairs-presentation-00 Stellar Consensus Protocol Update - David Mazières -------------------------------------------------- Slides: https://datatracker.ietf.org/meeting/102/materials/slides-102-dinrg-stellar-consensus-protocol-update-david-mazieres-00 David provided an update on the SCP draft (https://datatracker.ietf.org/doc/draft-mazieres-dinrg-scp/). The major changes in the draft have been in improved readability in response to questions and comments received on earlier versions of the draft. Status: a few people are implementing this and there are some things we still need to figure out in the protocol. There's work on formally verifying it that we'll hear about later today. Questions: Shane Kerr asked about what's meant by "stuck" in SCP - if something doesn't get enough votes (for nomination, not for balloting) to proceed, isn't it stuck? Answer: In SCP, you can always change your mind and vote for it if we're not making progress. Only those who haven't voted can change their vote (by voting). There's not a problem with nominating multiple values (there is a problem with allowing votes for and against). Shane: are there any clocks? A: there are some timers but they're not required for the safety or the non-blocking liveness of the protocol. There are timers associated with ballots. Formal Verification of the Stellar Consensus Protocol - Giuliano Losa --------------------------------------------------------------------- Slides: https://datatracker.ietf.org/meeting/102/materials/slides-102-dinrg-formal-verification-of-scp-guiliano-losa-00 Goals are: to develop a formal specification of SCP, formal proofs that the SCP specification satisfies its intended properties, and a formally verified reference implementation. Described an introduction to formal specification, using excerpts from SCP defined in the IVy formal specification tool from Microsoft. Why prove formally? Because distributed protocols are notoriously hard to get right and informal prose arguments are insufficient. Explained deductive verification in first-order logic. Current status: the high-level specification of the ballot protocol has been proved safe (see link in slides). Next: Produce a formal document, prove SCP's non-blocking property, and produce a verified reference implementation. Questions: Carsten Bormann: when you do a formal verification of a protocol you end up with a proof that what you modeled holds, but how do I know that what you modeled is actually the protocol? A: In this instance we're still in the process of of defining the protocol, so there's no existing protocol that we want to match. We could also check that an existing implementation corresponds to the specification by using the specification as a test oracle. Wes Hardaker: we're not positive that the proof you showed is not actually the protocol. A: this is a proof of the formal specification, not the prose specification. Wes: you have to make sure there are no other forms of input that are not accounted for in your specification. (missed name): Do you have any timers or time-outs in your model? A: I only prove safety and timers are used for progress. Q: you can have safety violations in race conditions. A: This proves that all possible race conditions are covered and will not cause a safety violation. Toerless Eckert: This won't tell me why the system shouldn't stop at a point in time and say that the assertion has failed. A: This is static analysis that you do beforehand so there is no assertion put in the code. Distributed Delegated Mappings - Jean-Luc Watson ------------------------------------------------ Slides: https://datatracker.ietf.org/meeting/102/materials/slides-102-dinrg-distributed-delegated-mappings-jean-luc-watson-00 Draft: https://tools.ietf.org/html/draft-watson-dinrg-delmap-00 Built on top of the SCP protocol. Described various existing mappings on the internet today (for example, email to public key) and problems around trust. Goal is to provide a common interface for authentication in mappings and to support delegation. The same structure can be used for a ton of different applications. The safety and consistency of these delegation tables must be provided by a consensus algorithm, in this case SCP. Considerations include who controls the root namespace, how we prevent spam, and scaling. Questions: Brian Trammell: with respect to your considerations at the end, I don't exactly see how we take the more delicate questions of governance and map them onto a consensus protocol. This is not a gotcha but rather a please think hard about this, and I am willing to help. (missed name): question about moving blocks between delegations. A: that's why there are timeouts. Once the timestamp expires the table authority can just modify the mapping. Coconut: Threshold Issuance Selective Disclosure Credentials with Applications to Distributed Ledgers - Shehar Bano ------------------------------------------------------------------------------------------------------------------- Slides: https://datatracker.ietf.org/meeting/102/materials/slides-102-dinrg-coconut-shehar-bano-00 Describes selective disclosure scheme - a user can choose which attributes to show to a verifier. Coconut supports blindness, unlinkability, threshold authorities, and authorities non-interactivity and is the first scheme that offers all of these properties. Based on BGLS signatures + Waters scheme + Pointcheval and Sanders (see slides). User verification is done through smart contracts on blockchains. Solves the problem of every blockchain node processing the transaction seeing the password, by having authorities outside the blockchain. A privacy-preserving petition application has been built using Coconut, and has been deployed and tested in Barcelona. Other Coconut applications include a coin tumbler (payment anonymizer), and censorship-resistant distribution of proxies (allows volunteers to unlinkably run verified proxies for censorship evasion). Questions: Robin Wilton: I'm aware of two other selective disclosure architectures. They are U-Prove from Microsoft, and IDMix from IBM. Have you investigated those? When you were talking about Chainspace and its use in smart contracts, if the user can use a single credential to sign multiple petitions while remaining anonymous and unlinkable, isn't that risk present anyway (a user can acquire multiple credentials). A: A verifier can check that a credential has been used only once. Daniel Kahn Gilmor: if the authorities are distributed but registering the same population it seems plausible that an individual could register with multiple authorities, creating multiple identities. David Mazières: I'm confused about the confusion. One credential says you have the right to vote, another says you have the right to drive, etc. A: yes, these would come from the Barcelona government, but different departments within the government. DINRG and ANIMA - Toerless Eckert --------------------------------- Slides: https://datatracker.ietf.org/meeting/102/materials/slides-102-dinrg-dinrg-anima-toerless-eckert-00 Provided a summary of what the IETF ANIMA working group is doing and how it could relate to what DINRG is working on. Existing ANIMA work can serve as an infrastructure or development platform for DINRG, and DINRG could help define guidelines or work for ANIMA. Described the ANIMA architecture. ANIMA wants to be the self-orchestrating self-configuring system, however many parts are centralized or decentralized. One problem is that we have no way to assert ownership, so this could be done in a decentralized fashion. Q: David Mazières: I'm wondering if there's been any interest in control over software updates on these devices? A: We haven't gotten to that point. Carsten Bormann: What I see on this diagram is really not so many protocols but most of them are actually documents that claim something and are signed by somebody else. In the SUIT working group the main outcome is a document, called a manifest, that contains signed claims. Maybe one thing we should think about is something like a calculus for deriving assertions from all these signed claims that we get. What are actually the commonalities between all these signed claims? Decentralized Internet Resource Trust Infrastructure - Bingyang Liu ------------------------------------------------------------------- Slides: https://datatracker.ietf.org/meeting/102/materials/slides-102-dinrg-decentralized-internet-resource-trust-infrastructure-bingyang-liu-00 The background is that the trust infrastructure in the internet is centralized, including the Resource PKI (RPKI), which is the trust infrastructure for IP addresses and AS numbers. These systems all have centralized or hierarchical structures. Roots have authority over their subtrees, so malicious or misconfigured roots can cause problems for their subtrees. System design: 1) eligible organizations run a decentralized ledger for consistent prefix ownership and mapping to ASNs. Smart contracts are used to ensure unique and aggregated prefix allocation; 2) prefix to AS mapping is done when an address owner initiates an ROA as a transaction and a smart contract verifies the address ownership and writes it into a ledger; 3) preventing address exhaustion is done by either ISPs must proving need for additional addresses by calculating a host density ratio, or using money. Open questions: 1) the interdependency between the blockchain and BPG, 2) the consensus algorithm, and 3) how to bootstrap. Q: Brian Trammell: you have a missing open question wrt the policy development process and have you verified that you can model that in smart contracts. Streamlining that policy out is not a feature. A: We investigated the policies of RIRs. Not all of those policies can be applied in practice. Brian: I strongly suggest that you take this to the address policy working groups of the RIRs. Policies applied to corner cases are there for a reason. David Mazières: if you could layer this on top of the delegated mapping work you could do a side-by-side comparison of the things that can happen, but you want to know how much additional benefit you get by putting the allocation policy into a smart contract. One particular problem that I anticipate is that it's going to be difficult to anticipate the density of the use of the address space. A consensus protocol could probe the density of the address space and different nodes could come up with different answers and become deadlocked. A: what we think is different from the delegation chain is that in a delegation chain you depend on others to give you the resource. The second is that in this case we calculated the assignment and logged it on the ledger. David: we can create a bunch of fake delegations and log those. A: I will think about it. Alyssa Cooper: there's been some confusion about how address blocks can be assigned for experimentation, and it requires IETF review.