[Ufmrg] UFMRG training at IETF118 - details

[Stephen Farrell <[e-mail]>]

Hi all,

As promised, on the 5th of November, the Usable Formal Methods Research
Group (UFMRG) will host a Tamarin training session from 12:00-16:00 at
the IETF 118 meeting hotel in Prague. The training session will be in
the "congress hall 3" room. [1]

Details below from Felix, who's one of the people who'll be leading the
training. Those details include some install instructions and if you're
planning on coming along, we'd ask you to try the install before you
arrive in Prague - feel free to use this list if you have issues.

While the room is also plenty big enough (capacity is 250:-) we'd also
like to get a sense of how many people to expect, so we can try ensure
we have enough Tamaarin-aware folks in the room to help as we do the
exercises. So please fill in your attendance plans at [2] in the next
week if you can. (You can make up a fake name if you like - we don't
really care who turns up, we just want a sense of likely numbers:-)

We are planning to use meetecho for the session, but we're not really
sure how well this would work for remote folks as it's planned as more
of a hands-on training. However, if a few people would like to try
that, it may help us figure out how to do remote training better in
future. Apologies in advance if the session isn't ideal for remote
attendees.

Many thanks to Felix and Alexander for creating the training materials,
and for Jonathan for helping out too. (If you're reading this and also
have Tamarin-clue, please feel free to get in touch in case we do end up
needing more help.)

Cheers,
Stephen.

[1] https://datatracker.ietf.org/meeting/118/floor-plan?room=congress-hall-3
[2] https://framadate.org/hBEM7APllDGWcxlx

Details from Felix:

What is Tamarin? Tamarin is a state-of-the-art protocol verifier that
has been for example used to analyze the protocols TLS 1.3, 5G AKA, and
the contactless payment protocol EMV, sometimes finding critical
security flaws. Tamarin is best-suited to analyze security critical
protocols that use encryption, digital signatures, or similar methods to
establish desired security properties. Tamarin is unbounded in nature:
it can consider an unbounded number of participants, parallel protocol
executions, or lengths of protocol runs. Its simple input language and
web-based GUI make it a great tool for both formal methods novices and
veterans.

The workshop will be conducted by Alexander Dax, Jonathan Hoyland, and
Felix Linker, three security researchers experienced with using Tamarin
and its internals.

The goal of the workshop is to introduce newcomers to Tamarin. There are
no prerequisites. We recommend, though, that one has a rough
understanding of the most common cryptographic primitives. For example,
it would be beneficial if you had a rough idea of what a public key or
block cipher is.

The workshop materials are provided in a github repository [3]. To
prepare for the workshop, we would like to ask you to install Tamarin
and download or clone the workshop repository. You can find all details
in the Workshop Preparation instructions [4] in the repository.

The repository will contain all workshop materials in a self-contained
form once they are prepared (currently, some exercises/slides are still
WIP). We invite anybody who cannot attend the workshop in Prague to
solve the exercises themselves!

[3] https://github.com/felixlinker/tamarin-workshop
[4] https://github.com/felixlinker/tamarin-workshop#workshop-preparation