Skip to main content

Minutes IETF102: dinrg
minutes-102-dinrg-00

Meeting Minutes Decentralization of the Internet Research Group (dinrg) RG
Date and time 2018-07-20 13:30
Title Minutes IETF102: dinrg
State Active
Other versions plain text
Last updated 2018-08-08

minutes-102-dinrg-00
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.