tamarin-prover

Contact owners and managers

1–30 of 201

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

Homepage: http://tamarin-prover.com/

Source code: https://github.com/tamarin-prover/tamarin-prover

Issue tracker: https://github.com/tamarin-prover/tamarin-prover/issues

Manual: https://tamarin-prover.com/manual/

0 selected

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

Aug 31

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,

Aug 31

Joshua “Sync” Singla, Daniel Clark2

Aug 28

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

Aug 28

mmhuang, Felix Linker3

Aug 14

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

Aug 14

Guillaume Nibert, … Ralf Sasse4

Aug 12

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

Aug 12

mmhuang, Ralf Sasse2

Aug 6

generate n values and randomly select one, how to model?

Hi, Very abstractly: is what comes out of this a random value? If so, just using a Tamarin fresh

unread,

generate n values and randomly select one, how to model?

Hi, Very abstractly: is what comes out of this a random value? If so, just using a Tamarin fresh

Aug 6

mmhuang, Felix Linker2

Aug 5

what does "/* from formulas */" mean

Hi Huang, „From formulas“ means that either (a) parts of your initial lemma, (b) an auxiliary lemma,

unread,

what does "/* from formulas */" mean

Hi Huang, „From formulas“ means that either (a) parts of your initial lemma, (b) an auxiliary lemma,

Aug 5

Jun 28

Feedback Wanted: New Feature - Editing Tamarin Lemmas in the GUI

Hi everyone, Ralf Sasse and I currently supervise a student, Alice La Porta, who implemented a new

unread,

Feedback Wanted: New Feature - Editing Tamarin Lemmas in the GUI

Hi everyone, Ralf Sasse and I currently supervise a student, Alice La Porta, who implemented a new

Jun 28

Jun 13

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

Hi, I've got the attached simplified model, where: 1. The Server sends its cert(certS) to the

unread,

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

Hi, I've got the attached simplified model, where: 1. The Server sends its cert(certS) to the

Jun 13

Daniel Clark, Felix Linker2

May 30

Ordering of cases

Hi Dan, The order is alphabetical and you cannot influence it, unfortunately. Happy proving, Felix

unread,

Ordering of cases

Hi Dan, The order is alphabetical and you cannot influence it, unfortunately. Happy proving, Felix

May 30

Simon BOUGET, Cas Cremers3

May 19

What is an "impossible chain"?

Hi Cas, Thanks for the explanation. There was indeed a contradiction a few steps further, due to a

unread,

What is an "impossible chain"?

Hi Cas, Thanks for the explanation. There was indeed a contradiction a few steps further, due to a

May 19

Ali S, Daniel Clark3

May 14

Diffie-Hellman with Symmetric Encryption Execution Problem

Dear Dan, Thank you so much for your detailed explanation, your answer has been very helpful in

unread,

Diffie-Hellman with Symmetric Encryption Execution Problem

Dear Dan, Thank you so much for your detailed explanation, your answer has been very helpful in

May 14

May 14

Unable to verify lemma with interactive GUI

Hello all, I'm creating a model that includes a high-level abstraction of secret sharing/message

unread,

Unable to verify lemma with interactive GUI

Hello all, I'm creating a model that includes a high-level abstraction of secret sharing/message

May 14

Leo, Felix Linker2

May 3

List implementation with <> doesn't work

Hi Leo, I suggest you use a constant to denote the empty list, eg <head, 'nil'>. <…

unread,

List implementation with <> doesn't work

Hi Leo, I suggest you use a constant to denote the empty list, eg <head, 'nil'>. <…

May 3

May 2

Looping behaviours when using counters with natural-numbers and GreaterThan restrictions

Hi, tl;dr: How can I model counters using natural-numbers and a GreaterThan restriction such that

unread,

Looping behaviours when using counters with natural-numbers and GreaterThan restrictions

Hi, tl;dr: How can I model counters using natural-numbers and a GreaterThan restriction such that

May 2

May 1

Learning Sapic+

Hi guys, I'm decently fluent in Tamarin, and the new Sapic+ looks very promising (especially

unread,

Learning Sapic+

Hi guys, I'm decently fluent in Tamarin, and the new Sapic+ looks very promising (especially

May 1

justin, Felix Linker2

Apr 29

Questions regarding KD and KU facts

Hi Justin, Tamarin uses a specific type of reasoning about adversary knowledge to avoid infinite

unread,

Questions regarding KD and KU facts

Hi Justin, Tamarin uses a specific type of reasoning about adversary knowledge to avoid infinite

Apr 29

Daniel Clark, … Simon BOUGET5

Apr 27

Tamarin chooses to find complex trace before simple trace

Hi Simon, That was actually super helpful, it seems obvious now you say it, but it gave me a bunch of

unread,

Tamarin chooses to find complex trace before simple trace

Hi Simon, That was actually super helpful, it seems obvious now you say it, but it gave me a bunch of

Apr 27

Apr 26

Different Channel Models in SAPIC+

Hi all, In the manual, section Advanced Features, different channel models are described using

unread,

Different Channel Models in SAPIC+

Hi all, In the manual, section Advanced Features, different channel models are described using

Apr 26

Syafrizal Ananta Adhitya

Apr 23

Modelling hash function

Hi, i'm just learning tamarin prover and have a question for protocol modelling. How to verify

unread,

Modelling hash function

Hi, i'm just learning tamarin prover and have a question for protocol modelling. How to verify

Apr 23

Ali S, … Cas Cremers5

Mar 29

Question about the asymmetric-encryption example

Hi all, "secret_B" is definitely an extremely relevant property. It establishes the

unread,

Question about the asymmetric-encryption example

Hi all, "secret_B" is definitely an extremely relevant property. It establishes the

Mar 29

Steven Gong, … Simon BOUGET6

Mar 26

Newbie Question on Syntax Error

Hi Steven, The error message clearly tells you that the problem is the exponentiation on line 35 ((

unread,

Newbie Question on Syntax Error

Hi Steven, The error message clearly tells you that the problem is the exponentiation on line 35 ((

Mar 26

Sergiu Bursuc, Jannik Dreier3

Mar 12

manual variants problem

The diff file fails in _command line_ mode. (Sorry!) On 12/03/2024 17:01, Jannik Dreier wrote: >

unread,

manual variants problem

The diff file fails in _command line_ mode. (Sorry!) On 12/03/2024 17:01, Jannik Dreier wrote: >

Mar 12

Marco Calipari, … Ralf Sasse6

Mar 4

Can I reuse a wrong result to prove another lemma?

To reiterate what Jannik said: It does not matter if the reuse lemma is true or false. It also does

unread,

Can I reuse a wrong result to prove another lemma?

To reiterate what Jannik said: It does not matter if the reuse lemma is true or false. It also does

Mar 4

Nazz, Cas Cremers3

Feb 23

regarding writing an oracle: 5G-AKA: SAPIC+: Tamarin

Many thanks for your response and your suggestion, Prof Cas! Kind Regards, Naz On Friday, February 23

unread,

regarding writing an oracle: 5G-AKA: SAPIC+: Tamarin

Many thanks for your response and your suggestion, Prof Cas! Kind Regards, Naz On Friday, February 23

Feb 23

Nazz, … Felix Linker10

Feb 12

SAPIC+ Related Issue: Execution is getting killed

Hi Felix, Thank you very much. I will try that. Best Regards, Nazz On Monday, February 12, 2024 at 7:

unread,

SAPIC+ Related Issue: Execution is getting killed

Hi Felix, Thank you very much. I will try that. Best Regards, Nazz On Monday, February 12, 2024 at 7:

Feb 12

Nazz, Felix Linker3

Feb 2

Regarding SAPIC+

Hi Felix, Thank you for your response. I will be posting my issues regarding SAPIC+ here. I hope to

unread,

Regarding SAPIC+

Hi Felix, Thank you for your response. I will be posting my issues regarding SAPIC+ here. I hope to

Feb 2

Jan 26

Observational Equivalence and Xor

Dear all, When I was using Tamarin to prove unlinkability, I found that it wouldn't terminate.

unread,

Observational Equivalence and Xor

Dear all, When I was using Tamarin to prove unlinkability, I found that it wouldn't terminate.

Jan 26

Guillaume Nibert

Jan 11

Observational Equivalence: attack based on the recognition of two terms

Dear Tamarin Team, I am still exploring the Basin et al's paper. There is an example on pairs of

unread,

Observational Equivalence: attack based on the recognition of two terms

Dear Tamarin Team, I am still exploring the Basin et al's paper. There is an example on pairs of

Jan 11

Guillaume Nibert, Marco Calipari7

Jan 10

Observational Equivalence - Privacy for voting manual example

Hello, Thanks for these explanations! Regarding the pairs example in the paper (page 4), the

unread,

Observational Equivalence - Privacy for voting manual example

Hello, Thanks for these explanations! Regarding the pairs example in the paper (page 4), the

Jan 10

hua hua, Marco Calipari5

Jan 9

question about observational equivalence

Dear all, But ina real protocol, the HN cannot authenticate the random numbers sent by the UE.

unread,

question about observational equivalence

Dear all, But ina real protocol, the HN cannot authenticate the random numbers sent by the UE.

Jan 9

Search

Clear search

Close search

Google apps

Main menu