okay so thanks a lot and I'm also very
excited to be here at Def Con I never
was was here although I had several
times watch the videos off of James Otis
area so so this talk will be about Tarun
our work it's like a joint research
project between the Technical University
of Darmstadt in Germany and the
University of Warsaw in Poland in
several of my co-authors so this is some
kind of academic work so we published
some papers at some top conferences in
security and several of them also here
sitting there over there and here in the
front row so we are very happy to answer
questions later also okay so as we have
seen already today several talks there
are many exciting projects currently
going on people like do a lot of
research and also development in
building different types of state
channel and payment channel networks so
I would like to explain to you basically
at a high level what we do in karoon so
in Peru essentially the goal is similar
to the previous two talks of Moore and
Liam we are trying to build generalized
state channel networks and I will talk
in a moment a bit in more detail what we
understand about general state channel
networks the main technique that we
developed in our work and I'm kind of
happy that nobody so far talked so much
about this is about virtual Channel so
some people also call it meta channels
and I will explain in more detail what
actually are virtual channels and what
are the advantages of these virtual
channels and the special feature and
maybe this is also one distinctive
feature of our project because we have
like a very strong background in
cryptographic research we focus a lot
also on not only designing these
protocols at an abstract level but also
proving the security of these protocols
okay so we usually when we come up with
a design of what the protocol is
specification of the protocol what it
what it what it is then we also usually
carry out a formal security proof that
it satisfies certain security guarantees
so what is the state channel network
I will essentially show you our view at
the rune of what this is the basic
ingredient and you have already seen
this in several other talks we call them
legislators and let us state channels
they are built directly over the ledger
okay so that's why they call legislate
channels so we have these two parties
Alice and Bob and they want for example
to execute some contract off chain for
example it could be some chess game or
some other online game or a payment or
whatever and the letter state channel
then works in three phases so in the
first phase the party's Alice and Bob
they have to go to the blockchain and
create this legislature and help this is
happening with some kind of cryptography
like signatures are exchanged and so on
and then at the end parties Alice and
Bob don't have a pointer here Alice and
Bob they can like go to the send
something to the blockchain and deploy
some channel contract which is later on
going to be used potentially if there
are some disagreements between the
parties
so once the letter state channel has
been deployed so it's established the
parties can then like execute contracts
of chain so this is the whole purpose of
course so they can like for example run
multiple execution of a chess game
without ever touching the blockchain and
s like Liam mentioned earlier so we also
support like this generalized state
channels where you can not only run a
chess contract but you could run several
chess contracts or like even completely
other games also in this in this in this
legislature and the main point here is
that as you can see that this execution
of contracts so this update of the state
this is carried out of jail
so it's carried out without Alice and
Bob needing to interact with the
blockchain so then at some point when
Alice and Bob they don't want to use
anymore this legislature state channel
then they can settle this channel and go
to the blockchain close it and this
again requires unchain communication
okay so this is essentially the three
phases of a basic state
now we would like to extend this to
forming a network so this is the most
simple network that you can think of you
have like LS ingress and Bob Ellis is
connected to Ingrid by a letter state
channel and Ingrid is connected to both
via a letter State Channel and now what
Ellis wants to do is she wants to
execute off chain a contract with Bob
okay so how can she do this there are
several options to achieve this the
first option would be of course we just
have seen like legislate channels so we
could just use this okay so we could
just create a new letter state channel
between Alice and Bob but this of course
has some disadvantages because as you
saw like creating a channel let us say
channel this requires interaction with
the blockchain so I need to communicate
to the ledger deploy it as contracts
this is slow so it takes some time it is
also expensive because like deploying a
contract takes cost a lot of fees so you
would like to avoid this so another
option is because we have these two
channels between LS English and English
and Bob we could use this existing
infrastructure to let Alice and Bob
directly execute contracts between them
by using these two underlying
legislators okay so and this is of
course the advantage that this can be
fast if we manage to design such a
protocol can be fast it can also be
cheap because it does not require any
communication with the underlying ledger
and this is essentially what we do in
Peru
so we developed a technique that we call
virtual channels and the main idea is
you can think of these underlying let's
just state channels as like a two-party
blockchain okay so let's just state
channels between Alice and Ingrid and
the letter state channel between Ingrid
and Bob they offer you something similar
to what the blockchain offers you so how
can we now create a virtual state
Channel so essentially also this works
in three phases in the first phase in
the creation of the legislature now we
run a protocol between Ellis Ingrid and
Bob now there are three parties involved
okay Ingrid kind of takes the role of
the blockchain to some extent
and this is object so the communication
between the the parties is going on like
off chain without touching the
blockchain so it can also be very fast
of course and then you can compare this
to let's just state channels they're the
creation was on chain so it took
potentially a lot of time now executing
executing is very similar to let us say
what happens in letter state channel so
Alice and Bob they can now execute
multiple contracts of chain so also here
we can allow contracts several contracts
potentially to be executed off chain and
finally when Alice and Bob they don't
want to use anymore dead Channel then
they can close it by again not going to
the to the blockchain not going to the
ledger but going to the underlying
legislature okay again this has the
advantage that all of this year as you
can see all of this create execute and
close all of this happens off chain
without interaction with the ledger
which is in contrast to the legend state
channels now this is very nice but we of
course would like to consider to also
capture exception more complicated
networks so like here we have much more
complicated network like little more
complicated Network and we want for
example that Ellis wants to talk to Dave
okay so how can they do this you can
just apply this technique that I just
thought I told you about
recursively so we could let Ellis first
create a virtual state channel with Bob
then over the virtual state channel
between Alice and Bob Ellis can now
create another virtual state channel was
clear and then this can be continuing
like this until finally Ellis has it has
reached Dave and then they can execute
in this final channels they can execute
their contracts of chain so what are the
advantages of channel visualizations
there are several of them that I would
like to highlight first of all this is
low costs so since the intermediary is
not involved anymore in the execution of
the the contract similar to the later
state channel where the blockchain is
not involved in the execution of the
contract
this can be very fast and it can also be
cheap so there in particular the
intermediary does not necessarily need
to ask for fees we also have better
privacy so because the intermediary does
not know what happens in the letter
individual state Channel Alice and Bob
can keep the state updates private and
tears of course the other advantage
there is no availability required so
even if Ingrid goes offline for a while
then Alice and Bob can still continue
playing chess which is of course a nice
feature so now you have seen a basic
idea of how we construct generalized
state channels now or like what are
actually general stations you would like
of course to know how you can construct
them unfortunately I cannot explain in
detail how this works now because it
will take quite a lot of time and we can
I would refer liked to refer you to our
papers which are on the webpage it was
mentioned on the first slide the one
thing that I want to explain to you is
what happens in the case of corruption
so corruption makes as we all know our
life more difficult and this is also why
designing such protocols gets quite
complex so we have the first case the
first example that I would like to look
at with you is now the following so we
have Ellis Ingrid Bob and clear and
Ellis wants to play chess was clear so
Ellis can open a virtual state channel
between Ellis and clear by using this
recursive approach that I just explained
and then she can open a chess contract
and maybe in this chess contract she did
some several moves okay she played very
smartly and at the end she is in state n
minus one and there is only one state
left substitue finally wins the game ok
so this has to submit to execute to the
next state and then she will win but now
of course clear and potentially all the
other parties they don't have any
interest in this ok so they tend to
interrupt and try to prevent this they
disappear like just in this example that
mu short on this slide they disappear
and then we still have to finish
finalize this execution because we want
to have a secure protocol so how can
this work at the very high level of
course it gets very technique
because of their many Sitecore aside
cases that we have to do is essentially
Ellis first tries to execute the
contract in the underlying virtual
channel between Bob if this also fails
because in my example Bob is also
corrupt and essentially everybody can be
the protocols have to work even if all
parties are corrupt except for this
single party and if this also fails then
she goes to the next underlying
legislation on here she tries to execute
to the next state in this and then
finally if also England as corrupt she
goes to the to the underlying ledger
okay and of course we trust a serum we
trust vitalik so we will get eventually
we get eventually the execution time
okay so this is the first example that I
would like to look in so now let's look
into the next example how can we deal
with the corruption case when Alice and
Bob are corrupted and they try to cheat
Ingrid and try to steal her money so
they want to steal some is from from her
and this is like a kind of can be a
difficult case so for example consider
the following situation we have a again
a virtual led a virtual state channel
between Alice and Bob and we are having
a rerun a contract and this contract has
the following property that if state n
minus 1 is set by n minus 1 it pays 5 is
to Bob and in state n it pays 5 is to
Alice ok so now what Alice and Bob can
do to try to cheat Ingrid for her money
they could try to submit in the
underlying legislation Al's because I
said this underlying legislation else
take the role of the blockchain the
accept MIT in these underlying lesson
state channels these conflicting states
and this would result in the following
situation if you don't design a
carefully develop protocol then it would
result in the situation that LS the
corrupted LS wins five coins to corrupt
the Bob who wins five coins but Ingrid
who just who's just played the role of
the intermediary she was not even
involved in this contract
she loses 10 coins okay so this is
something that we want to prevent and we
can do this by using the by developing a
carefully designed
called in particular using timings or
carefully chosen timings to deal with
these special cases unfortunately this
is like very simple cases only and it
gets much more complicated in our
situation so we have this complicated
Network and now we want to handle also
full concurrent protocol execution so
many things can happen in parallel
packets can open contracts in parallel
for example here this middle party here
she is involved in two virtual state
channels and she runs possibly several
contracts and them in parallel and they
can also be many corrupted parties and
of course we want to deal with this
situation okay so we want to design
protocol that even is secure when there
are so many corrupted parties when so
many things happen in parallel when
these all these messages are exchanged
and the protocol should guarantee
security the security requirements that
we specified so how can we design such a
complex protocol and for this we rely on
what is essentially the approach of
modern cryptography which uses what I
mentioned the beginning security proves
to kind of design the protocol using a
sound methodology so this approach of
modern cryptography which we use
essentially for designing cryptographic
protocols like whatever encryption
schemes are more complicated schemes it
works like this that you first specify
what is your security definition so you
what do you want that the protocol
actually should achieve then we design
the protocol so we come up with a
candidate scheme that hopefully achieves
the security definition and once we have
done this then we prove its security
okay so at the point so okay we prove
its security so at the point then of
course this process is not like so nice
as I showed to you here okay it's like
iterative way so we sometimes you come
up with the candidate scheme we find
some problem in this candidate scheme so
when we try to prove it so the proof
course fails okay so that's the nice
thing about it it's gives you a sound
methodology so to say so the proof fails
we have to adjust the protocol and then
we try to again prove it we fail we try
to again prove so we could try to adjust
it we try to again food and so on and so
forth
at some point hopefully then we have a
security proof that our protocol the our
protocol specification guarantees the
security requirements that we have
specified earlier in this definition but
so this is the main benefits of this
approach is that it provides a sound
methodology for designing complex
protocols and it also prevents insecure
Atok design so there is like maybe some
of you have heard about it there's like
this protocol of this probably most of
you have heard about TLS okay and it was
designed in a talk way without having it
without using this kind of approach of
modern cryptography of proofs provable
security and it turned out that there
are many kind of bugs in this protocol
okay so there are many people found
problems and now they are trying to fix
it it's a kind of a cat-and-mouse game
and we want to prevent this from the
start and actually now in the new
version of TLS people decided to use
security proofs to develop the protocols
so we believe that we should also do
this from this from the start with
something as complicated as state
channel networks so what is our basic
framework to use this this is the
quality universal comm possibility
framework and some time ago we gave a
talks if you gave some talks at the
workshop in Berlin and everybody liked
this universal compatibility framework
so I would like to mention it here as
well so this is basically how we kind of
define security what actually security
means okay so so we have these two
worlds ideal world and the real world
the ideal world is some kind of abstract
specification of what kind of security
properties the protocol should satisfy
okay so it's very simple it just can be
written maybe on half a page yeah so
it's very simple specification of what
this protocol it is and then the
protocol can be like pages long maybe in
our case was 2000 I don't know whatever
so and now we would like to show that
actually this protocol has the same
security features then this very compact
description this very compact RP
description of the specification and
this is done by what is called a you see
proof a universal comm possibility
security proof and this essentially
reduces complex protocol to something as
simple as this idea of functionality so
before I run out of time I want to
quickly
talk about some extensions and implement
it and also briefly about implementation
so we recently worked on some follow-up
of our original Peru Network paper and
we extended it to also cover or to also
support multi-party state channels so
what is a multi-party state Channel
we have now a situation Alice Bob Carol
David and Ellis Bob and David they would
like to execute some multi-party
contract like maybe a game that involves
poker game that involves three players
and they can do this as follows they
built first a virtual channel between
Bob and David which was stationed
between Bob and David that's what we
already have seen in this talk and then
over this virtual state channel and the
underlying legislation or between Alice
and Bob they can create a multi-party
state channel and in this case this one
then they can deploy a gaming contract a
multi-party gaming contract so about
implementation we are cooperating with
the company Bosh to provide an
open-source implementation for a cerium
of course we also happy to cooperate
with other people we are like a research
project mainly at the moment I talked to
our colleagues from Porsche and they are
currently developing the note software
for later state channels they will
release this in at the end of this year
as an open source project then in hue so
on the second half on the first half of
2019 we will they will release an
implementation of the visual state
channels and the Hopf software and then
later at the end of the year they plan
to integrate it in some industry use
cases okay so this is for the
implementation at the moment we of
course happy to like this would be open
source released soon and it would be
great if people here collaborate on this
with us so let me conclude my talk so
what we are trying to build is provably
secure layer two solutions we will also
look into other possibly soon other
solutions like plasma and so on and we
believe that to make them ready for mass
for mass of users
should there should be solid foundations
for these protocols okay so and that
just explained you at a very high level
what this is like giving these
definitions making a protocol
specification really formal and
releasing it to the public and then
proving the security so this is
essentially what we did we designed a
protocol it's out there you can go to
our web page you can read it and it's
it's really like I think fully described
so you can like take it and implement it
where maybe not tonight but maybe in
five nights okay
so then you can then we have security
proofs we prove that these protocols are
secure and the next step that we would
like to do is because these proofs are
quite complicated very involved like
many corner cases we have to take care
of we would actually like to formally
verify them by machines so there are
some kind of tools like easy crypt and
so on we would like to use to use them
to verify that actually our proofs are
correct we of course hope that they are
correct already but better to let them
check by a machine this is what we are
currently doing we want to in the future
work more on implementations and in
particular this is maybe a long-term
goal also provides some formally
verified implementation and of course is
it's very necessary to start with a
sound protocol before you like implement
something as complicated as this because
if you make mistakes at the protocol
level already then you don't need even
to formally formally verify your
implementation so talk further
information I hear I would like to thank
all our sponsors here it's for our
research and I'm happy to take questions
you
so when you're writing these protocol
specs to basically like specify or come
up with set of failure modes and then
prove that those failure modes can
happen and if so then then of course
there might be failure modes that you
did not think of right yeah and another
question is which frameworks are using
like what protocol specification
languages and proving languages are
using so the first question was if there
can be connect is I mean like of course
what we do is like we have a
specification of the after after of the
of the protocol okay we give this then
we have also model and then we show that
whatever and at worst we can do in this
model
he will not succeed whatever this means
for example he will not be able to steal
money from the intermediary okay like
whatever his behavior is as long as he
behaves as specified in the model so all
this kind of stuff that you heard today
like replay attacks and this kind of
stuff this is all covered by our model
automatically by this you see framework
but other stuff maybe it's not covered
like for example side channel attacks
okay if there is some kind of adversary
who tries to break it by doing some side
channel attack or I don't know some
other stuff this is the not covered by
our our model and you would have to
extend it also currently our model we
don't really like have integrated fees
yet so this is something also that we
would like so gasps you don't have this
probe you don't have this formally
modelled yet and this would also be some
next step the second question was well
yeah second part was just a twitch so
yeah at the moment we have like some
abstract specification of the pseudo
code of the protocols okay so it says
okay party a creates a signature sends
it to Bob then Bob does something waits
five seconds it creates a signature of
this sense it to others and so on so
there is something like this it's like a
like a pseudo code essentially but we
are trying now to move it closer to
something like formal language that can
then be checked by these automated tools
okay so you haven't like written
anything like from a large specification
and like like temporal if we have not
written it in Coke yet or some like I do
wanna yeah we will do this we are
working on this
we also here so you can catch us later
all right thanks passion
[Applause]