In this chapter we explain how to start tamarin, how it works internally, and how to interpret its output. For tamarin to work, two tools it depends on must be installed. One tool needed is Maude [106], which is used for variant computation and unification modulo associativity-commutativity. The other tool needed is GraphViz [69], which is used for visualizing graphs. tamarin supports two interfaces, each offering users a different way to interact with the tool. The first interface is a graphical user interface that is accessed from a web browser. This is the interface that most users will use most of the time as it supports an interactive mode of usage where users interact with the prover. For example, they can have tamarin display (incomplete) protocol executions as graphs and use these graphs to visualize attacks or debug models. Moreover, they can try different proof strategies to extend these graphs and explore different proof alternatives. The second interface is a simple command-line interface. It can be used to re-run existing files, to simply check protocol descriptions for syntax errors, or to measure the time needed for proof construction.