►
From YouTube: IETF113-LAKE-20220321-1330
Description
LAKE meeting session at IETF113
2022/03/21 1330
https://datatracker.ietf.org/meeting/113/proceedings/
A
B
C
C
A
C
C
All
right
good
afternoon
for
the
people
here
good
morning
good
evening,
whatever
it
is
for
remote
people,
welcome
to
the
lake
session
at
itf.
113
we've
fairly
full
agenda
today,
so
we'll
be
trying
to
keep
the
time.
I
think
I'm
gonna
do
some
of
the
administrative
stuff,
but
it's
just
going
to
look
after
the
technical
content,
but
I'll
be
hassling
people
if
they're
using
too
much
time
or
getting
close
to
their
time.
C
C
Thank
you,
and
as
far
as
I
can
see
that
the
jabra
room
is
connected
to
meet
echo
and
to
the
matrix
stuff,
that's
no
longer
supported
and
it
seems
to
be
unidirectional
talking
to
zulup
if
you're
using
xulip.
So
if
you
write
a
message
in
zulup,
I
might
see
it
here,
but
other
people
might
not.
C
C
There
is
a.
There
is
a
on-site
tool
that
allows
you
to
join
the
mic
line
and
to
take
part
in
polls.
C
That's
that's
a
pretty
limited
interface,
so
you
might
want
to
just
join
that
in
your
phone
and
be
in
the
other
one
on
your
on
your
laptop.
If
you
didn't
for
remote
people
again,
usual
things
make
sure
audio
and
video
are
off
unless
you're
presenting.
C
C
Okay,
so
our
agenda
we've
got
two
hours.
We're
on
the
first
point
militia
will
give
a
quick
update.
We
have
reports
on
hackathon
some
developer
feedback
militia
has
some
implementation
feedback
as
well.
Security
updates,
then
we'll
be
talking
about
the
various
pieces
of
analysis.
Work
that
have
been
happening
on
the
current
drafts.
C
C
A
A
So
the
the
article
kind
of
summarizes
the
the
protocol
and
invites
the
community
to
study
it
in
its
different
model
and
which
proved
to
be
a
good
idea,
because
we
already
received
quite
some
feedback,
as
you
will
see
during
the
this
meeting,
because
of
that,
the
ad
hoc
specification
was
frozen,
meaning
that
we
did
not
publish
any
new
versions
in
the
data
tracker
since
itf-112,
but
the
author
team
was
not
lazy
and
then
they
kept
working
on
the
specification
in
github.
So
currently,
the
latest
version
is
the
editors
version
in
github.
A
That
said,
we
will
be
discussing
the
next
steps,
how
to
proceed
and
how
to
get
organized,
considering
these
concurrent
activities
that
are
taking
place,
so
we
will
present.
Today's
meeting
is
a
little
bit
peculiar
in
that
we
have
the
chartered
items
at
the
end
of
the
meeting
the
items
of
the
charter
of
the
working
group.
This
is
because
we
are
giving
priority
now
to
the
analysis
that
is
taking
place
and
the
main
chunk
of
the
meeting
will
be
given
to
the
to
the
security
analysis
from
different
teams
that
are
involved.
A
So
just
to
give
a
brief
overview
of
about
this
article
that
was
published
in
ieee
computer
magazine.
It
summarizes,
I
said
it
summarized
the
protocol.
I
presented
it
briefly
before
it
was
even
published.
During
the
last
itf
meeting,
it
invites
the
community
to
study
the
protocol
in
the
two
models
symbolic
and
the
computational,
as
well
as
the
the
implement
to
provide
some
feedback
and
code
on
the
implementation
security.
A
Yeah
and
the
last
point
on
this,
one
is
like:
if
you
didn't
notice
once
I
was
correcting
the
proof
of
the
article
in
ieee
computer
magazine,
I
found
out
that
cosy
stands
for
common
open
software
environment
protocol,
so
that
was
kind
of
funny.
So,
yes,
we
went
ahead
and
corrected,
but
it
was
a
bit
it
was.
It
was
a
funny
situation
with
all
the
details
that
we've
been
working
on
in
terms
of
this
article
and
then
the
whole,
the
big
old,
the
big
title
coming
out
wrong.
So,
yes,
that
was
corrected.
A
So,
as
I
said,
today's
meeting
is
focused
on
community
feedback,
so
we
have
two
presentations
from
the
implementers
as
well
as
I
will
give
as
a
participant
of
the
working
group,
give
a
presentation
on
the
implementation
security
update.
That
is
also
kind
of
implementer
feedback.
A
We
will
have
a
presentation
on
the
symbolic
model:
progress
as
well
as
in
the
computational
model.
Progress
model,
analysis,
progress
and
in
terms
of
the
formal
status
of
the
working
group,
so
we
have
a
milestone
that
is
set
for
march
2022
to
ship
the
document
to
the
isg.
A
A
G
Can
you
hear
me,
I
suppose
so
so
this
is
a
short
report
from
the
academy
we
had
the
past
weekend,
mostly
on
site
next
slide,
please
yeah.
The
focus
was
very
much
on
development.
I
was
even
before
testing
and
especially
malicious
worked
a
lot
on
his
implementation
for
rust
aspect
as
part
of
a
bigger
project.
G
I
understood
to
produce
something
it
was
verifiable,
first
of
all
and
and
then
usable
later
on
also
for
microcontrollers
and
other
environments,
and
this
is
pretty
ambitious
indeed,
and
the
goal
was
very
specific
to
produce
a
runnable
implementation
very
minimal,
especially
with
the
goal
to
end
up
with
the
smallest
possible
size
for
the
most
critical
edit
message
number
two,
which
is
something
you
can
achieve,
considering
the
configuration
summarized
here
so
thinking
as
initiator,
only
static
static,
defilment
and
id
cred
as
kid
specifically
integer
trying
to
avoid
any
any
dependencies
and
and
to
use
harder
acceleration
when
possible.
G
Next
slide,
please
right
the
the
start
was
not
entirely
from
scratch.
Something
was
available
before
the
the
hackathon
started,
especially
harder
abstraction
layer
in
rust
and
and
of
course,
the
ambition
was
to
cover
the
very
latest
version
of
edox,
so
the
editors
copy
to
become
version
13
of
the
draft
and
well
by
the
end
of
the
academ.
G
Everything
missing
to
have
something
running
was
actually
completed,
so
the
the
protocol
state
machine
and
all
the
crypto
primitives
necessary
to
process
enoch
messages
basically,
and
this
code
is
now
available
in
the
openws
and
vehicle
github
on
a
dedicated
branch.
G
Next
slide,
please.
So
with
that
say
we
we
were
also
able
to
do
some
testing.
So
malaysia
considered
is
code.
Rascodas,
initiator
role,
run
against
my
code
for
eclipse
californium
as
a
responder,
again,
both
aligned
with
the
very
latest
editors
copy
of
the
specification
and
again
we
tested
the
configuration
intended
for
a
minimal
pair
of
endpoints
and
the
result
was
fortunately,
as
expected.
G
G
G
Yeah
we
are
on
the
next
steps.
There
are
a
bunch
of
few
more
implementations
that
are
under
currently
update
to
catch
up
with
the
latest
version
of
the
specifications,
so
we
expect
especially
those
implementations
and
more
to
run
more
tests
in
the
near
future.
I
think
it'd
be
good
also
to
yeah
cover
a
bit
more
of
the
traces
and
possibly
the
use
of
message,
four
and
of
some
error
messages
out
of
the
addoc
exchange
as
a
possible
additional
site
testing.
G
If
anyone
is
interested
as
a
separate
documenting
core
related
to
edoc
that
purposes,
if
you
want
an
optimization
to
combine
in
a
single
request
on
the
wire,
the
final
adopt
message:
three
with
the
first
oscar
protected
request
in
case
I
have
that
implemented.
So
I'd
be
happy
to
interrupt
that
little
extension
too,
and
that
should
be
it.
A
Thank
you,
marco,
so
just
for
clarification.
This
is
so.
We
now
have
nine
independent
implementations
available
of
ad
hoc,
which
includes
both
constrained
for
embedded
systems
and
for
non-constrained
systems.
So
I
think
that
that
is
important
to
stress
out
and
thank
you
for
running
for
championing
this
hackathon
activity.
Thank
you.
A
A
H
Okay,
thank
you
yeah.
H
So
today,
I'm
here
to
talk
about
a
little
bit
about
our
experience
with
implementing
and
using
ad
hoc
in
highly
controlled
environments,
so
just
to
go
through
a
bit
the
agenda
first,
going
to
go
through
a
bit
about
the
context
and
the
use
case
that
motivated
us
motivated
us
to
work
with
others
and
our
process
in
writing
this
network
implementation
and
and
using
it,
and
so
it
was
a
bit
about
first
looking
at
what
was
available,
what
we
could
use,
what
we
needed
to
implement
and
then
take
a
look
at
a
bit
of
some
benchmarks
and
the
lessons
learned
during
this
process,
and
so
our
contact
was
this.
H
Cyber
security
research
project
at
india
called
rio
tfp,
where
one
of
the
research
access
was
around
next
network
security,
and
so
the
some
of
the
use
cases
that
we
were
looking
into
there
made
lake
and
nether
really
really
relevant
for
us,
and
so
that's
how
some
of
some
of
the
people
in
our
teams
were
involved
in
the
working
group.
H
And
one
of
these
use
cases
we
had
in
mind
was:
we
are
looking
for
completely
different
research
projects
and
to
privacy,
concerns
around
contact
pricing,
and
we
have
these
this
use
case
where
we
had
a
couple
of
contractuation
devices,
which
were
an
f52
ple
devices
which
were
communicating
with
a
backend
server
over
an
untrusted
ipv6
over
ble-link,
and
so
we
were
using
ad
hoc
here
to
establishing
a
security
context
or
communication
channel
between
the
the
contact
pricing
server
and
the
devices.
H
So
we're
performing
a
king
key
exchange
between
these
two
and
so
just
to
set
a
bit
of
context.
Our
goal
here
was
to
write
a
generic
implementation
of
ad
hoc
that
would
be
able
to
run
on
a
different
series
of
microcontrollers
with
quad
core
resources,
so
we're
targeting
non-memory
allocation.
H
We're
not
planning
to
depend
on
hardware
acceleration,
so
most
of
the
things
we're
going
to
see
in
the
presentation
are
all
software
only.
We
wanted
to
support
all
authentications,
and
this
was
at
the
time
of
drop
05
a
little
bit.
So
we
wanted
to
target
cyprus
one
to
four
which
at
the
time
were
mostly
p.
Five,
one
six
of
p,
two,
five,
six
or
c
two
five,
four
one:
nine
signatures,
library,
for
example.
There
was
no
afterwards
and
no
the
all
the
application.
H
Encryption
algorithm
were
all
iscm,
so
there
was
no
chat
at
that
time,
for
example,
and
we
we
also
wanted
to
focus
just
on
writing
networks.
So
we
didn't
want
to
write
the
crypto
libraries
ourselves.
We
didn't
want
to
write
simple
libraries,
ourselves
or
cozy
libraries.
We
want
to
reuse
as
much
as
as
much
as
was
possible,
not
too
much
as
many
libraries
that
would
most
likely
be
used
for
our
own
applications
as
well.
To
avoid
call
duplication
in
the
end.
We
wanted
to
run
it
all
on
a
series
and
variety
of
microcontrollers.
H
So,
while
the
just
to
reiterate
it
was
on
draft
of
five,
and
so
all
the
building
blocks
are
pretty
evident
or
it
was
we
needed
something
to
seaboard
something
for
crypto
or
key
generation
timing,
etc.
We
also
needed
some
interrupt
interrupt
variability
infrastructure
in
the
sense
of
test,
vector
and
interability
interoperability
peers.
H
When
we
look
at
the
crypto
backend,
there
was
there's
a
lot.
This
in
no
means
an
exhaustive
list,
but
this
was
kind
of
crypto
libraries
that
for
our
previous
work
we
already
had
somehow
integrated.
H
So
we
knew
we
could
use,
and
the
main
part
here
is
that,
like
a
few
libraries
were
doing
everything
we
needed
the
ones
that
were
like
well
necessary
or
heckle,
we're
not
doing
it
in
an
embedded
friendly
way
or
did
not
provide
an
incremental
api
or
other
reason
that
made
it
not
the
best
choice
and
the
other
ones
were
not
doing
everything
we
needed.
So
this
was
our
first
point
to
telling
us
that
okay,
we're
gonna,
need
to
actually
support,
probably
multiple
crypto
backends
and
might
want
to
switch
among
them.
H
And
if
you
look
at
this
is
just
a
table
that
summarizing
some
some
stats
on
signing,
but
it
already
tells
us
that,
like
when
you
go
looking
for
some
crypto
library,
it's
all
it's
all
gonna
be
about
trade-offs.
There's
none
that
does
everything
perfect
and
if
you're
gonna
want
speed,
you
might
be
sacrificing
some
flash
and
stack
and,
depending
on
your
use
case,
you
might
be
okay
with
sacrificing
a
couple
of
kilobytes
in
ram
to
get
more
speed
and,
and
others
that's
just
going
to
be,
not
possible.
H
So
we
have
this
interesting
noise
that
we're
going
to
have
to
use
multiple,
crypto
icons
and
probably
abstract
them
for
our
own
application,
and
then
we
needed
something
to
put
it
all
together
and
so,
for
example,
there
was
a
lot
of
options
up
there
like
riot
zephyr,
embed
os,
my
new
etc.
We
went
with
riot
because
we
from
our
side
work.
H
We
knew
it
very
well,
and
so
we
knew
what
kind
of
package
of
support
it
has
and
how
we
could
use
it,
and
they
also
some
stuff
that
we
identified
pretty
early
that
or
during
the
process
that
we're
missing.
So,
for
example,
we
would
have
liked
to
use
cozy
abstraction
ourselves
to
avoid
then
having
code
duplication
in
our
application
side.
But
sadly,
at
the
time
there
were
actually
no
library.
We
could
find
that
we
could
use,
because
there
weren't
really
any
any
match
between
all
the
back
ends.
H
It
was
supporting
and
the
cypher
suits
at
the
time.
So,
sadly,
we
had
to
write
our
own
cozy
function,
but
at
the
end
that
had
some
side
effects
on
on
the
full
application,
and
also,
although
this
cozy
abstraction
of
having
a
cozy
library,
that's
basically
doing
the
abstraction
of
the
all
the
crypto
libraries
underneath
for
us
and
providing
more
clean
interface
to
all
of
that
was
nice.
We
still
realized.
We
were
gonna
need
some
direct
access
to
crypto
for
generating
keys,
hashes,
etc.
H
So
we
couldn't
really
get
a
way
of
going
completely
around
it
on
the
test
vector
side
at
the
time
it
was
somewhat
limited.
We
didn't
have
like
cyborg
certificates
and
the
certificates
we
had
were
not
real
certificates
like
we
tried
to
parse
them,
for
example,
for
with
an
embed,
tls,
x509
library.
We
will
get
errors
because
we
want
some
fields
that
we're
missing
and.
A
H
The
in
the
template-
okay,
that's
it,
and
and
on
the
interrupt
side
of
the
time
there
was
not
that
too
much
that
we
could
use
so
or
not
that
we
were
at
the
time
everyone
was
starting
to
develop
at
them,
so
we
didn't
have
too
much
there,
and
so
this
is
what
we
the
the
end
result.
Was
we
had
this
c
implementation
of
head
hook
called
ad
hoc
c,
there's
the
link
on
at
the
bottom,
and
we
we
use
nano
sieber.
H
Then
our
default
backend
was
time
equipped
for
all
the
piece,
notification
and
hashing
and
for
signature
we're
using
an
sdh
we're
mostly
using
the
c5119
implementation
from
daniel
beer
and
for
interpretability
well,
timothy.
That
was
working
with
us
wrote
by
head
of
edda,
which
was
quite
useful
for
us
for
testing
all
the
time,
because,
as
I
tried
to
emphasize
a
bit
at
the
start,
part
of
the
challenge
was
actually
putting
all
these
crypto
blocks
together
and
assembling
them.
H
And
on
the
python
side
there
was
a
non-issue,
so
we
could
easily
cover
most
of
the
cryptosuits
methods
and
parts
we
also
part
certificates
generate
certificates.
Much
easier
to
be
then
be
able
to
test
this
implementation
and,
as
I
said,
we
chose
right
and
just
some
some
now,
I'm
gonna
go
into
some
benchmarks,
some
stats
of
like
what
what
the
result
is,
and
so
rom
was
around
10k
9k
and
ram.
We
realized
was
actually
changing
a
lot
depending
on
the
method
we
were
using.
H
So
there's
there's
two
tables
here:
one
one
is
on
meth
of
zero,
so
sign
sign
and
three
is
static.
Dp
element
on
both
sides
and
two
different
colors
are
two
configurations,
because
we
also
realize
that
well,
since
we're
trying
to
not
do
dynamic
allocation,
we
have
static
buffers
everywhere
and
and
since
in
the
different
cryptographic
stages,
you
are
using
previous
information
as
cryptographic
material,
the
amount
of
size
you
are
locating
for
additional
data
or
for
credentials
for
credential
id
and
ends
up
being
more
buffer
space.
H
You
also
need
to
allocate
for
the
eventual
transcript,
etc
and
so
tuning.
These
parameters
like,
for
example,
just
allowing
for
one
byte
in
one
by
credential
ideal,
whatever
connect,
can
actually
have
quite,
could
have
quite
some
impact
on
the
actual
stack
usage
of
the
different
message
generation
and
parsing
functions,
but
it
was
roughly
around
4k
in
the
in
the
worst
case,
with
these
default
configurations.
But
again
it
was
very
influenced
by
the
size
of
the
allowed,
the
maximum
load
size
of
the
credentials,
the
credentials
id
additional
data.
H
When
you
look
at
the
timing
that
takes
actually
computer
handshake,
this
is
again
no
harder
acceleration.
We
run
some
measurements
where
we're
just
doing
taking
two
notes.
Doing
some
handshakes
either
either
over
the
wire
over
15.4
or
ble,
or
everything
through
co-op
and
our
worst
case
scenarios
or
maybe
were
with
a
signature
very
sign,
sign
metal,
zero,
where
between
two
cortex
and
zero
is
taking
up
around
20
seconds.
Well,
the
best
scenario
is
probably
with
an
m4
where
it
was
taking
around
six
to
seven
seconds
when
doing
a
static,
difficult
authentication
meeting.
H
But
if
we
try
to
take
a
bit
of
a
closer
look
to
understand
why
it's
taking
so
long,
it's
actually
most
of
it
is
related
to
crypto
and
if
there's
a
paper
that
I'm
referencing
at
the
bottom,
which
were
stuttering,
the
the
sign
of
verified
times
that
for
ed25519
and
we
can
see,
is
basically
the
overhead
is
coming
from
there.
For.
H
If
you
look
at
on
an
m4,
for
example,
verifying
a
signature
of
32
bytes
takes
around
two
seconds
and
800
milliseconds
to
to
sign
it,
and
so
we're
doing
this
twice
in
the
process.
And
so
we
have
like
a
baseline
of
six
seconds
just
from
the
signing
verifying.
H
But
again
this
just
one
library,
as
I
was
trying
to
put
in
context
first,
you
can
also
speed
it
up
by
changing
the
library,
but
maybe
you're,
sacrificing
more
ram
or
more
fresh
usage
than
your
implementation
is
gonna
use,
yeah,
and
so
this
is
a
little
bit
of
some
numbers
and
then
we
try
to
integrate
it
all
into
our
application,
and
we
have
a
couple
of
things
that
we
then
realize
in
the
field
that
sure
initially
we
we
decided
just
to
write
our
own
cosi
function,
because
it's
pretty
simple
code
but
at
the
end
we
under
have
ended
up
using
cosy
libraries
in
our
application
code,
which
end
up
ended
up
having
some
redundancy
so
yeah.
H
No,
I
don't
I
didn't
we
so
the
end
result
we
have
so
far
is
that
we
didn't
support.
We
only
supported
at
the
time
cypher
stood
zero
and
one.
So
there
was
no
p
two
five
six,
but
I
do
have
a
table
somewhere
where
I'm
comparing
them.
But
I
didn't
do
the
hog
enough.
I
can
I'll
locate
up.
Let
me
see
I'll
finish
and
then
I'll
try
to
look
it
up,
but
it's
in
the
same
paper
that
there's
the
comparison
as
well
for
p256
that
I'm
referencing
in
slides,
15
or
14.
H
yeah,
and
so
we
also
realized
okay,
a
reaction.
Api,
like
the
one
embed
tls
was
providing,
would
have
actually
been
quite
useful
in
most
of
these
cases,
because
the
amount
of
time
it
was
taken
to
verify
or
signatures
or
signing
verifying
was
actually
going
over
the
default
timeouts
we
had
in
for
our
application.
So
we
had
to
do
some
special
handling
for
that,
and
all
of
this
could
have
maybe
been
prevented
with
the
re-engine
api
and
then
just
some
feedback
to
focus
on
the
on
the
implementing
the
draft
itself.
H
So
again,
this
was
just
drop
five
at
the
time
it
was
quite
confusing
for
timothy
who
was
developing
this,
who
had
the
responsibilities
of
passing
credentials,
how
it
should
be
purged
since
from
the
ad
hoc
side,
what
how
was
it
supposed
to
receive
the
credentials
information?
H
This
buy
string,
identifier
that
was
trying
to
save
this
one
byte
from
its
point
of
view,
seemed
to
not
be
worth
the
extra
code
completely
that
I
was
actually
introducing
and
well
now
it's
been
dropped.
Since
seven,
I
think
we
got
some
insights
on
how
we
could
like
also
to
go
ram
to
get
the
best
out
of
it.
There's
probably
some
stuff.
H
We
could
have
optimized
and
maybe
have
some
work
buffers,
because
most
of
the
rams
that
come
from
static
buffers
that
are
allocated
for
the
key
streams,
the
cozy
keys
and
stuff
like
that,
and
then,
even
though
we
used
cipher
should
0
at
the
time
it
was
mostly
because
what
we
had
available,
we
would
probably
do
cipher
two
or
three,
but
we
could
also,
if
we
didn't
have
something
in
our
application
that
was
already
using
iscm.
H
We
might
use
cypher
suits
fund
because,
at
least
in
rio,
chacha
poly
is
smaller
in
size,
the
accm
it's
simpler
in
this
business
in
its
implementation
and
and
it's
as
well
easier
to
implement
within
incremental
api,
which
translates
roughly
into
less
ram
space.
That
is
needed
because
you
don't
have
to
serialize
the
same
information
twice
in
memory
while
parsing
and
that
is
it
I'll.
Try
to
look
up
the
table
for
the
paper
where
the
there's
the
comparison
for
d4,
pe256
and
ct5019.
H
I
Am
I
in
the
queue?
Yes,
you
can
hear
me
now.
Oh
good.
Yes,
on
page
eight,
I
just
had
a
question
about
the
comparison
between
the
the
different
cipher
suites.
Am
I
to
read
this
correctly
saying
that
you
don't
believe
that
embed
tls
supports
aes
gcm.
J
A
Okay,
so
thank
you
francisco.
I
think
that
is
a
good
overview
of
at
least
of
the
that
gives
us
an
insight
into
the
performance
of
the
of
the
protocol
when
it
is
fully
implemented
in
software
when
the
crypt
is
fully
implemented
in
software.
Those
numbers
are
indeed
quite
large
but,
as
you
said,
they
are
allocated
to
to
crypto.
A
A
E
K
K
Why
I
actually
been
introduced
to
this
challenge
is
that
the
company
I
work
for
is
built
upon
number
of
of
companies
and
divisions,
and
the
idea
was
that
every
of
these
divisions
are
building
the
stack
of
their
own
and
and
just
to
unify
that
I've
been
introduced
to
the
to
the
challenge,
to
find
a
stack
that
can
be
then
shared
across
multiple,
multiple
companies
and
multiple
divisions,
and
it's
just
because
it's
it's
the
numbers
and
the
scenarios
that
are
so
large.
K
It's
been,
it's
been
a
hard
challenge
and
if
we
can
go
to
the
next
one,
please
so
the
yeah.
So
the
challenge
I
like
we
got
introducing
was
to
to
find
a
good
modular
iot
stack
that
can
run
on
the
embedded
platforms,
also
mobile
and
the
cloud
and
yeah
one
of
the
the
key
challenges
and
something
that
we
wanted
to
enable
is
to
device
to
cloud
device
to
mobile
and
also
other
way
around
and
device
to
device.
K
Secure,
end-to-end
communication,
where
we
can
go
over
multiple
hops,
with
different
middle
boxes
and
not
and
just
keep
that
do
not
break
that
end-to-end
security.
Just
keep
it
all
the
way
down
so
and
and
to
have
all
of
that
implemented
in
the
application
layer.
So
we
would
not
have
to
rely
on
on
something
within
the
the
lower
layers
and
we
wanted
to
work
with
the
formats
around
the
identity
like
x,
509
certificates
or
maybe
using
cvts
or
jvts,
and
then
all
of
it
to
be
backed
by
standards.
K
So
we
can
maintain
security
more
efficiently.
So
we
don't
have
to
keep
evaluating
and
and
just
be,
the
only
paradise.
Looking
at
the
issue-
and
you
know
we
wanted
to
achieve
that
with
the
with
the
open
source
as
well,
and
if
we
can
go
to
the
next
one
please
so
the
areas
that
I
was
looking
at
and
we
were
looking
at
was-
was
more
complex
than
just
the
communication,
so
we
had
to
look
on
the
provisioning
so
like
the
generic
iot
stack,
the
provisioning
devices
with
identities
etc.
K
The
communication,
which
is
something
I
will
focus
on
today,
and
the
operations
like
firmware,
updates,
etc.
Next,
one
please
right.
So
the
solution
we
have
we
have
been
evaluating
and
we
have
been
using
so
far,
was
based
upon
co-op,
oscar
erock
we
use
for
identities.
We
primarily
focus
on
the
x,
509
certificates
and,
more
so
just
to
give
you
a
little
bit
of
details
on
the
edoc.
K
Oscor,
like
I
said,
for
the
key
exchange,
we
focus
on
using
error
and
then
we
treat
everything
was
backed
by
the
by
the
co-op
and
then
on
the
transport
layer
we
wanted
to
like.
I
said
we
wanted
to
run
on
the
application
layer,
so
we
wanted
to
stay
a
little
bit
independent
from
the
transport,
so
we
escaped
going
on
the
ip
networks
only
so
we
wanted
to
use
the
stack
in
the
mobile
phone
like
device
to
mobile
phone
and
mobile
phone
to
device
examples.
K
K
We
use
usbl,
let's
say
on
the
we
wanted
to
keep
like
rx
and
tx
pipe
on
on
every
protocol,
that
that
would
support
that.
So
on
the
ble
side,
we
didn't
have
any
good
use
case
and
we
didn't
have
any
good
example,
maybe
on
using
on
how
to
use
the
the
co-op
over
ble.
So
we
went
down
with
leveraging
uart
protocol
on
over
ble,
so
one
characteristics
for
read
and
one
characteristics
were
right.
K
I
can
go
to
the
next
one
and
then
on
the
yeah.
Just
looking
on
this
one
across
the
different
platforms
we
could
we
could
have,
or
we
did
replicate
that
the
whole
stack
over
multiple
over
multiple
areas.
So
on
the
embedded
we
we
could
have
achieved
the
same
stack
and
then
on
the
tooling
side,
like
the
cli
tools,
mobile
sdks.
We
also
completed
to
do
that
for
the
cloud
as
well
and
as
you
can
see,
we
just
have
a
little
bit
different
on
the
on
the
transport
back
ends.
K
So,
for
example,
in
the
cloud
we
also
wanted
to
see
if
we
can
fit
that
feed
that
use
case
into
existing
solutions.
So
we
we
use
the
message
broker
when
in
our
case
was
mqtt.
We
wanted
to
prove
that
the
communication
can
run
over
like
just
any
any
transport.
So
I
know
maybe
it's
not
ideal,
but
we
run
it
over
mqtt.
K
So
we
had
the
co-op
running
over
mktt
just
to
see
how
well
it
can
fit
into
the
existing
ecosystem,
but
and
and
and
just
having
all
the
security
and
the
logic
within
the
application
layer.
Next
one
please
right
so
just
focusing
on
the
adult
libraries
in
the
previous
presentation.
There
were
a
few
technologies
mentioned,
which
I
didn't
put
in
here,
but
but
I
I
might
as
well
talk
about
it.
K
So
we
wanted
to
keep
the
tech
the
the
code
stack
to
the
minimum
and
to
not
have
like
six
or
seven
different
or
five
different,
ad
doc,
implementations
and
oscars.
So
we
went
with
this
architecture
so
for
the
embedded
part
for
the
ios
and
for
the
node.js
which
we
use
for
tooling,
we
went
with
the
single
c
library
that
is
microscope
micro,
adopt
library.
K
So,
each
of
them,
each
of
these
three
free
components
like
on
the
embedded,
ios
and
node.js,
are
just
the
wrappers
or
just
wrapping
the
native
c
library.
So
on
the
node.js
we
have
a
native
module
on
ios
we're
wrapping
the
c
component
with
objective
c
and
then
using
in
swift
and
then
on
embedded.
We
just
use
micro,
oscar
micro
directly
and
yes,
we
have
as
a
back-end.
K
We
have
used
embed
tls,
which
I
can
confirm
on
the
on
the
previous
note
on
the
aes
that
it
worked,
but
we
use
embed
tls
on
on
nrf
on
the
embedded
part.
We
use
embed
tls
version
from
nordic
semiconductor.
That
is
hardware
accelerated
version.
So
we
got
the
full
hardware
acceleration
on
that
which
are
some
numbers
I'm
going
to
talk
about
in
a
sec
and
then
for
android
and
cloud.
K
We
have
our
own
add-on
implementation
that
for
now
we
keep
internal,
but
that
might
change
in
the
future
and
just
on
the
top,
you
can
see
that
we
try
to
keep
these
apis
very
easy
to
use
and
and
just
with
the
minimum
input
from
the
user
next
one
right.
So,
just
to
give
you
some
details
on
our
add-on
use
case
we
are
focusing
just
for
now.
We
are
just
focusing
on
on
adult
usage
with
the
certificates
and
then
so.
K
We
have
cas
on
both
ends,
so
we
have
a
responder
root
certificate
on
the
initiator
side,
an
initiator
root
certificate
on
the
responder
side
and
then
for
the
for
the
credentials.
We
use
full
x509
certificate,
which
we
then
validate.
So
we
go
with
our
certificates,
use
p256
curve.
So
we
go
to
the
with
the
method:
zero
with
signatures
and
suit
number
two
right.
Okay,
so
just
on
the
embedded
platform
like
I
mentioned,
we
use
nrf52840
with
the
freertos.
K
That's
a
maybe
not
not
not
a
main
or
master
three-artist
version,
but
we
have
our
own
modified
version
a
little
bit
for
the
co-op
we
use
lobaro,
co-op
library
and
then
microscope
micro,
edc
and
then
for
crypto.
We
use
embed
tls.
That
is
hardware
backed,
and
we
have
that
platform
that
you
can
see
here,
but
all
in
all,
we
just
as
the
main
we're
running
this
on
the
standard,
nrf
50
to
840
dev
kit.
K
So
we
have
our
own
dongle
firmware
like
a
zephyr
dongle
zephyr,
firmer
dongle,
as
acting
as
a
ble
as
a
bli
donku
that
that
is
running
over
uart,
so
node.js
tools
over
on
over
standard
hci
command
will
communicate
with
that
board
and
then
we'll
in
the
node.js
library.
We
have
like
full
ble
api
to
back
it
up.
It's
actually
based
on
the
open
source,
noble
library
and
then
this
screenshot
shows
a
node.js2
being
an
initiator
communicating
with
the
responder
that
is
running
on
rf
52840,
with
our
rpc
protocol.
K
On
top
of
it,
and
as
you
can
see
like
we
do,
what
we
do
here
is
we
do
scan
for
ble.
We
connect,
we
discover
gut,
we
perform
the
addoc,
like
I
said,
with
the
credentials
using
certificates
on
both
ends
with
the
method,
zero
and
suit
number
two,
and
then
on
top
of
that
we
do
oscor,
and
then
we
set
up
our
own
rpc
command
and
then
all
of
that
is
taking
less
than
a
second.
A
Just
just
for
my
understanding
and
the
clarification
of
595
milliseconds,
what
does
it
refer
to.
K
Okay,
so
that's
the
first
number,
so
the
first
number
is
where
we,
where
we
con
connected
over
scanned,
the
ble
connected
over
ble,
discovered,
got
and
sent
message.
One.
D
Maybe
maybe
melissa
michael
richardson
here,
maybe
melissa,
just
asked
the
same
question
and
I
didn't
understand
the
question
the
same
way.
So
bluetooth
has
a
encryption
layer
and
gat
avoids
it
or
yes,
okay,
so
so
you're
going
clear,
your
your
ad
hoc
messages
would
in
sense
be
in
clear
over
bluetooth.
A
A
K
For
800
something,
but
for
the
screenshot
wise,
I
I
choose
the
700
milliseconds,
but
yeah
roughly,
we
always
stay
around
seven
800
milliseconds
so,
but
and
that's
important
to
know
that
this
is
there
is
also
you
are
delay,
because
the
bridge
is
communicating
over.
The
ble
bridge
is
also
running
over
uart.
So
there's
always
going
to
be
a
few
milliseconds
here
and
there
of
the
delay
next.
B
K
So
it's
exactly
the
same
process
so,
like
I
described
before
so
scanning,
connecting
discover,
got
certificate,
exchange
with
the
certificate
validation
and
what
we
validate
for
is
just
so
you
know
we
validate
for
the
we
validate
against
the
root
certificate,
and
then
we
validate
the
expiration
time.
That's
the
for
now!
That's
the
the
only
certificate
validation
that
we
do
and
then
on
the
mobile
side,
we
did
avoiding
this
uart
part
like
with
the
tooling
site.
We
get
a
resource
in
600,
700
millisecond
range
next,
one
please
right
so
for
the
future.
K
For
now,
we
would
really
focus
on.
We
want
to
build
now
a
co-op
http
to
call
a
proxy
for
our
cloud
infrastructure.
That's
also
gonna
be
backed
and
working
with
the
adult
and
oscar,
and
we
can
try
to
stay
as
much
as
compliant
to
the
to
the
co-op
http
proxy
specs.
K
We
have
some
things
that
we
are
not
sure
yet,
but
with
that,
with
those
things
we
hopefully
can
contribute
back
to
the
specs
and
also
the
open
source,
which
we
already
do.
For
example,
for
the
microscope,
micro
reduce
library,
we
have
been
working
first
with
the
front
offer
and
then,
with
the
author
stefan
now
to
to
also
be
included
as
a
as
the
collaborators
on
the
on
the
on
the
c
library.
A
K
So
yes,
so
we
work,
we
we
work
with.
Stefan
on
that
as
well
and
then
more
on
the
personal
activity.
I
was
working
with
goran
on
the
on
the
latest
test,
vectors
for
the
traces
and
and
my
contribution,
that's
going
to
be
that
hopefully.
K
A
A
A
So
yes,
but
before
we
go
to
the
next
presenter,
I
would
just
like
to
bring
the
comment
by
francisco
to
the
mic,
where
he
confirmed
that
on
the
slide
set
of
developer
feedback
number
one.
There
was
a
mistake
in
the
embed
tls
column,
where
all
the
all
the
rows
should
have
been
tracked,
including
the
asccm
primitive,
which
was
shown
as
not
supported.
So
francisco
confirms
that
this
was
discussed
in
the
chat.
A
A
H
H
It
I
didn't
quite
capture
that
maybe,
if
you
can
release
it,
sorry
there's
in
the
in
the
in
the
table.
I
had
like
some
checks
with
some
from
with
an
asterisk
and
those
means
that
it's
not
in
the
master
branch,
but
you
can
there's
pr
or
somewhere
that's
implemented.
Then
you
can
use
it
and
for
e25519.
B
A
A
A
So,
to
give
you
some
context
about
this
presentation,
as
you
know,
as
we
all
know
at
ho,
so
as
we
all
know,
lake
as
a
working
group
targets,
constrained
environments
and
constrained
environments
in
our
context
mean
embedded
systems.
So
many
of
our
implementations
will
be
executed
on
embedded
systems
and
you're.
Probably
all
aware
that
the
embedded
programming
languages
today
is
dominantly
c
and
c
is
memory
unsafe
and
c
doesn't
play
well
with
security.
A
So
what
we
standardize
here
is
obviously
crucial
to
security
of
the
protocol,
but
what
what
ends
up
in
the
wild
is
as
important
and
the
protocol
in
the
wild
will
be
as
secure
as
its
implementation
is.
So
the
goal
of
the
work
we've
done
was
to
produce
an
implementation
that
has
some
security
properties,
such
as
provable
correctness
of
the
implementation,
with
respect
to
a
given
model,
provable
memory,
safety
and
side
channel
resistance
to
considering
the
threat
model
where
the
the
device
itself
is
not
completely
trusted.
A
So
a
team
from
india
in
paris
called
prosecco
developed
a
framework
called
hackspec.
That
is
a
a
framework
for
verification
of
different
implementations
that
essentially
for
the
generation
of
verified,
implementations
and
next
slide.
Please,
this
framework
is
called
hackspec.
A
So
the
it's
called
hackspec
and
the
specification
language
is
a
subset
of
rust.
So
what
that
means
is
that
when
you
write
your
model,
your
specification,
you
are
essentially
writing
rust
code
and
when,
since
you
are,
writing
the
rust
code,
this
means
that
what
you
write
the
model,
the
formal
verification
model-
is
no
longer
some
mathematical
abstraction
of
the
protocol.
A
It
is
executable
code
and
this
specification
enables
the
generation
of
verified
implementations,
which
means
that
it
is
possible
to
generate
a
formally
vetted
implementation,
satisfying
those
security
properties
from
this
model,
and
this
pro,
this
team
from
india
has
developed
a
complete
framework
to
type
check
this
rust
specification
and
to
enable
its
compilation
onto
different
mathematical,
abstraction,
abstracting
languages
such
as
f
star,
and
essentially
it
can
be
also
executable.
A
So,
in
practice,
what
that
means
is
that
to
to
arrive
at
at
an
implementation
that
is
formally
vetted.
We
need
to
write
some
implement
some
code
in
rust
in
a
subset
of
rust,
called
hackspec
and
then
by
using
their
framework
to
generate
the
to
generate
the
f
star
model,
which
is
this
mathematical
of
mathematically
abstracted
language
of
the
protocol
that
allows
the
the
verification
of
different
properties
of
the
protocol
against
the
model.
A
A
What
is
necessary
is
to
write
and
to
write
and
verify
the
implementation
in
another
language
called
low
star
against
this
f
star
model
that
was
generated
automatically
and
from
there
on
there
is
automatic
set
of
tools
to
compile
the
slow
star
code
to
verified
c
or
verified
rust
code,
satisfying
those
properties
that
we
wanted
to
prove
from
the
very
beginning.
So
you
can
see
this
kind
of
flow
on
the
right
and
I'm
trying
kind
of
to
abstract
it.
A
For
you,
and
I'm
focusing
mainly
personally
on
step
number
one
where
we
are
implementing
this
specification,
that
is
the
model
that
is
going
to
be
compiled
to
the
f-star
f-star
model.
Next
slide.
Please.
A
So
for
in
my
mind,
that
means
minimal
implementation,
minimal,
very
lightweight
implementation
of
the
protocol,
where
we
are
not
pulling
in
a
bunch
of
different
libraries
and
dependencies,
and
we
are
keeping
the
memory
footprint
and
the
the
code
footprint
to
its
minimum.
A
As
we've
seen
from
the
previous
presentations
software
execution
of
different
cryptographic,
libraries
takes
a
lot
of
time
and
we've
seen
from
francisco's
presentation
that
it
can
take
up
to
like
50
or
10
to
15
seconds,
to
complete
the
hand
track
due
to
the
crypto
to
the
execution
of
crypto
on
different
microcontrollers.
A
In
software,
we
want
to
rely
on
hardware
accelerated
crypto,
so
our
initial
compilation
targets
are
essentially
native
to
facilitate
development,
but
then
also
cc2538
board
from
texas
instruments
and
this
nordic
chip
that
both
support
acceleration
of
the
different
ad-hoc,
cipher
suites
next
slide
is
so.
We
encountered
a
couple
of
challenges
on
this
path
and
the
main
one
is
that
we
said
we
want
a
verifiable
implementation.
A
Second
point,
which
is
kind
of
a
feedback
for
the
well,
not
not
really
a
feedback.
But
it's
mostly
a
point
to
to
be
aware
of
is
that
during
the
this
work
of
implementing
the
protocol,
majority
of
my
time
was
spent
on
figuring
out
the
the
su,
not
the
support,
but
getting
around
the
the
the
point
compression
not
being
supported
in
the
libraries
point
compression,
meaning
that
the
elliptic
curves.
The
point
in
an
elliptic
curve
is
typically
represented.
With
x
and
y
coordinates
in
a
compact
representation.
A
You
will
transfer
as
we
use
in
ad
hoc.
We
transfer
only
the
x,
coordinate
and
you're
supposed
on
the
constrained
device
or
in
the
implementation
to
calculate
the
y
coordinate
on
the
fly,
and
this
is
poorly
supported
with
the
existing
libraries,
including
the
one
that
huxpeck
uses.
So
a
lot
of
my
time
during
the
implementation
implementation
actually
was
spent
on
that
and
finally,
in
rust,
since
trust
is,
there
is
an
ongoing
initiative
on
porting
rust
to
the
different
different
popular
hardware
embedded
systems.
A
A
So
the
current
status
of
the
implementation
is
that
we
progressed
this
during
the
hackathon.
Quite
a
bit,
we
came
into
the
hackathon
as
marco
outlined,
with
a
minimal
implementation
that
passes
the
test,
vectors,
different
essential
unit
functions,
and
we
came
out
with
the
fully
fledged
minimal
implementation
that
interoperates
with
the
java
based
back
end
that
that
was
used
for
interrupt
testing.
So
this
minimal
implementation
means
the
initiator
in
static
static
mode
with
ccs
and
with
integer
kits
essentially
instantiating.
A
The
45
byte
handshake,
45
byte
message.
Two
of
the
adhoc
handshake,
and
what
is
important
here
to
outline
is
that
the
implementation
essentially
uses
zero
external
libraries.
All
the
seabor
and
cosy
encoding
are
done
inline
and
it's
completely
no
std
style
developed.
So
the
as
I
said,
the
status
is
that
the
implementation
passes
the
test
vectors
on
a
native
machine
for
now
successfully
interrupt
with
with
the
california
medha,
and
we
are
currently
working
on
the
build
support
for
different
boards
that
I
outlined
next
slide.
Please.
A
So
we
have
a
couple
of
open
questions
that
we
want
to
bring
up
and
discuss
with
the
formal
analysis
community,
and
this
is
mainly
related.
How
can
we
ensure
that
this
model
that
we
write
is
really
bound
to
the
specification,
because
this
is
the
the
one
big
assumption
that
the
academic
community
makes
when
doing
when
modeling
the
protocol
and
when
verifying
the
implementations
so
essentially
they're
making
the
assumption
that
the
model-
so
in
this
case,
this
rust
code?
That
we
write
is
a
perfect
or,
I
would
say,
ideal
representation
of
the
rfc.
A
A
The
next
steps
are
essentially
to
complete
the
port
to
these
two
boards
and
to
publish
this
as
an
as
a
crate
on
crates,
dot
io
to
be
available
to
the
people
in
open
source,
and
once
that
is
done,
we
have
our
formal
model
that
we
need
to
use
to
formally
prove
the
verif
to
generate
formally
vetted
code
that
can
be
executable
on
a
microcontroller.
A
A
Okay,
with
that,
I
propose
we
go
with
the
next
agenda
item
and
this
is
the
computational
analysis
of
the
ad
hoc
protocol
and
baptist.
Can
you
hear
us.
K
M
So
in
computational
security
we
consider
the
messages
as
bit
strings
rather
than
terms
and
the
primitive
are
simply
functions
on
bits
and
bit
strings
in
the
computational
model.
M
We
we
have
to
prove
that
anata
cannot
distinguish
between
a
secret
key
and
random
value.
M
M
In
the
summer,
so
you
have
need
to
use
a
64-bit
security,
mac
and
128-bit
security,
electric
curves
defiant
and
so
there's.
A
A
qualification
about
this
sorry
for
interrupting
you,
so
just
as
a
clarification.
So
this
is
one
particular
mode
of
ad
hoc
and
static
static
and
obviously
the
most
constrained
setting
the
cipher
suite
zero
and
two
which
use
the
eight
byte
max.
M
M
So
with
t
the
occasion
time
of
the
protocol
and
epsilon
the
success
probability,
we
have
to
prove
that
t
on
epsilon
is
at
least
greater
than
2
to
the
128..
So
if
we
reach
this
we
can.
We
can
say
that
we
have
a
security
level
of
128
bits,
so
we
have
three
points
to
approve.
So
first
we
have
the
key
privacy.
So
at
most
both
participants
know
the
finalization
key.
So
by
compromising
the
long
term
credential
of
srp
an
attacker
should
not
be
able
to
compute
past
session
keys.
So
this
is
a
forward
security.
M
M
So
for
the
the
key
privacy,
so
that's
also
known
as
implicit
authentication.
It
relies
on
the
computational
development
assumptions
and
therefore
it
depends
on
the
group
side
in
which
we
are
working
and
to
prove
the
key
privacy.
We
will
we'll
use
the
find
then
guess
model
where
we
give
the
adversary
the
access
to
three
records.
M
So
the
first
one
is
the
descent
where
the
attacker
can
model
well,
where
the
send
oracle
models,
an
active
attack
in
in
which
the
editorial
may
intercept
the
message
you
can
modify,
it
create
a
new
one
and
you
can
do
whatever
you
want.
M
M
So
the
idea
here
is
to
that.
We
will
consider
the
the
attacker
that
can
use
as
many
times
the
sand
and
reveal
oracles
when,
when
he
will,
he
will
think
that
he
he
when
we
think
he
can
say
that
the
key
is
either
a
valid
key
or
a
number.
U
he
use
the
test
record
and
then
he
he
wins.
If,
if,
if
it's
guess
is
a
is
the
good
one.
M
So
we
we
use
flags
to
represent
the
the
mutual
authentication.
So
we
have
two
flags,
the
first
flag,
so
most
initialized
eyes
at
zero.
Is
the
flag
accept
so
either
the
initiator
of
the
responder
will
activate,
will
put
the
accept
flag
at
1.
1
am
when
he
has
the
required
material
and
we
have
the
terminate
flag
that
asserts
that
the
the
other
participant
has
the
required
material.
M
So
when
the
the
idea
is
to
prove
that
both
participants
can
activate
the
terminate
flag
with
the
recurrent
security,
and
here
it
relies
on
the
mac
security,
so
I
said
before,
as
we
use
64
bits
mac.
M
So
that's
that's.
There
is
a
that's
there's
a
mistake,
so
64
bits
max
provides
64
bits
security
and,
as
we
want
to
prove
that
the
we
have
a
128
bit
security,
we
are.
We
will
check
so
the
if
the
128-bit
security
is
reached
after
few
messages,
because
the
idea
is.
We
know
that
we
have
a
sync
with
a
simple
execution.
We
will
have
a
64-bit
security,
but
we
want
to
check
if,
after
four
or
six
messages,
so
we
have
other
information
that
will
allow
us
to
guarantee
to
prove
the
mutual
authentication.
M
A
A
Just
as
a
clarification
in
the
requirements
document,
we
have
agreed
upon
the
security
level
of
127
bits
and
we
do
include
eight
byte
max
in
the
in
the
protocol.
So
what
what
this
is
referring
to
is
that
the
128
security
bits
that
they
are
studying?
A
If
I,
if
I
understand
correctly
about
this,
please
correct
me
that
you
are
studying
that
after
a
few
application
messages
that
are
exchanged,
we
can
actually
reach
the
127
bit
security
over
the
given
key.
Even
though
the
macs
that
were
used
to
authenticate
the
handshake
were
only
eight
bytes.
Is
that
correct.
M
M
And
the
third
point
is
the
identity
protection,
so,
by
definition,
we
we
have
the
identity
protection.
If
the
protocol
is
secure
against
active
attackers
for
the
initiator
and
against
passive
attackers
for
for
the
responder
and
how
to
represent
the
security
by
using
games,
so
we
will
give
the
attacker
two
identities
and
an
active
attacker
should
not
be
able
to
say
which
one
is
the
initiator
and
for
the
for
the
responder.
So
also
we
give
two
identities.
M
And
to
conclude,
we
have
the
protocol
decomposition,
so
in
yellow
you
have
the
data
used
for
the
key
privacy,
so
that
are
the
the
difficult
man
defeatment
public
keys
and
mutual
authentication
will
be
other
value
in
with
the
value
in
in
green
and
the
identity
protection
is
ensured
by
the
inclusion.
So
the
idea
is
to
study
so
each
of
these
values
for
the
the
security
concerns
and
prove
or
conclude
that
the
the
security
is
as
expected.
J
Okay,
okay,
can
you
hear
me?
Yes,
we
can
yeah.
Excuse
me
for
for
not
following
us
real
closely,
but
I
believe
what
you're
doing
is
saying:
you'll
exchange
several
messages
using
a
64-bit
mac
and
you're
yours,
and
if
all
those
messages
authenticate,
then
you
hope
to
get
the
full
127-bit
security
level.
Is
that
correct.
B
J
I
don't
believe
gcm
gives
you
that
property,
because
if,
if
the
attacker
finds
the
initial
message
and
manages
to
forge
it,
how
we
perform
the
forgery
will
tell
them
how
to
perform
later
later
forgeries
with
essentially
no
with
with
essentially
no
additional
effort.
So
you
only
get
64-bit
security.
M
I
can't
tell
you
more
because
you
want
to
to
determine
if
yes
or
not,
but
the
idea
is
maybe
to
be
able
to
say
that
do
we
have
the
we
do
not
have
the
security
before
the
attacker
can
forge
a
value.
So
I
don't
know
if
it
answers
your
question.
J
This
is
not
a
question.
This
is
a
comm,
an
observation
based
on
the
security
properties
that
gcm
gives
you.
This
is
specific
gcm,
your
other
authentication,
your
integrity
program,
routines
functions,
do
not
have
the
same
property.
M
So,
yes,
the
idea
is
more
than
we
know
the
we'll
have
64
bit
on
the
forgery.
But
yes,
we
don't
know
how
to
say
that.
J
What
the
attacker
will
have
to
do
is
basically
do
a
correct
guess
on
the
very
first
mackie's
attacking
basically
doing
a
blind
guess.
Actually
you
can
do
a
little
better
than
that,
but
not
much
once
he's
done
that
then,
and
he's
done
that
successfully,
then
he
can
actually
do
later
perform
more
forgeries
for
essentially
for
free.
J
J
Once
he's
done
that
and
and
if
he's
successful,
then
he
can
he,
then
he
he
can
forge
later
messages,
which
means
that
the
security
of
the
later
messages
of
those
macs
does
not
increase
the
security
level.
Therefore,
you're
stuck
at
64
bits.
C
Just
at
the
interest
of
time,
scott
scott
is,
it
is
the
kind
of
attack
you're
mentioning
specific
to
gcm
or
what
it
also
means.
C
Okay,
great
thanks
so
mark
and
and
if
we
could
can
I
move
on
time-wise-
be
great,
so
mark
go
ahead.
C
I
guess
not
okay
in
in
that
case
batiste.
Thank
you.
I
I
guess
you're
wondering
about
time.
Go
ahead.
Yes,.
A
So
marx
has
again
asked
to
send
screen
mark.
Can
you
hear
us
we're
not
getting
audio
so
we'll
have
to
cut
it
here?
Oh
yeah,
we
cannot
hear
you,
we
see
you,
but
we
cannot
hear
you.
E
I
apologize
microphone
problems.
I
just
had
a
question
for
baptist.
Thank
you
for
the
presentation,
so
I'm
from
ethioric,
where
we
have
a
team
also
working
on
the
computational
analysis.
So
this
presentation
is
of
interest
to
us
and
we're
just
wondering
in
your
analysis.
When
you
were
talking
about
ski
secrecy,
what
did
you
define
actually
as
a
session
key
for
the
protocol?
E
M
So
the
final
session
key
is
the
is
the
key
that
the
common
key
that
both
participants
share.
So
that's
the
that's
the
I
don't
know
how
to
say
that.
M
E
Yes,
in
a
sense
yeah,
so
essentially
in
in
as
far
as
we've
been
in
the
analysis,
we're
not
able
to
to
really
clearly
say
is
the
pr
key
considered
as
sort
of
the
final
session
key
or
whether
there
should
actually
be
some
sort
of
final
derivation
as
well
to
actually
extract
what
should
be
the
session
key.
So.
A
Okay,
some,
maybe
the
authors
can
respond
to
that.
If
not,
I
can
also
compliment.
B
Yeah,
I
think
we
should
take
the
next
presentation,
but
yeah
it
should
be
higher.
The
arcade
correct.
We
have
more
derivation.
N
N
I
can,
I
think,
what
what
is
session
key.
It
might
be
different
from
the
formal
analysis
we
need
to
define
the
the
concept
of
a
session
key
and
then
what
is
actually
used
in
ad
hoc,
where
you
we
do,
derive
different
session
keys
for,
for
example,
oscar,
but
that
may
or
may
not
be
covered
in
the
formal
analysis.
But
I
think
we
need
to
come
back
to
that.
L
A
Okay,
so
so
we'll
have
to
cut
it
here,
so
I
propose
we
take
this
to
the
mailing
list,
as
this
is
crucial
for
the
security
of
the
protocol
and
for
the
for
the
for
the
work
of
this
working
group
so
mark.
Thank
you
for
letting
us
know
that
you
work
on
this
on
this
as
well.
A
M
Yes,
so
normally
I
guess
it
would
not
require
so
much
time,
so
I
have
to
check
with
david,
but
I
think
yes,
two
months
is,
will
be
enough
to
conclude
the
security
analysis.
A
A
O
So
maybe
the
single
typical
slide
will
be
this
one,
which
is
just
to
give
you
a
taste
of
what
it
looks
like.
Essentially,
oh
we
model
things
and
what
we
do
is
we
abstract
the
function
computations
by
simply
specifying
which
property
they
should
satisfy
so
typically
to
declare
a
decryption
and
encryption.
O
We're
going
to
give
this
definition
that
decryption
of
encryption
gives
back
the
plaintext
essentially
and
we're
just
going
to
define
positively
the
kind
of
properties
verified
by
the
computation,
and
this
will
be
enough
to
verify
your
security
file
attacks
and
we
can
define
properties
in
a
very
generic
way,
which
is
essentially
event-based
and
time-based.
O
So
we
can
ask
for
response.
So
what
you're?
Seeing
at
the
bottom
of
the
slide
is
some
authentication
property.
We
will
say
saying
that,
whenever
r
accept
with
some
parameters,
typically
a
pki,
a
public
key
for
the
initiator,
which
corresponds
to
some
honest
api,
then
it
implies
that
somewhere
in
the
past,
the
initiator
did
accept.
So
we
can
specify
a
lot
of
properties
like
that
secrecy
and
everything
we
want
to
check
essentially
on
lake.
O
What
we've
done,
which
is
a
bit
different
from
other
works
in
in
our
model-
is
that
we're
trying
to
push
a
bit
further,
the
modeling
to
capture
a
lot
of
small,
sometimes
unexpected
behaviors
of
the
primitives
that
are
not
taken
into
account.
So,
typically
for
the
field,
man,
you
have
an
identity
element
that
whenever
you're
gonna
exponent
it,
it's
gonna
fall
back
to
the
identity
element.
But
you
also
have
lower
points
that
can
easily
create
collisions
between
exponential
exponentiated
values.
O
O
Public
keys
that
will
always
validate
for
against
all
messages
and
typically
functions
like
256
have
well
based
on
the
merchandise,
lens
extensions
and
also
some
kind
of,
and
we
can
consider
many
subtle
weaknesses
of
high
functions
that
already
exist
typically
for
md5
and
show
one
that's
exclusions,
and
that
will
maybe
one
day
will
exist
on
256
and
we
try
to
be
prepared
if
they
arrive
so
more
quickly
includes
the
four
methods
of
authentication
that
can
be
fully
executed
in
parallel.
O
So
that's
which
nice
for
the
protocol,
but
when
we
can
start
to
consider
a
stronger
threat
model
that
will
occur
a
lot
of
fun
that
are
less
likely
to
happen,
but
that
can
still
be
realistic
and
interesting.
O
So
I'm
not
gonna
disappear
quickly.
Those
three
points,
but
for
the
details
and
everything
we'll
be
sending
out
on
the
main
list,
with
concrete
proposals
to
make
it
straightforward
so
talking
about
potential
misuse
now,
and
it
actually
ties
back
to
the
description
that
was
happening
at
the
end
of
the
previous
talk.
What
we
call
the
session
key
so
prk
for
extreme
actually
offers
weaker
properties
in
terms
of
securities
than
the
exported
keys.
O
Typically,
because
if
we
have
a
dishonest,
if
you're
talking
to
a
distance
responder,
they
may
have
a
lot
of
control
over
the
final
value
of
this
prk,
for
instance,
because
they
will
standards,
the
identity
actually
match
or
in
the
post,
confirm
setting
an
encapsulation
that
can
have
full
control
actually
of
the
prk
for
x3
and
k,
and
also
compared
to
the
exported
section
here.
This
session
key
is
not
linked
to
the
execution
of
the
protocol,
and
typically
it
does
not
authenticate
gh4
and
so
typically.
O
Well,
an
implementer
may
decide
currently
from
the
standard
to
use
a
different
key
exporter
than
the
one
specified
actually
and
if
they
do
and
do
not
include
the
tf4
inside
the
key
which
is
used,
then
you
can
break
the
authentication
of
th4,
because
the
key
confirmation,
since
we
have
prk
for
x3m,
won't
authenticate
tier
4,
of
course,
and
even
competing
successfully,
because
typically,
yes,
ccm
is
kind
of
viable.
So
in
the
formal
sense
you
have
the
integrity
of
the
plaintext,
but
not
on
the
side
for
text
you
can
break
the
absolute
key
of
th4.
O
So
essentially
it
looks
like
it
was.
A
protocol
would
benefit
from
a
clarified,
essentially
final
key.
What
is
precisely
the
session
key,
which
would
be
the
equivalent
of
the
master
secret
in
class
and
so
typically
adding
a
final
cheat
elevation
where
we
tie
together
the
prk
and
the
transcript
will
produce
the
final
key
with
the
best,
whatever
guarantees.
Essentially
and
typically,
this
will
develop
some
kind
of
optimization
to
remove
the
tf4
from
the
star
material
and
the
exporter
in
later
times,
essentially
a
second
potential
misuse
of
the
designer.
O
O
The
last
message
there's
actually
an
issue
with
that
for
the
third
message,
because
whenever
we
use
aeds,
it's
very
important
in
terms
of
cryptographic
guarantees
to
never
use
the
same
key
and
the
same
iv
for
two
distinct
messages
and
well
at
the
step
of
the
third
message:
if
you
store
the
stair,
if
you
store
the
statues
to
compute
this,
this
message:
if
and
if
the
signature
is
randomized,
which
is
the
case
for
some
of
the
skills
proposed
here,
what
you're
going
to
do
is
compute
two
different
messages,
because
the
signatures
are
randomized,
entrepreneur
use
the
id
came
with
the
same
iv
and
key
for
both
of
those
different
messages,
and
thus
it
falls
outside
of
the
classical
use
of
aed
schemes.
O
So
here's
the
suggestion.
If
it's
simple,
we
should
just
follow
this
state.
Storing
and
just
simply,
if
you
want
to
listen
message,
you
need
to
listen
exactly
the
same.
Essentially.
O
O
O
It's
in
the
static
qualification
mode,
where
the
idea
is
that
actually
the
mac
key
and
the
station
key
are
exactly
exactly
the
same
thing.
They
are
the
same
value.
So
if
you
look
at
the
on
the
session
key,
you
are
licking
the
mac
key
and
then
the
attacker
can
using
this
mac
key
use
it
to
produce
other
macs
expected
and
you
can
lie
to
respond
essentially
and
thus,
essentially
in
the
static
authentication
mode
trusted
execution.
Environment
doesn't
really
make
sense,
and
it's
to
note
that.
O
It's
not
the
case
in
method,
zero,
where
you
can
do
everything
nicely
and
the
secret
key.
If
you
store
this
product
for
the
signatures
inside
the
te,
you
don't
have
this
issue
so
there'll
be
two
things
here,
which
is
one.
The
static
authentication
method
is
in
term
of
te
implementation
slightly
weaker
than
method
zero,
and
we
need
to
think
if
we
want
to
propose
implementations.
O
We
need
to
find
a
way
to
make
those
things
better.
So
there
may
be
possibilities,
but
it's
it's.
Quite
it's
still
a
question
to
propose
the
best
interface
for
people
that
would
want
to
use
a
ge
and
finally,
the
last
point,
which
is
about
so
what
about
10
years
or
20
years
from
now?
Will
it
be
still
secure
and
essentially
what
we
want
to
look
at?
O
Are
children
to
these
collisions
so,
as
I
said,
for
mp5
and
show
one
those
things
actually
exist
and
for
statue
not
yet-
and
maybe
never,
maybe
in
10
years
they
exist.
So
ideally
it
would
be
cool
if
we
don't
have
those.
If
these
kind
of
things
don't
lead
to
attacks
on
the
protocol,
and
so
we
have
a
threat
model
where
essentially
the
attacker
given
two
prefixes
p1
and
p2-
can
compute
two
big
bit
strings,
c1
and
c2.
O
Subject:
z
creates
a
collision
between
the
hash
of
p1
method
with
c1
and
the
hash
of
p2
connected
with
cq
and
using
this
kind
of
collisions
and
the
fact
that
the
protocol
adjusts
may
accept
the
identity
element.
O
O
It's
actually
quite
simple
to
mitigate
this
thing
and
typically
so,
checking
for
lower
the
groups,
or
at
least
the
identity
element,
and
this
kind
of
attacks
typically
expose
the
fact.
Well,
you
need
to
stuff
a
lot
of
bits
that
respond
to
the
collision
bits
inside
the
transcript
to
be
able
to
create
the
collision.
So
it
actually
exploits
a
lot.
O
So
to
conclude
this
overview
well
on
the
long
term,
we
first
want
to
improve
on
the
analysis
so
typically
to
include
the
cube
date.
The
first
message
we
plan
to
keep
themselves
up
to
date,
so
whenever
the
draft
evolve,
our
plan
is
to
keep
them
up
to
date
and
this
all
the
way
up
to
the
final
lfc.
A
Thank
you,
charlie.
So
do
we
have
any
questions
for
charlie,
so
there
was
a
comment
by
christian,
but
you
okay,
so
so
he
will
bring
it
to
the
mailing
list
about
future
proofing.
This,
I
suppose
so
in
since
we
don't
have
any
questions
yeah.
We
can
only
thank
you
for
doing
this
work.
The
this
is
really
great.
A
I
propose
a
as
an
action
item
for
the
authors
to
convert
this
list
of
this
list
of
remarks
into
github
issues
and
that
we
start
with
discussing
those
one
by
one
on
github
and
on
the
mailing
list
where
necessary,
and
this
would
be
our
typical
working
process
in
the
working
group,
but
other
than
that.
I
think
again.
This
is
great.
Thank
you.
A
So
much
for
doing
this
work,
and
just
maybe
could
you
comment
so
could
you
comment
on
your
future
plans
regarding
this
work,
because
the
protocol
is
still
not
completely,
we
might
publish
new
versions.
Do
you
plan
on?
Do
you
plan
on
updating
this
model
that
you
did
and
do
you
plan
to
stick
around.
O
Definitely
so,
at
least
on
my
side,
I
want
to
commit
on
that.
Hopefully
I
can
bring
my
curve
in
also
but
yeah.
I
want
to
keep
working
on
this
project.
Definitely.
A
Okay,
that's
great,
and
one
last
question
is
or
you
I,
I
suppose
you
plan
on
publishing
this
in
some
venue
in
this
work.
Yes,
so
please
let
keep
us
informed
the
working
group
or
us
the
chairs,
and
we
can
forward
to
the
working
group
about
any
publication.
That
is,
that
results
from
this
work.
A
Yes,
so
with
that,
I
would
like
to
conclude
the
slot
on
the
formal
analysis
and
again
I
cannot
emphasize
this
enough
how
important
this
work
by
baptiste
and
by
by
charlie
and
his
team
is
important
for
the
working
group,
and
I
believe
I
speak
on
behalf
of
the
whole
working
group
when
I
really
thank
you
for
doing
this,
and-
and
also
I
invite
mark
who
we
have
just
came
to
be.
A
We
just
realized
that
there
is
another
activity
going
on
that
we're
kind
of
not
aware
of
to
reach
out
to
the
to
the
lake
chairs
or
the
lake
at
itf
mailing
list
to
let
us
know
about
the
plan
and
the
activities
such
that
we
can
synchronize
the
activities
for
end
presentations
for
the
next
itf
meeting.
A
A
B
B
I
have
control
fantastic.
Oh
sorry,
I
actually
don't
know
how
to
change
lines.
C
B
Found
it
no
worries?
Okay,
so
since
this
will
be
talking
about
the
ad
hoc
draft
and
the
trades,
this
drive-
those
are
the
two
drafts
and
there
has
been
on
the
terms
of
publications.
There
has
been
no
changes
because
we
have
still
the
old
versions,
but
we
have
been
progressing
these
on
the
github
and
what
we've
done
is
mainly
finishing
off
the
five
reviews
and
updating
based
on
all
those
comments
and
that's
completed.
Now
we
don't
have
any
old
issues.
B
B
B
B
And
similarly,
in
section
3
8.
We
also
split
the
content
into
what
are
the
expectations
on
the
external
authorization
data
and
that
specification
of
the
ead
value,
and
that's
that's
from
that's
part
of
the
body
now,
whereas
the
append
new
appendix
e
contains
examples
like
we
talked
about
in
the
previous
itf
meeting.
B
So
we
hope
this
is
making
more
clear
what
is
part
of
the
core
protocol
and
what
is
outside
the
protocol
and
things
that
sort
of
relate
to
the
protocol,
but
are
not
strictly
part
of
of
of
the
specification
and
the
update
to
processing
was
also
to
handle
the
accordingly.
What
what
the
things
that
relate
to
the
core
protocol
is
is
is
stays
in
the
processing
and
the
things
that
are
not
in
the
core
protocol
is
taken
out.
B
So
implementations
must
support
cypher,
suite
2
and
3,
but
we
also
have
a
general
precondition
saying
that
in
the
absence
of
an
application
profile
specifying
otherwise-
and
so
that's
that's
what
we
have
agreed
on
in
on
the
mailing
list-
and
I
mean
following
this
interim
discussion,
so
it
it
wasn't
something
everyone
was
super
happy
over,
but
this
was
basically
something
that
everyone
seemed
to
be
able
to
live
with,
and
there
is
another
update
on
the
compliance
requirements
related
to
padding
and
we
have
now
introduced
them
must
be
able
to
parse
padded
messages.
B
So
it's
the
ability
to
handle
plain
text
sort
of
to
hide
the
length
of
the
plain
text.
You
must
be
able
to
parse
padded
messages,
but
not
all
use
cases
need
to
actually
use
this,
so
the
must
is
on
the
receiving
side,
not
on
the
on
the
sending
side
and
those
were
the
changes
to
the
compliance
requirements.
B
B
As
you
see
here,
score
master
secret
and
oscar
master
salt
is
now
there's
not
a
shorter
label,
and
that
means
that
the
that
that
is
sort
of
new
that
means
that
the
that's
that's
the
breaking
change.
Basically,
when
everything
up
to
this
point
is
the
same,
but
when
you
derive
the
oscore
master
secret
and
salt,
you
would
now
get
new
values
and
the
test
vectors
are
updated.
B
On
this
point
and
another
update
related
to
connection
identifiers,
where
there
was
a
request
that
to
mention
that
you,
you
actually
don't
need
to
have
support
both
integer
and
byte
string
connection
identifiers,
an
endpoint
may
choose
to
select
a
specific
range
and
specify
that
in
the
application
profile
and
there's
updates
to
security
considerations,
ionic
considerations
and
clarifications.
B
So
that's
the
other
updates
and
and
with
that
we
have
addressed
all
open
issues
and
now
we're
just
waiting
for
for
the
the
new
issues
coming
from
from
the
hackathon
and
from
these
excellent
inputs.
From
the
from
the
analysis
we've
heard
today
for
the
traces
document.
This
situation
is
similar.
We
have
a
new
version
in
the
github
and
we
have
no
open
issues
related
to
that
and
just
a
reminder.
The
trace's
document,
the
purpose
of
that
is
to
help
implementers
to
get
detailed
printouts
with
intermediate
steps.
B
So
you
could
go
basically
line
by
line
through
through
your
code
and
verify
that's
been
confirmed
to
be
very
useful.
But
it's
not
a
complete
set
of
test
vectors.
It's
just
two
specific
traces,
two
specific
test
vectors
which
are
annotated
carefully
and
the
change
we've
made
since
version
zero.
Zero
is
that
we
have
as
this
scene.
Here
we
used
to
have
two
traces.
We
still
have
two
traces,
the
the
one
with
static
diffie-hellman
used
to
be
curb25519
in
the
new
trace.
B
It's
actually
p256
the
signature,
one
is
still
eddsa,
but
we
have
now
included
real
x509
certificates,
not
the
dummy
ones
that
was
mentioned
previously
in
in
this
session.
There
is
also
two
more
additions.
There
is
an
example
of
cyprus
with
negotiation
on
the
static
tiffy
helmand
trace,
and
there
is
an
explicit
mentioning
of
y
coordinates,
which
also
been
requested,
and
we
reversed
the
order
of
the
two
traces
just
an
editorial
here,
but
basically
we
have
all
all
the
changes
that
was
requested
on
the
tracer.
B
And
that
leaves
us
with
the
test
vectors,
and
I
can
I
think
I
can
skip
now
to
the
last
slide.
I
only
have
a
minute
left,
so
the
next
steps
we
propose
to
now
take
what
is
done
in
the
master
branches,
the
master
branch
to
and
submit
a
new
version,
because
that
has
been.
We
have
basically
completed
all
the
reviews
and
all
the
old
dishes,
and
we
get
comments
from
people
who
read
the
old
versions
and
think
that
elder
12
is
the
latest
version
which
it
is,
but
it
there
are
some
changes
now.
B
B
So
those
were
the
documents
and
then
the
next
step
is
also
the
most
issues.
Current
issues
are
about
test
vectors.
So
that's
what
we
want
to
progress
next,
we
should
set
up
a
breakout
meeting
this
week
and
marek
has
already
done
a
very
good
input
here
and
he's
proposed
to
to
help
out
with
making
the
test
vectors
more
available.
B
C
Okay,
so
any
quick
comments
on
the
changes
or
clarification
questions.
C
C
So
maybe
the
right
thing
to
do
is
now
that
we
know
that
some
people
are
working
on,
doing
analyses
to
poll
them
and
see
what
it
would
delay
or
upset
them.
If
we
move
on
to
13,
or
would
they
find
it?
Okay,
we
could
do
that.
We
could
just
we
kind
of
know
who
the
set
of
people
to
work
is
now
right.
Yeah,
yeah.
A
Exactly
so,
we
know
there
are
so.
This
is
four
teams
that
are
involved
right
now
and
I'm
so.
I
think
it
kind
of
makes
sense
to
reach
out
directly
and
work
directly
with
those
folks
and
once
again
I
invite
everyone
who
might
we
not
be
aware
of
that
is
working
on
the
security
analysis
of
ad
hoc
to.
Let
us
know
such
that
we
could
coordinate
about
this.
C
C
A
So
yes,
so
yes,
the
decision
to
freeze
the
specification
was
until
further
notice,
so
it
is
up
to
us
right
now.
John,
do
you
want
to
say
something.
N
Yeah,
I
think
we
in
the
room
here
knows
what
what
expired
draft
is
not
the
end
of
the
world,
but
people
outside
our
diet
sometimes
believe
that
means
the
work
has
been
dropped.
So
I
think
I
think
the
expiry
means
something
and
we
should
not
let
it
expire.
I
think,
if
the
implementers
absolutely
don't
want
the
new
version,
I
think
we
should
just
take
for
12
version
and
resubmit
the
deaths
at
13
without
any
changes
just
to
avoid
expiry.
Otherwise
I
100
sure
we
will
get
people
asking
about
if
this
has.
A
So
if
I
understand
correctly,
the
draft
will
expire
on
23rd
of
april,
so
that
gives
us
one
month
to
decide
and
to
proceed
with
the
to
proceed
with
the
next
steps,
essentially
seeing
if
the
teams
checking
out
with
the
different
crypto
analysis
teams,
whether
they
can
update
their
their
models
and
their
work
to
the
latest
specification.
A
A
So
so,
with
that
we
are
done
with
all
the
agenda
items.
Do
we
have
any
other
business.
B
Yes,
yes,
I
just
wanted
to
say
I
didn't
talk
about
the
about
the
test
vectors
here,
so
people
who
are
interested
in
test
vectors
pay
attention
to
what's
happening
in
the
get
will
happen
in
the
github
now
so
as
we
start
to
make
that
that
seems
to
buy
the
last
part,
which
is
which
we
need
to
to
take
some
action
on
and
there's
been
a
lot
of
interest
in
the,
in
particular
the
json
test
vectors,
because
that's
the
bulk
of
the
of
the
tests
that
you
may
want
to
do
on
your
implementation.