Re: [Ufmrg] UFMRG training at IETF118 - details

[Stephen Farrell <[e-mail]>]

Hi all,

And another last minute detail: the room for the UFM training has
changed to Berlin 3/4 so please head there shortly!

Thanks,
S.

On 23/10/2023 21:43, Stephen Farrell wrote:
> 
> 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
>