►
From YouTube: IETF-UFMRG-20230901-1600
Description
UFMRG interim meeting session
2023/09/01 1600
A
A
B
A
A
There
now
great
and
there's
a
slide
copied
here.
We
obviously
don't
have
in-person
participants,
but
you
know
please
mute
unless
you're,
presenting
or
speaking
and
headsets
are
kind
of
recommended.
Even
though
I'm
not
using
here's
today's
agenda,
we
have
an
hour,
we
don't.
We
don't
need
to
use
an
error
if
we
go
quicker,
that's
better!
A
A
You
know
the
sequence
of
meetings
goes
on
in
the
future.
If,
if,
if
you
don't
do
something
this
time,
you
can
do
something
next
time
or
in
a
year's
time
or
perhaps
remote,
so
you
know
don't
think
about
this
as
a
winners
and
losers
thing,
it's
more.
What's
what's
who's
in
a
position
to
kind
of
do
something
for
Prague,
you
know
most
easily
most
effectively,
that
kind
of
thing.
A
So
that's
our
agenda
and
then
at
the
end
we
have
sort
of
any
other
business.
If
people
want
to
raise
stuff,
does
anybody
have
a
issue
with
the
agenda,
something
they
want
to
change
and
while
you're
thinking
about
that
can
would
anybody
be
willing
to
help
with
just
keeping
a
few
notes
in
the
headstock.
D
A
A
I
think
you
can
right
click
the
note
taking
tool
to
open
a
new
window
or
tab.
Oh
yeah
I.
Have
it
thanks
excellent
thanks
for
helping
so
yeah,
and
we
don't?
We
don't
need
blah
blah
blah
notes.
Just
just
you
know,
decisions
or
information.
It
doesn't
have
to
be
narrative,
notes,
okay,
so
anybody
else
want
to
patch
the
agenda.
A
If
not,
then
I
guess
our
Jonathan.
Do
you
want
to
jump
in
and
say
anything
at
this
point
or
no
okay,
so
I'll
just
leave?
This
is
the
list
of
Technologies
I.
Think
that
people
have
mentioned
has
been
possibles
and
I'll
kind
of
try
and
describe
what
we
think
is
possible.
Logistically,
so
the
Sunday
before
the
ITF
meeting
there's
a
thing
called
the
iepg
which
meets
at
from
10
until
noon
and
typically
their
room
is
prepared
with
all
the
audio
visual
stuff.
A
That
seems
to
make
sense
to
have
two
hours
as
a
length
of
a
session
for
one
particular
training
or
just
under
two
errors,
with
a
20
minute
cap
in
between
which
then
would
lead
us
to
think
that
it
seems
to
make
sense
to
try
and
have
training
about
two
different
Technologies,
if
possible
in
Prague.
So
that's
two
sessions
roughly
two
hours
each
and
what
we
were
thinking
and
again
this
this
could
be
up
to.
A
A
What
we
also
do
is
we're
again
we're
not
quite
sure
of
the
numbers
that
we'll
have
available
sorry,
the
room
we
have
available,
how
big
it
is.
So
we'll
probably
ask
people
to
do
a
sign
up
and
we
might
limit
the
numbers
to
yeah
whatever
same
sensible
based
on
the
room
and
the
actual
people's
preferences,
because
it's
not
credible
to
kind
of
be
doing
any
useful
training
for
200
people,
and
if
we
only
get
two
people,
then
it's
probably
also
that
tells
us
something.
So
we
have
a
sign
up.
A
Forget
it's
North
America
somewhere
I,
guess,
yeah,
Vancouver,
Vancouver
and
then
Dublin
so
yeah
and
yeah.
You
know
I
think
there
is.
There
is
a
slight
kind
of
European
Focus
for
this
people
in
this
technology
space.
So
if
we
wanted
to
do
something
in
the
Years
time
in
Dublin,
I
I
can
certainly
help
with
with
that
I
can
get
rooms
if
we
want
to
live
in
University
or
something.
A
Lastly,
okay
I
should
have
said
it
because
this
is
an
ietf
setup,
we're
recorded
and
similarly
we'd
like
to
be
able
to
record
the
training
if
possible,
and
then
you
know
so
the
people
who
can't
make
this
love
can
still
get
some
benefit,
and-
and
so
we
can
learn
to
do
it
better
next
time
so
again,
we'd
hope
to
be
able
to
record
the
training
in
Prague.
We're
not
100
sure
if
that's
possible
yet
or
not,
it
depends
to.
A
It
depends
on
what
the
meadeco
setup,
how
complete
it
is
for
a
Sunday
so
we'll
find
that
out
shortly,
I
guess
Okay,
so
any
other
any
questions
about
the
logistics
or
people.
Thinking
that
what
we're
described,
what
we
described
is
that
the
terrible
idea
or
an
okay
idea,
any
feedback
on
that
it'll
be
good
to
get
now.
So
if
you
have
some
feedback
on
that,
please
do
join
the
Q
and
Phoenix.
D
A
E
So
if
we
could
do
something
more
higher
level,
that
would
be.
That
would
be
really
useful.
I
think,
maybe
not
for
the
first
attempt
at
this,
but
certainly
I,
think
for
a
future
attempt.
It
would
definitely
be
worth
saying
we
assume
you
know,
you
know
the
first
five
pages
of
the
Tamara
manual
I,
don't
know
some
number
but
yeah
I,
guess
maybe
for
the
first
iteration,
we'll
still
not
be
really
sure
what
we're
doing
so.
A
F
Yeah
I'm
very
happy
with
this
plan
and
more
than
a
little
bit
of
a
guess,
future
logistic
question
which
is
more
about
if
the
results
of
these
first
experiment
just
go,
that
way
are
going
to
then
be
posted
Somewhere
over
the
PDFs
of
the
talks
or
the
slides.
You
know,
I,
don't
know
if
the
research
group
has
a
GitHub,
but
it
would
be
good
for
future
reference
to
get
anything
that
it's
documentation
from
these
to
be
publicly
available
for
future
reference.
A
Sure
yeah
I
believe
the
I
think
the
setup
that
we'll
be
using
is
pretty
much
the
meteco
thing
that
we
have
here.
The
only
question
is
whether
we
have
normal
recording
or
not.
So
all
the
slides
and
things
will
be
in
the
in
the
data
tracker
and
if
we
can
get
recordings
and
we
probably
will
somewhere
another
those
will
end
up
in
the
normal
places
on
YouTube,
for
example,
and
we
can
we
can
populate
the
research
group
Wiki
or
whatever,
whatever
people
think
is,
is
best
yeah.
E
There's
one
other
like
there's
one
bit
of
documentation
that
we
might
forget
to
put
in
which
Sophie
just
reminded
me
of
we
should
say
at
least
which
version
of
the
tool
the
thing
relates
to,
because
at
least
Tamarind
changes
stuff.
Sometimes
so
we
should
say
like
we
are
using
version
XXX
of
this
tool.
A
Good
and
then
one
other
thing
actually
I
forgot
to
say
is:
if
somebody
here
has
experience
with
how
to
do
a
good
survey
about
the
effectiveness
of
this
kind
of
training,
then
I
Jonathan
I
would
like
to
hear
from
you,
so
we
can
figure
out
what
kind
of
feedback
to
look
for
that's
not
kind
of
stupid
and
might
be
useful.
So
again,
if
somebody
here
knows
how
to
do
that
kind
of
thing.
Well,
then,
please
do
get
in
touch.
A
A
A
A
Record
flux
again,
we
don't
seem
to
have
anybody
who's
able
to
talk
to
that.
Right
now
looks
like
that
in
that
case,
so
let's
try
and
get
like
you
know
again:
it's
not
a
competition,
it's
like
which
of
US
thinks
we
can
kind
of
do
the
best
thing
and
let's,
let's
have
like
five
minutes
for
each
of
those
Felix.
You
have
a
question.
First
I
was
going
to
do
them
in
the
order
of
Isabel,
Tower
and
cochlear
program.
C
A
Have
somebody
from
willing
to
talk
about
to
verify
here?
Sorry,
pardon
me,
Nadeem
I,
see
you
are
here
so
I
presume
you
can
do
that
and
I
shall
fix
the
slide,
yeah
yeah,
so
I.
The
answer
may
be
obvious.
Hopefully
it
is,
but
let's
give
people
a
couple
of
minutes
to
talk
about
what
they
think
could
be
done.
So
we
take
them
in
the
order
of
Isabel
Tamron,
then
verif
pal,
which
was
the
order
of
the
emails
then
then
proverbs
so
Isabel
I.
Think
Gregory.
A
B
B
F
E
A
Grace,
the
other
thing
I,
wouldn't
I,
mean
if
you're,
if
you're,
not
if
it
turns
out
you're,
not
able
to
work
for
produce
something
for
product
which
is
which
is
fine,
and
you
want
to
do
something
for
later-
maybe
don't
put
in
too
much
effort
until
after
product
and
you
can
kind
of
learn
from
how
we
get
on
there.
That's
just
a
suggestion.
Okay,
so
that's
great
that
simplified
our
problems,
fantastic.
A
D
Yeah
I
remember
I,
quickly,
introduce
myself
again
as
well:
I'm
Felix
I'm,
a
PhD
student
at
eth,
Zurich
and
I
have
worked
both
with
and
on
Tamron,
so
in
a
two-hour
Workshop,
my
goal
would
be.
Maybe
let
me
also
introduce
Tamron
for
a
second.
So
Darren
is
a
protocol
verification
tool
that
allows
the
consideration
of
an
unbounded
number
of
participants
and
parallel
sessions
and
I'm.
Also
lengths
of
the
protocol
runs
and
it
has
been
used
for
various
case
studies.
One
of
them
is
the
verification
of
TLS
1.3
performed
by
in
part
Jonathan.
D
Here
I
would
give
a
two
hour
workshop
on
Tamarind,
where
the
goal
really
is
to
lower
the
barriers
of
access
to
Tamarind,
so
where
the
goal
is
to
get
people
comfortable
approaching
the
tool
I've
hosted
a
workshop
like
this,
with
some
success.
I'd
say
last
week
at
the
of
security
Workshop
in
akam
by
London
and
I.
I
cannot
talk
for
cars
schedule.
He
also
expressed
interest
to
give
a
tutorial
on
Tamron,
but
if
he
has
time
we
would
certainly
do
it
together.
D
We
did
it
in
the
past
and
we
have
a
lot
of
materials.
I
think
a
good
thing
about
Taiwan,
which
is
worth
pointing
out,
is
that
it
has
a
fairly
decent
GUI.
That
makes
it
very
that
makes
it
in
the
space
of
formal
methods,
rather
approachable
yeah.
So
that's
that
would
be
my
goal
for
the
ITF
Workshop.
Are
there
any
questions?
Maybe.
A
D
I
think
it's
rather
possible
they're
not
possible.
If
Jonathan
is
there
I
don't
know,
Jonathan
could
help
out
with
Tamron
cast
expressed
interest.
I
cannot
speak
on
cast
behalf
he's
currently
on
vacation,
so
we
did
like
he
didn't.
Tell
me.
Phillies
I'm
definitely
going
to
be
there,
but
obviously
he
expressed
interest
and
as
I
know
him
he
would
have
checked
his
calendar
as
well
before
expressing
interest.
So
that
would
make
three
people
already
yeah.
A
D
A
A
G
It
does
support.
You
know
modeling
protocols
between
principles
and
so
on,
but
it
does
some
things
differently
from
proverif
and
Tamarin,
with
a
uncompromising
focus
on
user
friendliness,
it
painstakingly
speaks
about
principles
and
protocols.
Explicitly
you
know,
there's
Alice,
explicit,
Alice,
explicit,
Bob
Alice
is
doing.
This
Bob
is
doing
that.
The
way
that
messages
are
formulated
and
queries
are
formulated
is
meant
to
be
more
intuitive
and
easy
to
learn.
G
That
being
said,
it
is
not
a
tool
that
is
as
suitable
for
a
more
sort
of
profound
analysis
and
fine-grained
Analysis
as
Tamarin
or
proverif,
and
so
I
would
very
much
like
to
stress
that
the
value
that
verify
brings
in
general
and
also
at
an
event
such
as
potentially
this
one
is
more
so
its
ability
to
enfranchise
Engineers
people
who
are
really
not
into
this
stuff.
To
begin
with,
as
an
initial
stepping
stone
towards
learning
how
models
are
written,
how
to
read
models,
how
analysis
Works?
G
G
Please
keep
this
in
mind
if
you
decide
to
move
forward
with
verif
pal,
because
if
you
want
to
get
like
more
serious
analysis,
stuff
you're
going
to
have
to
go
with
some
of
the
other
tools,
I'd
also
close
by
saying
that
I
have
significant
knowledge
and
expertise
in
proverb
and
so
I
would
be
able
to
contribute
in
the
Prevail
area
as
well,
potentially
in
collaboration
with
Mohamed
Sardar,
who
I
think
is
also
volunteering
and
yeah
thanks.
That's
all
I
have
to
say.
A
G
Sure
yeah
yeah
we've
done
a
bunch
of
sessions
on
verif
pal
and
there's
a
bunch
of
people
in
the
community
who
are
either
involved
or
have
helped
out
concessions.
Before,
notably,
there
was
one
at
eurocrypt,
where
I
did
it
with
my
former
Master's
student
and
so
yeah.
That
was
significant
involvement
in
participation.
H
E
G
So
we
formalized
the
soundness
of
verif
pal.
In
being
I
mean
when
I
was
a
PhD
student
working
on
proverb,
we
found
a
ton
of
bugs
in
proverb
bugs
have
been
found
in
Tamarind,
bugs
are
certainly
found
in
verif
pal,
but
these
bugs
are
more
so
just
like
errors
in
the
code,
the
general
way
in
which
verif
pal
Works
has
been
described
formally
and
also
analyzed
and
formalized
in
as
well.
D
Oh
yes,
I
have
a
question.
Maybe
this
is
just
hearsay
but
I
thought
that
someone
once
mentioned
that
the
tool
can
report
it
doesn't
find
an
attack
while
there
is
one,
but
maybe
that
was
so
in
in
some
intuitive
Sense
on
soundness
but
yeah.
Maybe
this
person
was
just
wrong
and
formed
right.
It's
just
hearsay.
I
didn't
look
into
verify,
so
it's
it
sounded
complete
in
both
senses
like
it
might
not
terminate,
of
course
undecidability,
but.
D
G
D
C
C
But
then,
of
course,
if
you
want
to
go
into
the
details
and
then
the
question
is
how
far
do
you
have
to
go
and
how
much
can
you
assume
from
the
audience
to
know
already
so
I
really
like
to
make
sort
of
this
distinction
right?
You
have
the
general
purpose,
Theory
improving
tools
like
Isabel
cook,
and
then
you
have
sort
of
domain
specific
tools
really
focused
on
on
modeling
protocols
and
for.
F
C
C
C
A
A
C
C
Yeah,
so
so
the
the
the
the
domain
specific
tools
are
more
for
suited
for
protocol
verification
in
the
sense
of
man.
You
want
to
verify,
for
instance,
security
properties
in
in
this
case
a
general
purpose.
Theory
improver
is
more
showing
how
you
would
model
the
behavior
of
a
protocol.
So
that's
sort
of
it's
it's
more.
How
you
would
embed
protocol
behavior
in
a
general
purpose?
C
C
A
H
Now
we
are
working
with
arm
and
very
actively
with
other
partners
harness
who
is
in
the
call.
So
he
has
one
of
the
internet
drafts
that
we
are
now
formatizing,
which
is
a
remote
attestation
plus
TLS,
so
people
from
arm
Siemens,
linaro
and
burkhausen
Institute
and
myself
from
TU
test,
and
so
we
are
all
involved
in
this
and
trying
to
use
proverif
to
provide
a
better
specification
for
this
draft
that
I
also
sent
in
the
email.
H
So,
in
brief,
or
in
summary,
what
I
would
say
is
that
we
have
tackled
both
kind
of
audience,
which
is
number
one.
I
will
skip
out
the
the
students
of
the
address
and
who
have,
let's
say,
even
no
knowledge
of
security.
So
we
started
from
the
beginning
slightly
over
the
period
of
these
four
years,
we
started
introducing
program
slightly
via
simple
examples,
giving
them
to
the
background
of
security
and
then
a
little
bit
for
formal
methods.
H
We
are
working
very
actively
with
Intel,
where
we,
they
have
shown
a
lot
of
interest
and
they
wanted
to
formalize
further
parts
of
their
own
of
their
system,
which
is
upcoming,
trust
domain
extensions.
Red's
working
group
is
actively
working
on
this
and
then
the
second
category,
which
is
that
knowledge
of
security,
knowledge
of
formal
methods,
but
not
necessarily
of
protocol
verification.
H
In
that
we
have
worked
with
arms
verification
team
and
therefore
arm
the
solution
called
confidential
compute
architecture.
Again
from
the
rats
working
group
of
ITF
there
we
are
working
with
with
Simon
Thomas
and
shields
young.
So
so
what
we
are
doing
is
basically
formalizing
the
parts
of
these
protocols
so
that
they
can
be
integrated
into
the
TLs.
H
So
now
that
part
is
being
integrated
into
into
verification,
so
I
believe
what
I
can
do
is
I
can
I
can
and
proverif
is
maybe
one
of
the
exceptions
which
does
not
have
nice
get
to
start
a
kind
of
a
tutorial,
so
I
had
a
lot
of
difficulties
in
the
beginning,
but
I
would
also
like
to
focus
more
on.
Like
the
the
example,
the
internet
draft
of
harness
I
think
is
a
very
good
example
where
we
have
cover
remote
attestation
and
TLS,
covering
authentication.
Key
exchange
and
Nadeem
also
has
expertise.
H
A
H
B
A
That's
it
looks
like
we
have
four
four
options.
So,
let's
just
have
a
you
know:
what
do
people
think?
How
would
you
go
from
four
to
two?
What's
your
what's
your
suggestion
for
that,
please
join
the
queue
if
you
have
some
suggested
Way
Forward
I
can
see
since
there's
someone
that
some
people
have
been
chatting
in
the
chat
room
and
that's
fine
to
repeat
that
it
might
be
useful.
In
fact,
FedEx.
D
Yeah,
so
will
the
two
sessions
be
hosted
in
parallel
or
consecutively?
It's
consecutive
okay,
I
I
mean
for
me,
I
would
say
it
makes
sense
to
go
for
and
one
other
tour,
because
I
think
all
the
other
truth,
probably
with
Tamarind
verif
Pyle
their
rather
close
together.
So
I,
don't
think
I,
don't
think
it
would
introduce
an
audience
to
that
is
new
to
formal
methods
to
two
different
concepts
of
a
variety
I
would
go
for
and
then
of
course,
I'm
biased
towards
Tamron.
So
this
is
where
I
must
stop
talking.
A
A
F
F
Which
is
I
think
Tamarind
would
be
a
great
age
to
actually
have
sorry.
My
Discord
is
doing
noises.
It
would
be
really
great
to
have
also
because
at
least
several
working
groups
on
the
ATF
has
have
heard
about
the
tool
know
that
it
could
be
used
for
different
protocols.
So
at
least
we
have
that
and
then
I
also
support
what
Felix
was
saying
regarding
so
because
I
think
it's
mainly
a
big
building
block
that
can
serve
for
many
things.
So,
second,
in
that.
A
G
A
G
I'd
like
to
Second
the
like
the
soundness
of
The,
Tamarind
combination,
I
think,
like
I'm,
very
familiar
with
proverif
and
like
well.
Nevertheless,
I
would
say
that
this
is
probably
the
best
way
forward,
given
the
selection
of
the
tools,
the
benefits
that
Tamarind
brings
here
are
likely
the
fact
that
it's
under
a
lot
of
active
research
and
development.
G
A
Great,
thank
you.
Other
I
mean
that's
three
people
in
a
row
who
said
that,
so
we
probably
don't
necessarily
need
more
people
saying
it,
but
if
you
feel
motivated
to
say
that
great
does
anybody
want
to
suggest
a
different
thing,
or
is
everybody
kind
of
saying
you
know
if
timer
and
are
things
we
can
get
the
the
people
and
presentations
ready
for?
A
B
A
So
I
think,
okay,
we
have
11-0.
That
seems
like
okay,
I
think
we
have
a
result.
Excellent!
Thank
you
thanks,
everyone
for
for
being
so
reasonable
about
it
and
and
so
quick,
which
is
good
okay.
So
so,
if
we
go
with
Tamron
and
what
we
I
think,
what
we'll
do
is
Jonathan
and
I
will
kind
of
follow
up
with
email.
We
might
try
and
do
a
few
more
calls
with
people
on
more.
You
know
on
the
kind
of
more
granular
detail
between
now
and
November
and.
A
A
G
18
years,
yes,
I
I
still
am
of
the
opinion
that
it's
possible
that
verif
pal
might
be
useful
for
super
beginners.
Given
that
the
proliferation
of
like
thinking
about
protocols
in
a
formal
way
isn't
exactly
very
strong
in
the
engineer
like
commune
culture
of
the
ietf.
So
and
that's
maybe
not
for
this
event
like
Tamarin
and
are
probably
way
better
and
more
mature
and
developed
and
so
on.
G
A
Great
I
know
you
thank
you
and
and
yeah.
Certainly
we
are
thinking
about
the
future
as
well.
I'm
sure,
for
example,
gergely
will
will
probably
be
you
know,
interested
in
in
maybe
doing
something
with
Isabel
also
in
future,
so
I
think
the
yeah.
This
is
not
the
be
all
an
end.
All
this
is
like
just
the
first,
the
first
kind
of
iteration
of
this.
Thank
you
thanks.