Tamarin Prover Introduction posted June 2017

I've made a quick intro on Tamarin Prover, which is a protocol verification tool. I just wanted to show people how practical and fun it looks =)

Well done! You've reached the end of my post. Now you can leave a comment or read something else.

Here are some random popular articles:

Here are some random recent articles:

Comments

Matt

Hi David and thanks for this introduction. Really well-explained, it's the best intro to Tamarin I've found.
Do you mind sharing your dotfiles / tmux settings? That Shell looks really smooth! :) (Is that ZSH?)

david

Hey Matt! Thanks!

I don't really have a lot of congifs, this is oh-my-zsh with the lambda theme, and a few plugins (z, extract, safe-paste, ...)

as for tmux I use the Solaris 256 theme and this plugin: https://github.com/tmux-plugins/tmux-continuum

Gresh

Hi David,

I am trying to look for a way to use a puzzle in tamarin prover lie the client solves a puzzle from server are you able to a assist

Lionel

Hi David,
Very nice intro, I felt like I’ll be able to model something immediately ????

Few questions:

Are In() and Out() already defined primitives, or do they rely on the builtin call you wrote in the top of your file?

Did you thought about using Tamarin for more general models (outside security scope) implying state transitions and expected behavior ?

Best regards,
Lionel