david wong

Hey! I'm David, cofounder of zkSecurity and the author of the Real-World Cryptography book. I was previously a crypto architect at O(1) Labs (working on the Mina cryptocurrency), before that I was the security lead for Diem (formerly Libra) at Novi (Facebook), and a security consultant for the Cryptography Services of NCC Group. This is my blog about cryptography and security and other related topics that I find interesting.

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.



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?)


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


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


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,

leave a comment...