Tamarin-prover

Contact owners and managers

1–30 of 225

This is the mailing list for discussions and announcements about the Tamarin prover for security protocol analysis.

Tamarin Prover homepage: https://tamarin-prover.com/

On the homepage you can find a manual, a book, tutorials, tools, and many more resources.

0 selected

Nikodem Witkiewicz, hua hua3

Jan 22

help with partial deconstructions caused by iterative rules and equations.

Dear hua, Thank you very much for your answer. Yes, there is such an option. However, I reached a

unread,

help with partial deconstructions caused by iterative rules and equations.

Dear hua, Thank you very much for your answer. Yes, there is such an option. However, I reached a

Jan 22

Yuheng Wen, Felix Linker5

Jan 19

Interpretating interactive mode for source lemma

Thank you for the clarification! On Mon, Jan 19, 2026 at 12:11 PM Felix Linker <linkerfelix@gmail.

unread,

Interpretating interactive mode for source lemma

Thank you for the clarification! On Mon, Jan 19, 2026 at 12:11 PM Felix Linker <linkerfelix@gmail.

Jan 19

Nikodem Witkiewicz, Felix Linker3

Jan 16

Subterm restriction causes unexpected lemma contradictions

Hi Felix, Thank you very much for your answers. It's quite funny to find a bug in a tool to find

unread,

Subterm restriction causes unexpected lemma contradictions

Hi Felix, Thank you very much for your answers. It's quite funny to find a bug in a tool to find

Jan 16

Emilie, Felix Linker3

Jan 14

DH and Partial Deconstructions Question

Hi Felix, The pattern matching on 'g'^x instead worked! Thank you so much for the pointer and

unread,

DH and Partial Deconstructions Question

Hi Felix, The pattern matching on 'g'^x instead worked! Thank you so much for the pointer and

Jan 14

hemant gupta, Cas Cremers2

12/28/25

Need Help in Rules and Lemmas, its not showing in localhost

Hi Herman, I am not sure how you produced your code, but we should not be debugging LLM outputs. Some

unread,

Need Help in Rules and Lemmas, its not showing in localhost

Hi Herman, I am not sure how you produced your code, but we should not be debugging LLM outputs. Some

12/28/25

Yuheng Wen

11/25/25

Interpretating attach graph in --diff mode

Hi group! I am working with the observational equivalence feature in Tamarin for my protocol. I got

unread,

Interpretating attach graph in --diff mode

Hi group! I am working with the observational equivalence feature in Tamarin for my protocol. I got

11/25/25

Prashant Agrawal, Felix Linker4

11/4/25

Restrictions in diff-mode

Hi Prashant, I think my point is that you do require m1/m2 to be sent for the model to be

unread,

Restrictions in diff-mode

Hi Prashant, I think my point is that you do require m1/m2 to be sent for the model to be

11/4/25

何子林, Felix Linker2

9/24/25

Question about Modeling ECIES_MAC in Tamarin

Hi Hezl, You ask a very involved question about detailed aspects of a complex protocol. It is not

unread,

Question about Modeling ECIES_MAC in Tamarin

Hi Hezl, You ask a very involved question about detailed aspects of a complex protocol. It is not

9/24/25

Ardek Veri, Cas Cremers2

9/18/25

About non-termination

Hi all, There exists no criterion. Pragmatically though, after two days, I would personally start

unread,

About non-termination

Hi all, There exists no criterion. Pragmatically though, after two days, I would personally start

9/18/25

Daniel Zimmerman, Cas Cremers3

9/1/25

Minimization/Pruning of Proof Scripts?

Thanks for getting back to me! I have tried exactly what you suggested in the past, with varying

unread,

Minimization/Pruning of Proof Scripts?

Thanks for getting back to me! I have tried exactly what you suggested in the past, with varying

9/1/25

Daniel Zimmerman, Felix Linker3

8/7/25

A Question on Partial Deconstructions

Felix, That was very helpful, thanks. And what you said about partial deconstructions basically

unread,

A Question on Partial Deconstructions

Felix, That was very helpful, thanks. And what you said about partial deconstructions basically

8/7/25

Cas Cremers

8/6/25

Tamarin book now available from Springer Nature

Dear all, We are happy to report that physical copies of our Tamarin book have now started to ship

unread,

Tamarin book now available from Springer Nature

Dear all, We are happy to report that physical copies of our Tamarin book have now started to ship

8/6/25

Shrey Mukund

7/10/25

Help with introducing some equational theories

Dear All, I am trying to work on protocols to verify their security, and I am very new to Tamarin .

unread,

Help with introducing some equational theories

Dear All, I am trying to work on protocols to verify their security, and I am very new to Tamarin .

7/10/25

Daniel Zimmerman, Felix Linker4

6/19/25

Hang while Saturating Sources

As a quick follow-up, I decided after watching some verbose output to see if cutting down the

unread,

Hang while Saturating Sources

As a quick follow-up, I decided after watching some verbose output to see if cutting down the

6/19/25

William Harrison, Cas Cremers3

6/12/25

Examples from "Modeling and Analyzing ..." book?

Hi Bill and all, I've just made these available now on the book webpage: https://tamarin-prover.

unread,

Examples from "Modeling and Analyzing ..." book?

Hi Bill and all, I've just made these available now on the book webpage: https://tamarin-prover.

6/12/25

Nik Stuckenbrock

5/15/25

TLS 1.3 Tamarin Model

Hi, I'm currently working on the formal verification of TLS 1.3 build in Tamarin I found on [

unread,

TLS 1.3 Tamarin Model

Hi, I'm currently working on the formal verification of TLS 1.3 build in Tamarin I found on [

5/15/25

Cas Cremers, Alexandre Anzala-Yamajako3

5/2/25

Tamarin prover book draft now available for download!

Dear all, We have just released a new version (v0.9.5) of the Tamarin book, available at https://

unread,

Tamarin prover book draft now available for download!

Dear all, We have just released a new version (v0.9.5) of the Tamarin book, available at https://

5/2/25

Daniel Clark, … Petar Paradžik5

4/14/25

Tamarin building infinite chains of the same rule (similar to looping behaviour)

Thanks so much for that reply, it works perfectly. For future reference, that oracle deprioritises

unread,

Tamarin building infinite chains of the same rule (similar to looping behaviour)

Thanks so much for that reply, it works perfectly. For future reference, that oracle deprioritises

4/14/25

Daniel Zimmerman, … Simon BOUGET6

3/7/25

A Question about Adversary Capability

On Tuesday, March 4, 2025 at 4:57:46 PM UTC+8 Ralf Sasse wrote: For your protocol, the source for the

unread,

A Question about Adversary Capability

On Tuesday, March 4, 2025 at 4:57:46 PM UTC+8 Ralf Sasse wrote: For your protocol, the source for the

3/7/25

Daniel Zimmerman, Robert K3

2/19/25

SAPIC+ Channel Questions

On Wednesday, February 19, 2025 at 4:20:40 PM UTC+8 Robert K wrote: For secret channels, the

unread,

SAPIC+ Channel Questions

On Wednesday, February 19, 2025 at 4:20:40 PM UTC+8 Robert K wrote: For secret channels, the

2/19/25

Daniel Zimmerman, Felix Linker2

2/16/25

Confusing Message Derivation Check Failure with SAPIC+

Hi Dan, I helped implement this feature. Let me describe you by example what it does. Presume you

unread,

Confusing Message Derivation Check Failure with SAPIC+

Hi Dan, I helped implement this feature. Let me describe you by example what it does. Presume you

2/16/25

Daniel Zimmerman

2/14/25

Odd Error Message w/SAPIC+, state storage, and symmetric-encryption built-in

Hi! I've written a version of the symmetric Needham-Schroeder key exchange protocol in SAPIC+,

unread,

Odd Error Message w/SAPIC+, state storage, and symmetric-encryption built-in

Hi! I've written a version of the symmetric Needham-Schroeder key exchange protocol in SAPIC+,

2/14/25

rolando....@gmail.com

12/13/24

Postdoc position in formal methods for security and privacy

We seek to hire a full-time postdoctoral researcher in the area of formal methods for security and

unread,

Postdoc position in formal methods for security and privacy

We seek to hire a full-time postdoctoral researcher in the area of formal methods for security and

12/13/24

hua hua2

12/4/24

observational issue

Dear all, May be my description above is not clear,below is the specific example and description.

unread,

observational issue

Dear all, May be my description above is not clear,below is the specific example and description.

12/4/24

hua hua, Felix Linker6

11/26/24

help lemma

Dear Felix Thank you for your response,I think in my model R2 =\=> R1,so the help lemma not work.

unread,

help lemma

Dear Felix Thank you for your response,I think in my model R2 =\=> R1,so the help lemma not work.

11/26/24

Ralf Sasse, hua hua3

10/26/24

Re: [tamarin-prover] error result about Observational_equivalence

Thank you for your response. If I want to prove the unlinkability of the AKA protocol, meaning the

unread,

Re: [tamarin-prover] error result about Observational_equivalence

Thank you for your response. If I want to prove the unlinkability of the AKA protocol, meaning the

10/26/24

‍한윤선(대학원생-정보융합보안전공), Ralf Sasse2

8/31/24

Seeking advice to resolve server down while autoprove with 256GB RAM

Dear Yoonsun Han, Generally we would try to run the proof attempt without any --heuristic parameter,

unread,

Seeking advice to resolve server down while autoprove with 256GB RAM

Dear Yoonsun Han, Generally we would try to run the proof attempt without any --heuristic parameter,

8/31/24

Joshua “Sync” Singla, Daniel Clark2

8/28/24

Converting a persistent fact to a linear fact causes Tamarin precomputation to be too much

Could you provide an example model that has your issue? It'll be almost impossible to help

unread,

Converting a persistent fact to a linear fact causes Tamarin precomputation to be too much

Could you provide an example model that has your issue? It'll be almost impossible to help

8/28/24

mmhuang, Felix Linker3

8/14/24

Error: tamarin-prover: fd:17: commitBuffer: invalid argument (invalid character)

It worked! Thanks again. 在2024年8月14日星期三 UTC+8 23:24:17<linke...@gmail.com> 写道： Hi, Can you try

unread,

Error: tamarin-prover: fd:17: commitBuffer: invalid argument (invalid character)

It worked! Thanks again. 在2024年8月14日星期三 UTC+8 23:24:17<linke...@gmail.com> 写道： Hi, Can you try

8/14/24

Guillaume Nibert, … Ralf Sasse4

8/12/24

Calculation of the number of partial deconstructions via CLI only

Dear Reynaldo, That would of course be great! Guillaume, maybe you can use the version of Reynaldo in

unread,

Calculation of the number of partial deconstructions via CLI only

Dear Reynaldo, That would of course be great! Guillaume, maybe you can use the version of Reynaldo in

8/12/24