We should adapt the space-based indent to the space that is lost due to not using a fixed-width font in the GraphViz output.

A typical graph contains ~x.313, ~y.444, ~z.236, $R.11. It is cumbersome for a human to match them up and to remember which one he has already seen somewhere else in the graph - and image scrolling is usually necessary.

One solution, which I have also been using in Scyther, is to normalize these numbers when displaying the graphs. In particular:

Let I be the set of 'base' identifiers (in the above: ~x, ~y, ~z, $R).
Let occurs(i) be the set of instances of i in (the displayed part of) the graph.
Let #(i) be the number of instances in (the displayed part of) the graph, e.g. for a graph with occurs(i) = { i.313, i.400, i.600 } we have #(i) = 3.

for all identifiers i in I:
  if #(i) = 1
  then replace occurs(i)[0] by i
  else
    cnt = 1
    for x in occurs(i):
      replace x by 'i.cnt'
      cnt += 1

This would make at least one human happier.

This avoids users being confused by having no further clickable goals.

This is a simple, but very useful first step towards #14. It entails changing the theory summary.

Use a different arrow type for persistent and linear arrows.

For example JKL_TS3_2008 hardcodes '1' and '2' and it it seems like this should be the sorted identities.

It would also be cool to have some more finished and documented protocol models that we can publish with the tool in order to get our users up to speed more easily. I'm thinking TLS handshake, NSL3, minimal wrapping example with a comment on our future work (induction invariants).

As indicated by the profiling at the end of February, we spend more than 50% of the proof construction time on normalizing the terms due to our reliance on maude for this task. We should see a large speedup by implementing this functionality directly in Haskell.

Alternatively, we could go crazy and define 'A' to try subsequent autoproves for all lemmas.

We now have 'a', but not 'A'.

The current term output in /devel has for multi-line items typically a last line that consists only of closing brackets. I would join such a set of closing brackets up with the previous line, saving a line.

If Tamarin is started in interactive mode, but the browser does not support Javascript, the layout collapses to a mess without warning.

This can occur also for recent browsers with Javascript-disabling extensions (e.g. noscript).

In this case, we should give the user a fair warning instead of letting him guess what the cause of the broken page is.

@meiersi : the cabal install file refers to MANUAL (missing) and to Tutorial.spthy in /stable (missing; possible renaming of UserGuide.spthy)

Benedikt has some further ideas on how to speed this up.

i.e., fix the issue noted below.

Yes, this helps. The real cause is that you don't have alex installed, which we can get either via Ubuntu's package repo or via cabal install. I'll add it to the installation instructions.

2012/4/5 Cremers Cas [email protected]:

Hi Simon:

I tried (something) like you suggested:

cas@doekoe:$ cabal install bytestring-lexing --reinstall --flag=reinstalls
Resolving dependencies...
Configuring bytestring-lexing-0.4.0...
cabal: The program alex version >=2.3 is required but it could not be found.
cabal: Error: some packages failed to install:
bytestring-lexing-0.4.0 failed during the configure step. The exception was:
ExitFailure 1
cas@doekoe:$

Hope this helps,

Cas

On Wed, Apr 4, 2012 at 13:54, Simon Meier [email protected] wrote:

Hi Cas,

thanks for the input.

2012/4/4 Cremers  Cas [email protected]:

Hi guys,

I did a clean install on my Precise Pangolin beta according to the web
page. Here's my experience:

zlib-0.5.3.3 failed during the configure step. The exception was:
ExitFailure 1
zlib-bindings-0.0.3.2 depends on zlib-0.5.3.3 which failed to install.
zlib-conduit-0.2.0.1 depends on zlib-0.5.3.3 which failed to install.
make: *** [install] Error 1

Rereading the webpage, I noticed the fairly hidden dependency on
zlib1g-dev. Why don't we simply add this to the step 1 install line?

Added your fix. This makes sense as zlib1g-dev are external C-header files.

Then, proceeding, I got:

cabal: Error: some packages failed to install:
bytestring-lexing-0.4.0 failed during the configure step. The exception was:
ExitFailure 1
tamarin-prover-0.3.0.0 depends on bytestring-lexing-0.4.0 which failed to
install.
warp-1.1.0.1 depends on bytestring-lexing-0.4.0 which failed to install.
make: *** [install] Error 1

It took me a bit of googling to find I needed:

sudo apt-get install libghc-bytestring-lexing-dev

(a ghc expert might have guessed the prefix)

Hmm, this is strange. You should be able to install bytestring-lexing
using cabal.

Could you check the output of

'cabal install bytestring-lexing --reinstall --force-reinstalls'

Now it works.

So I recommend adding to the step 1 dependencies for ubuntu:

zlib1g-dev
libghc-bytestring-lexing-dev

Also, there is some discrepancy between the README in the sources (at
least in /devel) and the installation instructions on the webpage. I
recommend that we synchronise these as much as possible.

I agree. Noted in the corresponding issue.

Now it compiles and can be started. However,

cas@doekoe:~/src/tamarin-prover$ tamarin-prover --prove -Ocase-studies
+RTS -N -RTS examples/csf12/*.spthy
maude tool: 'maude'
 checking version: 2.6. OK.

analyzing: examples/csf12/Artificial.spthy

tamarin-prover: case-studies/Artificial_analyzed.spthy: openFile: does
not exist (No such file or directory)
cas@doekoe:~/src/tamarin-prover$

Any suggestions?

fixed in 9b085d4

best regards,
Simon

The builtins are currently (somewhat) described in the README, but this is not distributed currently. The description should be included in the userguide instead.

Jup, let's be nice software developers :-)

They only clutter the visualization.

@beschmi, @cascremers I like that github displays the image of the author of a commit, issue, etc. However, you two look quite the same. Just registering some image in your preferences would be great :-)

This will enable better scaling and opens the way to lots of great stuff like

• making the goals clickable in the graph
• providing additional roll-over information
• use JavaScript to allow inline resizing of the graph
• ...

As a follow-up to #31, this simplifies understanding the status of a proof in the GUI.

@cascremers I suggest replacing https://github.com/meiersi/tamarin-prover/blob/develop/data/img/favicon.ico with the black rounded rectangle containing just the beard. It doesn't have to be great, as it will anyways be better than the SY logo, which has no relation to Tamarin anymore.

It is just too painful to not know which repository version was used to build a release of tamarin-prover and its utility libraries. There's some code lying around. We should make good use of it.

The current protocol specification format has some shortcomings that hamper further experimentation with proving and reusing inductive invariants and with exploiting filtering constructions in a more general way. This also reflects in the internal data structures representing security protocol theories. The following is an example outline of the extended/new protocol specification format. Afterwards, we'll explain the implications on the UI and some implications with respect to the implementation.

theory Name begin

// The sections must come in the following order: signature, protocol, properties

// The term signature is defined first. It consists of two named lists: functions and equations.
signature:
   functions:
   equations:

// rules and axioms can only be specified in the protocol section
protocol:
    rule blah:
    rule blih:

    // Axioms are trace formulas that filter the set of traces. They are not proven and reused by default.
    axiom blah:

// here come the properties
properties:
    // you can freely name your properties: claim, lemma, theorem -- this name has no semantic meaning
    claim secrecy[attributes]: 
      valid " formula "

   /* valid "formula"          means that we claim that the formula to hold for all traces.
       satisfiable "formula" means that we claim that the formula holds for at least one trace
   */

   /* possible attributes: 
         inductive (means induction should be used as first proof step)
         reuse (means that this validity claim should be reused by default)
         use: list-of-names (means that these names should be used additionally as lemmas in the proof)
         dont-use: list-of-names (means that these lemmas/claims/axioms/theorems should not be used in the proof)
   */

// Note that the layout-sensitive syntax is currently optional. 
// We might consider making it mandatory to avoid future parsing problems.

end

Internally axioms/claims/lemmas/theorems are represented uniformly. They all share a common flat name space. Duplicate names are disallowed. Their attributes classify them into their respective sets. We cache precomputed case distinctions indexed on the set of theorem names involved.

In the HTML view, every lemma has a link to the case distinctions (perhaps the full proof-context?) that are used for proving it.

Running some case studies, where it is important to understand any attacks that are found, has again proven to be unnecessarily hard by the amount of detail in the current graphs (that are meant to support inspecting the proof state and therefore contain information that is not needed to understand attacks).

Clearly, there are many great ways of improving such outputs but they may involve a lot of work.

So here is a recommendation for a simple fix:
Add an option to the gui to collapse all non-protocol rule instances into single dots (just change the style and drop the box spec in the graphviz output). This means none of the dependencies need to be changed - edges can stay as-is, the only thing that changes is some node definitions.
Inevitably, the graph will be much simpler to inspect.

Key wrapping like it is used in the PKCS#11 system requires stronger invariants to reason about the effect of handles. These invariants must be able to reference the deduced messages. Here, we follow the direct approach of logging the conclusion of every construction rule as a Ded(m) fact. Formulas referencing such facts denote invariants of normal dependency graphs.

In our constraint systems, we have to take special care when solving action constraints with such facts because we have no symbolic representation of the n-ary multiplication rule. We choose the approach to consider only Ded(m) @ i actions as open, if we can prove that m is neither a pair, an inversion, or a multiplication. This breaks our assumption that we can extract a P-solution from every solved form. We'll take care of that later.

At several points we are now using different ways to refer to Tamarin.

I've seen at least:

• Tamarin
• tamarin
• tamarin-prover
• the Tamarin prover

We should be as consistent as possible. I recommend:

• Short: Tamarin
  (latex: {\sc Tamarin}) ("we used Tamarin")
• Long: the Tamarin prover
  (latex: the {\sc Tamarin} prover)
• Referring to the executable: tamarin-prover
  (latex: {\tt tamarin-prover})

In HTML, the small-caps can be accomplished by
<span style="font-variant:small-caps">Tamarin</span>

I've also defined a CSS style for the web server, so there you can use
<span class="sc">Tamarin</span>
Besides setting small caps, the "sc" style also modifies the font to 'roman' or at least to 'serif' for consistency with the other visuals.

In the user interface, we often just want to expand all non-case-split goals. We therefore would like to introduce a further menu item that calls a corresponding safe proof method.

The current graphs (even the condensed ones) are often unreadable because they are too big. They also contain quite a lot of information that is interesting for the internals or for interactive proving, but that is irrelevant for understanding attacks.

One way to solve this is to add another view/output mode, that just shows (one) trace of the system, possibly with listed open goals, possibly just the protocol rule transitions. This would enable understanding attacks and would also make the output more suitable for printing.

We would like to allow for user defined sorts and a user-defined sort hierarchy. We do not plan to support overloaded functions; i.e., all functions must work on top-level sorts. The planned syntax is the following.

sorts: s1, s2, ..., sn
subsorts: s1 < s2 < ... sk, sk < ... sn

Once we have this change, we'll introduce a sort fact and require the user to define all fact symbols explicitly. We can then get rid of the Fact.hs module.

Currently, we use Debug.Trace.trace to log output. All of this goes to stdout. However, some of the output should be visible in the GUI, some should be mixed with the batch output and other you want to drop. Designing and implementing a simple, but more powerful solution seems to make sense. Especially, as Windows users are not accustomed to having a shell display any output that they might need to look at :-)

The user guide has a few mistakes (Init_1 instad of Client_1) and I'm not sure if it has a proper explanation of the induction stuff. Check this before the release.

Moreover, we could also add the TLS.spthy handshake and NSL to get people going a bit easier.

The installation instructions in the README should be synchronized with the ones on the website.

Cas suggested to use a status-popup when a branch is solved and the prover jumps to the next open goal in the interface.

Often one starts digging into a proof, and then one realizes a keyboard shortcut would be handy. By then it is pretty hard to find what they are without backing up out of the proof. Not convenient.

What about a pop-up window? Also, semi-transparent help overlays are all the rage nowadays (unity, gmail,...)

While modeling a protocol, it frequently occurs that one removes a clause and subsequently all occurrences of a variable.
When this happens, we get something like

All x. P

where x does not occur in P. Currently this yields an error stating that the formula does not meet 'guardedness'. This can be mistifying/misleading.
There's two options:

• Report error: quantified variable x does not occur in quantification formula
• Ignore this case and do not give an error (implicit removal of x). Possibly a warning would just be fine.

Intuitively, the second option makes most sense. Clearly the guardedness is then not met by the given spec.

After improving the communication with maude, the most expensive functions are unification and substitution application. Switching to a DAG style representation should yield further benefits here.

I wanted to write 'Init' somewhere in a formula to filter out Session ID's for the initiator, without introducing a role-specific fact.
In the session ID I have a constant for the role. However, this yielded an error.

A simple way to reproduce the core of the issue is to modify NAXOS to include a nested constant 'x', e.g., as in:

lemma eCK_key_secrecy:
  "not (Ex #i1 #i2 #i3 s A B minfo k .
            Sid(s, A, B, minfo) @ i1 & K( k ) @ i2 & Accept(s, ) @ i3

This yields:

/*
Error: the following well-formedness checks failed!

formula terms:
  lemma `eCK_key_secrecy' uses terms of the wrong form:
    `pair(Bound 3,'x')'
  
  The only allowed terms are public names and bound node and message
  variables. If you encounter free message variables, then you might
  have forgotten a #-prefix. Sort prefixes can only be dropped where
  this is unambiguous
*/

I think there's nothing problematic about the formula and it should therefore work just fine.

Any thoughts/fixes?

The following spec gives an incomprehensible Maude error. The problem is that I forgot 'builtin: diffie-hellman' so '^' is not defined. However the user won't easily be able to tell what is going on.

theory maude_error_but_should_work
begin
   
section{* Test *}
   
rule the_test:
   [ In(x^z) ] --> []

end

On a side note, running this simple spec with the added "builtin: diffie-hellman" takes an unreasonable 13 seconds on my machine. That's plain weird.

There is 'etc/filetype.vim' in /devel but the userguide refers to 'filepath.vim'.

The intruder variants generation using tamarin-prover variants -O. generates a different file than the one we currently have in data/dh_intruder_variants.spthy. Do you know the reason for that @beschmi ?

This should speed up tamarin a bit more.

Most of the the times, when clicking on a proof method in the HTML GUI, the focus does not change in the same way, as when executing the proof method using the keyboard shortcuts. The detail view shows the standard startup page instead of the next open branch in the proof.

This should be fixed. The desired behavior is the one implemented for the keyboard shortcuts.

This is issue is currently more a reminder than a concrete plan.

I noticed the shelltestrunner tool, which could provide a nice way to test our command-line interface.

Currently, if we don't get a proof and we don't get an attack there's not much we can say. It would be nice to have a bounded result similar to Scyther's bounded verification.

Simon has worked on some ideas for making node identifiers unique that might address this issue.

We are programmatically producing different ISend rule instances. This is a possible soundness bug. Fix and ensure that for every built-in rule there is exactly one function to create it.

Title says it all.

We use even version numbers for stable releases and odd numbers for development versions. Add comments to this issue for further stuff I should not forget to do before releasing to hackage. Currently, I know of the following:

• [DONE] Make sure that all issues in the csf-12-release milestone are resolved
• [DONE] Rerun all case-studies to ensure no regression has crept in
• [DONE] Update reference in paper to point to http://hackage.haskell.org/package/tamarin-prover-0.4.0.0
• [DONE] Check that tarballs compile with the three GHC 7.Xs

The equation splits often yield many cases and it would be interesting to be able to quickly see which branch belongs to which equation. I imagine annotation (just as is done now with some other text):

case split_case_02 // x = y^z

The lexer is currently based on alex and has trouble parsing Unicode tokens. Moreover, some operators allow internal spacing, which is rather strange. Switching to a parsec based solution will allow us to simplify the code and tighten the grammar.

A failing wellformedness check indicates that the model is likely to be flawed. This is easily forgotten when looking at a summary which just states NewKey_secrecy (all-traces): verified (5 steps).

Here's a nice core dump:

The reason does not seem to be the 'let'. Instead, the dump is caused by me using H1/H2 as below. This causes Maude to bork (in some examples silently, in this one with an error) but Tamarin core dumps.

theory NAXOS_eCK
begin

builtin: diffie-hellman

functions: H1/1
functions: H2/1

section{* NAXOS *}

rule generate_ltk:
   let pkA = 'g'^~lkA
   in
   [ Fr(~lkA) ] -->
   [ !Ltk( $A, ~lkA ), !Pk( $A, pkA ), Out( pkA ) ]


rule Resp_1:
  let pkI    = ('g'^~lkI)
      exR    = H1(< ~ekR, ~lkR >)
      hkr    = 'g'^'4'
      seskey = H2(< pkI^exR, X^~lkR, X^'6', $I, $R >)
  in
   [ In( X ), Fr( ~ekR ), !Ltk($R, ~lkR), !Pk($I, pkI) ]
   --[ SidR_1( ~ekR, $I, $R, X, hkr, seskey) ]->
   [ Out( hkr ),
     !Ephk(~ekR),
     !Sessk( ~ekR, seskey) ]

end