Explain proof export and import feature

On Debian, sudo apt-get install pandoc does not suffice: you also need pandoc-citeproc.

On OSX, brew install pandoc does not suffice: you also need pandoc-citeproc.

Perhaps this should be in README.md?

Currently the manual does not explicitly explain the wellformedness conditions for protocol rules (in particular that one should not use K/KU/KD facts), nor does it explain the meaning of K/KD/KU facts in general.

Hi all, Happy New Year :-)

I think there's an error in Page 2 of the manual about installation and installing code editors; in the Sublime Text section it says:

Pull directory into Packages folder.
SSH: git pull [email protected]:tamarin-prover/editor-sublime.git
HTTPS: git pull https://github.com/tamarin-prover/editor-sublime.git

I think this should be git clone not git pull on both lines!

(The installation text in https://github.com/tamarin-prover/editor-sublime/blob/master/README.md is correct)

Thanks,

Martin

Some of the screenshots (particularly in Section 6) were taken before the renaming to raw/refined sources and still show Typed/Untyped case distinctions. The ones that focus on that have been replaced already.

Retake screenshots on new version.

You can quite easily get tamarin with GUI working under Windows 10. You have to use the Windows Subsystem for Linux (https://docs.microsoft.com/de-de/windows/wsl/install-win10).

This was my workflow:

$ wsl
$ sudo apt-get update
$ sudo apt-get graphviz maude
$ wget https://github.com/tamarin-prover/tamarin-prover/releases/download/1.4.1/tamarin-prover-1.4.1-linux64-ubuntu.tar.gz
$ tar -xvzf tamarin-prover-1.4.1-linux64-ubuntu.tar.gz
$ ./tamarin-prover interactive .

I'm happy to add this to the introduction (https://github.com/tamarin-prover/manual/blob/master/src/002_installation.md) if you'd like.

Semi-Persistent Facts

I would like to share some knowledge on how to model semi-persistent facts. Maybe they find their way into the manual at some point or (ideally) they are implemented directly in Tamarin.

Use Case

While persistent facts are read-only-and-never-change and linear facts are destroy/consume-on-read, we often need a thing inbetween. For example modeling a storage cell with an identifier ~id where we sometimes want to read the value but sometimes also want to change it.

Implementation with Linear Facts (not recommended)

With that, the exact same Fact has to be inserted again in the Read-rule such that it is not destroyed when reading it:

rule Init:  [Fr(~id), In(val)]           --> [Cell(~id, val)]
rule Read:  [Cell(~id, val)]             --> [Cell(~id, val), Out(val)]
rule Write: [Cell(~id, oldVal), In(val)] --> [Cell(~id, val)]

This has one big disadvantage: Often in proofs, we need to find the source of a value. For example "where did that secret key come from". If we have some Read-rules between writing and the current point, Tamarin is easily trapped into a loop or has to unfold many Read-steps before finding the source - the rule where the value was actually written.

Implementation with Persistent Facts and Restrictions

The other idea is to use persistent facts as follows:

rule Init:
    [Fr(~id), In(val)]
    --[WriteCell(~id, val)]->
    [!Cell(~id, val)]

rule Read:
    [!Cell(~id, val)]
    --[ReadCell(~id, val)]->
    [Out(val)]

rule Write:
    [In(~id), In(val)]
    --[WriteCell(~id, val)]->
    [!Cell(~id, val)]

restriction StorageCell:
    "∀ id  c #i.  ReadCell(id, c)@i
    ==>  ∃   #j. WriteCell(id, c)@j ∧ j<i
      ∧ ¬∃ d #k. WriteCell(id, d)@k ∧ j<k ∧ k<i"

Note that we have to add action facts to the rules now such that the restriction can talk about them.
The restriction then ensures that when reading from a cell, there has to be a WriteCell with the same value which was not overwritten.

That approach works but has some caveats. Notably, the restriction will spawn a WriteCell goal for each ReadCell. This can cause looping problems if ReadCell and WriteCell are in the same rule. But even without that, it creates additional goals which are not needed as there is already a goal that aims to satisfy the source of the persistent fact !Cell(...). A better way to write what we want in a restriction is actually:

restriction StorageCellBetter:
    "∀ id c d #i #j #k. WriteCell(id, c)@i
                      ∧ WriteCell(id, d)@j ∧ i<j
                      ∧  ReadCell(id, c)@k ∧ j<k
    ==> ∃ #l.           WriteCell(id, c)@l ∧ ¬l<j ∧ l<k"

Here we let the persistent fact goals for !Cell(...) do their job until a "bad" situation occurs where we have a second WriteCell@j inbetween a ReadCell@i and a WriteCell@k. In that case we require a third WriteCell@l which is after the second WriteCell@j (or equal to it in case of c=d).

This way of writing the restriction is much less invasive as it triggers only if we have a "bad" situation to "heal" it. Thus, it does not pollute our goals.

Separating cells

Quite often, we want to store multiple values grouped together. For example on a device ~id we store a long term key ltk and an ephemeral key eph which is changed each protocol iteration. Then we can model this as Cell(~id, ltk, eph). However, if we want to find the source of the ltk, we would have to trace it back trough all changes of eph which usually requires to write (possibly multiple) loop breaker lemmas.

Instead we can model the same behaviour with separate facts LtkCell(~id, ltk) and EphCell(~id, eph) - deciding upon need which one is persistent, semi-persistent or linear. That has the advantage that it is now irrelevant how often we change eph between writing and reading ltk because we directly jump to the source of ltk. Note that you then need a restriction for each Cell name which would be StorageLtkCell and StorageEphCell in this case.

Be aware that this separation has disatvantages as well - especially when trying to prove connections between two separated values. And writing a fitting oracle might be harder because you have to deal with more goals. However, I found that it helps especially for more complex protocols where I had to write oracles anyways.

A Direct Implementation in Tamarin

There are multiple ways of dealing with the problems of semi-persistence and separation and I'm thinking about ways to implement them. Things that I thought about:

• Adding the action facts is quite nasty and a source of error if they become out of sync with the persistent facts when changing the model
• Letting the user write the restrictions is a source of error
• Thus, it would be nice to have a new type of fact (maybe called storage-fact) which does effectively what we do with persistent facts and restrictions.
  • If we use a constraint rewriting rule for that (instead of a restriction) we can directly refer to the rule that satisfied the premise fact instead of using an existential quantification as a hack to refer to it
• We can automatically detect linear facts that should be rewritten as storage facts and hint the user
• Automatically (internally) splitting facts is harder because it is not always beneficial - though it is definitely worth looking into them. One thought was to write Cell(~id, a, b, _, _, _) if only a and b are read and the others are unimportant for that specific rule.

In the section "Reasoning about Exclusivity: Facts Symbols with Injective Instances" it would be helpful to note that one can view which facts are injective. I found this feature accidentially.

They can be showed by clicking on "Multiset rewriting rules and restrictions".

There are a lot of note and edge types in the GUI graphs. The meaning of some is relatively straightforward, but that's not the case for all of them. We should document them.

Need to document the
TAMARIN_NO_MAUDE_VARIANTS
environment variable which can be set to use the old, Tamarin-internal variant computation. This might be needed for reproduction of older examples.

In the update where
005_protocol-specification.md
got split into
005_protocol-specification-rules.md
and
006_protocol-specification-processes.md
the references to each of the files seem to be not properly updated.

As an example, on the organisation section of https://tamarin-prover.github.io/manual/book/001_introduction.html
chapter 7 is still linked as https://tamarin-prover.github.io/manual/book/006_property-specification.html#sec:property_specification.
However, the new link should be
https://tamarin-prover.github.io/manual/book/007_property-specification.html#sec:property_specification.

Illustrate use for counting/comparisons and (multi)subset.

chapter 5 writes about persistent facts:

Modeling this using linear facts would require that every rule that has such a fact in the left-hand-side, also has an exact copy of this fact in the right-hand side. While there is no fundamental problem with this modeling, it is inconvenient for the user and it also might lead Tamarin to explore rule instantiations that are irrelevant for tracing such facts.

Is this really true? From my experience it looks like I get in infinite loops doing this, while persistent facts do not get me in this awful scenario.

From discussion with @katrielalex it seems like the bang also has the property that when Tamarin looks for the source of a persistent fact, it will only pull up the rule where the instantiation of this persistent fact happened.

The sapic-used heuristics p and P are not documented (or even mentioned) in the manual at all. This should be done.

The diffie-hellman equational theory now includes a "DH_neutral" symbol, this does not appear in the manual though: ( at least not here https://tamarin-prover.github.io/manual/develop/book/004_cryptographic-messages.html ).

It often appears in trivial attacks and I think for users it would be useful if it was mentioned in the theory definition. This is also true for the release version!

This is more of a clarification (and support) thread, rather than an actual issue, apologies for that.

In the Common Restrictions section of the manual, two of the common restrictions explained are Unique and OnlyOnceV.
However, these two seem identical to me (modulo renaming). Q1: Am I correct?

Q2: Is it also correct to say that both these restriction could be called AtMostOnce? (given that the rules carrying these facts may appear either 0 or 1 time within a trace).

Also (here comes the support request), to enforce a given rule X to be instantiated ExactlyOnce within every trace, I'm using the following restriction:

restriction exactlyOnceX:
" Ex #i . ExactlyOnceX()@i 
  & All #i #j . ExactlyOnceX()@i & ExactlyOnceX()@j ==> #i=#j "

However, I was unable to write a more general version that is parameterized by a specific instantiation of a variable, as that seems to introduce an invalid formula (universal quantifier without toplevel implication).

// Not allowed
restriction exactlyOnce: 
" All v . ( Ex #i . ExactlyOnce(v)@i ) & ( All #i #j . ExactlyOnce(v)@i & ExactlyOnce(v)@j ==> #i=#j ) "

Q3: Would you confirm that the only way to enforce a rule to appear exactly once in a trace is by my first restriction?
(And there is no way to have a more general version like my second restriction?)

Thanks!

The compiled PDF at https://tamarin-prover.github.io/manual/tex/tamarin-manual.pdf states on page 3 (Contents) that the introduction starts on page 5. Clicking it leads to the introduction, but that is on page 7. So, the link works correctly, but the numbers shown in the TOC are off by 2.

The same happens for the Installation chapter (2) and the Modeling issues chapter (8), so this is throughout the document.

--stop-on-trace has no documentation beyond the output of --help

Normally Travis recompiles the HTML and PDF versions of the manual and updates the homepage on every push or merge.

Currently this does not work any more. I fixed the Travis integration and pandoc problems (by replacing outdated versions of pandoc and Ubuntu), however the push to the gh-pages still fails (see https://travis-ci.com/github/tamarin-prover/manual/builds/183856234). Can anybody knowledgeable help out? @katrielalex ?

Add description of XOR support into the manual.

The sublime text 3 plugin was moved from a private repository to the tamarin-prover repository under https://github.com/tamarin-prover/editor-sublime

The manual https://tamarin-prover.github.io/manual/book/002_installation.html still points to the old non-existing repository and needs to be updated.

Limitations could also point to specific primitives that are currently hard to handle (e.g. xor).

Add description of the flag

--prove[=LEMMAPREFIX]

which allows to specify which lemmas should be verified on the command line.

The example lemma for injective authentication (https://github.com/tamarin-prover/manual/blame/59525bd2c117da7acf21e58412ea209d7bc02522/src/007_property-specification.md#L783) uses upper case "A" and "B" as the two agents, but all the other authentication lemmas use the lower case "a" and "b". This becomes super confusing because the description specifically mentions that "a"/"b" are the agents, and "A"/"B" are the roles of those agents, which (as far as I understand) is not the intention.

I'm happy to make this change myself, I'd just like a vague confirmation that it wasn't the intention to be referring to the role in the lemma.

At the end of section 6 we first describe secrecy including an example, and then give the abstract lemmas for the authentication hierarchy including honesty requirements. It would be very helpful to add at least one (or possibly differentiating) example theory that uses these actions.

On Debian, make (or minimal example pandoc --bibliography=src/manual.bib src/005_protocol-specification.md) gives me a citeproc error:

> pandoc --bibliography=src/manual.bib src/005_protocol-specification.md 
pandoc-citeproc: "stdin" (line 9, column 2):
unexpected "i"
expecting "c", "C", "p", "P", "s" or "S"
pandoc: Error running filter pandoc-citeproc

This corresponds to the i of @inproceedings in the bibtex; Googling seems to indicate that @inproceedings isn't supported. Perhaps I have an old version of bibutils?

pandoc version = 1.12.2.1
pandoc-citeproc version = 0.2

For example, use tamarin-prover +RTS -N1 -RTS to use only one thread, or tamarin-prover +RTS -Nx -RTS for x in general.

The following text is added to the end of Section 9, both in PDF and HTML, but is not in the source file:

<!– ### functions ### function-> where does it go? doesn have support: local to rule with “let”–!><!– Using rewrite rules to ‘share’ ——————————TODO: Katriel? –!>

Looking for ideas how to fix it. This was reported by @jlallemand - thanks!

The title says it all, really :)

After a decade long transition, python2 is phased out and not included, e.g. in mac os anymore. We should port this little script to not make producing the manual unnecessarily difficult. Unfortunately, I don't speak in split tongues.

In page 75 (Tamarin's manual), in the authentication section, the formalization given of Lowe's specifications does not correspond to the text nor to Lowe's definition itself. For example, "we say that a protocol guarantees to an initiator aliveness of another agent if, whenever A (acting as initiator) completes a run of the protocol, apparently with responder B, then B has previously been running the protocol."

Whereas in "lemma aliveness":
lemma aliveness:
"All a b t #i. Commit(a, b, t)@i ==> (Ex id #j. Create(b, id) @j) ... "

There is no condition over i and j (no condition about the order of the actions). According to the text and to the definition given by Lowe, "B has previously been running the protocol", so at least one should test if j < i ( & (#j < #i) in the lemma).

My comment applies to Weak-Agreement and Non-Injective agreement as well.

While programming a parser for the Tamarin theory files, I came across some problems in the Syntax Description chapter of the manual where the grammar seems different from what Tamarin could parse :

• In the rule lemma, proof_skeleton should probably be optional

• The grammar says that the list of facts between brackets must be non-empty but in Tamarin it is possible to have rules without facts

   simple_rule := 'rule' [modulo] ident [rule_attrs] ':'
       				[let_block]
       				'[' facts ']' ( '-->' | '--[' facts ']->') '[' facts ']'

  Is probably something like

   simple_rule := 'rule' [modulo] ident [rule_attrs] ':'
   	[let_block]
   	'[' [facts] ']' ( '-->' | '--[' [facts] ']->') '[' [facts] ']'

  Or facts could be rewritten as

   facts := [ fact (',' fact)* ]

• No description of hexcolor : (done in #105 ✅)
  hexcolor which is used in the rule rule_attr is not defined explicitly in EBNF style.
  The manual only says A color is represented as a triplet of 8 bit hexadecimal values optionally preceded by '#'
  but after some testing I found out that Tamarin seems to accept some files where hexcolor is between simple quotes,
  making all #ffffff, #FFFFFF, 'ffffff, 'FFFFFF', '#ffffff' and '#FFFFFF' valid syntaxes.
  Maybe consider adding something like this to the manual

   hexcolor := "'" ["#"] hex "'"
   	| ["#"] hex

• multterm is used instead of tupleterm in nary_app

• No description of preprocessor directives :
  Tamarin has some preprocessing capabilities (support for #ifdef, #else, #endif, #include) but those are not present in the grammar

• No description of predicates :
  The syntax description for predicates and _restrict() is also not present in the grammar

• There are some missing built-in names (eg. locations-report)

Also document associated errors, and Tamarin's requirements for user-defined equational theories (convergence).

See discussion here: tamarin-prover/tamarin-prover#181

The Homebrew/Linuxbrew formula for Tamarin has moved from homebrew/science/tamarin-prover to brewsci/science/tamarin-prover.

TL;DR: Could someone pretty please add a formal licence to the manual? :-)(Preferably/hopefully/ideally something like GPLv3 as per the rest of Tamarin).

The Wikipedia page for Tamarin has sadly (erroneously) been marked for deletion due to alleged "copyright violation"; they are correct in pointing out that the wiki article text quotes a couple of paragraphs of the manual verbatim, as I thought it was well written and useful content.

It is my belief that the manual was written and released under an open source licence (same as Tamarin itself, hence the repo being publicly available here on GitHub), and that this use of the text is not a copyright violation. If I can prove that the content is open source, this issue goes away.

To resolve this and any future issues, would it be possible to include a formal LICENCE file (preferably licensing it as something like GPLv3, although obviously whatever you think most suitable!) within this public repo, so that I can demonstrate its open source status to the Wikipedia administrators? I really don't want my lovely article to be deleted!

Thanks, and hope you've all had a lovely Christmas / holiday period.

Martin

P.S. I assume the LICENCE.highlight.js is a licence for highlight.js or other such software used to create the manual, and not the the text of the manual as a whole!

TL;DR: Please add at least one original sentence each to the wikipedia article!

So this isn't strictly an issue for the manual, but I thought I'd flag it here to make people aware.

Sadly, some heartless wikipedia editor has gone through and entirely gutted the Wikipedia article on Tamarin, citing the (sadly correct) fact that the CC BY-NC-SA licence that the manual is released under isn't strictly compatible with Wikipedia's requirement (they don't allow the No Commercial bit).
To add insult to injury, having gutted the article, they've then slapped a great big 'may not meet notability requirements' tag on it, which is patently false, but they can justify it because the person removed all the content demonstrating notability… (angry reacts only).

PLEASE oh wonderful people of Tamarin-land, could I beg you to all spend just FIVE minutes today or tomorrow, writing (say) one sentence each on the page? If you can cite a source for it, even better. Or, perhaps just link to a major paper that used Tamarin (to show utility / notability)? I don't care what; it doesn't matter if the content is later merged or edited, but just any useful (non-copyrighted, originally written material especially for this page) would be amazing.

Thank you!

Martin

Update the manual to reflect the integration of SAPIC, including installation and execution

The manual currently explains guardedness only in terms of actions, but omits the case of quantified equations. Notably, these don't need binding to an action, but the quantified variables should only occur on one side of the equation. (Cf. e.g. the definition in Benedikt's thesis)

Currently, the "Download" button is explained in the middle of a paragraph of the initial example, and this is the only place it is mentioned.

Being able to download, and replay, proofs is an important feature though that deserves better explanation. Probably should additionally get its own heading to help readers find it: "Storing proofs", "Storing (partial) proofs", "Storing (partial) proofs and reloading" or something like that, and then a bit more about the reloading process.