tamarin-prover

Contact owners and managers

1–30 of 190

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

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

Marco Calipari, Felix Linker2

12/23/23

How come that the secure channel models introduce partial deconstructions

Hi Marco, In my experience, secure channels modelled as custom in/out rules often lead to partial

unread,

How come that the secure channel models introduce partial deconstructions

Hi Marco, In my experience, secure channels modelled as custom in/out rules often lead to partial

12/23/23

12/20/23

Beginners often face difficulties when learning tamarin-prover to handle complex protocols.

Dear all I hope the manual provides more information on how to write proof strategies for complex

unread,

Beginners often face difficulties when learning tamarin-prover to handle complex protocols.

Dear all I hope the manual provides more information on how to write proof strategies for complex

12/20/23

12/19/23

Tamarin interactive mode performance issue

Hello group! I am trying to run a complicated proof for my master thesis, and since I am still in the

unread,

Tamarin interactive mode performance issue

Hello group! I am trying to run a complicated proof for my master thesis, and since I am still in the

12/19/23

12/11/23

Tamarin's Performance botleneck

Hello group, What is the biggest bottleneck regarding the performances of Tamarin? As far as I

unread,

Tamarin's Performance botleneck

Hello group, What is the biggest bottleneck regarding the performances of Tamarin? As far as I

12/11/23

gilcu3, … Jannik Dreier8

12/8/23

[question] builtin xor equational theory and partial deconstructions

Dear Guillaume, I suspect that simply removing a variant will cause the verification to be incorrect.

unread,

[question] builtin xor equational theory and partial deconstructions

Dear Guillaume, I suspect that simply removing a variant will cause the verification to be incorrect.

12/8/23

Denis D'Ambrosi, Jannik Dreier4

12/8/23

Precomputation halts when introducing a custom XOR

Dear Denis, > I have just read your article about introducing XOR into Tamarin and now > it

unread,

Precomputation halts when introducing a custom XOR

Dear Denis, > I have just read your article about introducing XOR into Tamarin and now > it

12/8/23

Guillaume Nibert, Ralf Sasse5

12/8/23

Questions about XOR, solving lemmas and partial deconstructions.

Dear Ralf, Thank you for this clarification. Best regards, Guillaume Nibert Le mardi 21 novembre 2023

unread,

Questions about XOR, solving lemmas and partial deconstructions.

Dear Ralf, Thank you for this clarification. Best regards, Guillaume Nibert Le mardi 21 novembre 2023

12/8/23

12/8/23

Changing user policy due to spam

Dear all, I have just changed the user policy: previously, anyone could join the group and

unread,

Changing user policy due to spam

Dear all, I have just changed the user policy: previously, anyone could join the group and

12/8/23

hua hua, Ralf Sasse2

11/23/23

Proof Strategies about 5GAKA

The easiest way to see what the oracle does is to run two instances of Tamarin on the same file at

unread,

Proof Strategies about 5GAKA

The easiest way to see what the oracle does is to run two instances of Tamarin on the same file at

11/23/23

Lelio Brun, … Jan5

11/20/23

Case distinctions order

@Jan, It might be the same kind of problem I'm facing indeed, I'll try that as well, it's

unread,

Case distinctions order

@Jan, It might be the same kind of problem I'm facing indeed, I'll try that as well, it's

11/20/23

11/14/23

Re: [tamarin-prover] cyclic behaviour in my proof.

Hi Marco, I haven't looked at your file, but my understanding is the following… When you see the

unread,

Re: [tamarin-prover] cyclic behaviour in my proof.

Hi Marco, I haven't looked at your file, but my understanding is the following… When you see the

11/14/23

Adam, Felix Linker2

10/24/23

Questions about nat numbers/counters

Hi Adam, I did not work on the natural numbers theory, but my understanding is that you can only

unread,

Questions about nat numbers/counters

Hi Adam, I did not work on the natural numbers theory, but my understanding is that you can only

10/24/23

Search

Clear search

Close search

Google apps

Main menu