Speaker: Maiwenn Racouchot, Loria (Nancy), CISPA
Tuesday 2025-03-04 14:00, 1Z62
Abstract: Tamarin-prover is a tool for symbolic modeling and analysis of security protocols. It takes as an input a protocol's model, specifying the roles of the different agents (initiator, responder, different attacker models...) and some security properties required by the protocol. Tamarin can simulate an unbounded number of sessions running in parallel, which means an infinite number of role instances and possible fresh numbers. The execution of the different roles gives a transition system. The security properties are written as trace properties that will be matched against the transition system. To conduct proofs, Tamarin includes by default eight static heuristics. They help cover most cases, but can sometimes be really inefficient. In order to deal with these cases, Tamarin allows its users to create personalized heuristics by writing a script in a foreign programing language (usually python). However, this functionality has several limits (limited input information, state agnostic, compatibility issues). Moreover, while going through the proof tree, Tamarin can get stuck in a loop which prevents the proof from finishing. In this presentation, I will present several tools and approaches to improve Tamarin termination, from a new heuristic language to loop detection and bounded explorations for attack finding. I will also show how these new tools can be combined for greater results.