Groups
Sign in
Groups
tamarin-prover
Conversations
About
Send feedback
Help
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/tamar
in-prover/tamarin-prover
Issue tracker:
https://github.com/ta
marin-prover/tamarin-prover/is
sues
Manual:
https://tamarin-
prover.com/manual/
Mark all as read
Report group
0 selected
Leo
,
Felix Linker
2
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
Daniel Clark
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
Simon BOUGET
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 Linker
2
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 BOUGET
5
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
Simon BOUGET
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 Cremers
5
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 BOUGET
6
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 Dreier
3
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 Sasse
6
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 Cremers
3
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 Linker
10
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 Linker
3
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
hua hua
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 Calipari
7
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 Calipari
5
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 Linker
2
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
hua hua
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
Marco Calipari
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
Marco Calipari
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 Dreier
8
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 Dreier
4
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 Sasse
5
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
Cas Cremers
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 Sasse
2
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
, …
Jan
5
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
Felix Linker
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 Linker
2
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