Merge branch 'develop' into fix-grammar-terms

data/js/tamarin-prover-ui.js

@@ -316,6 +316,19 @@ var ui = {
             $("a.active-link").click();
         });
 
+        // Click handler for clustering toggle
+        var agent_toggle = $('a#agent-toggle');
+        agent_toggle.click(function(ev) {
+            ev.preventDefault();
+            if ($.cookie("clustering")) {
+                $.cookie("clustering", null, { path: '/' });
+            } else {
+                $.cookie("clustering", true, { path: '/' });
+            }
+            $("a.active-link").click();
+            mainDisplay.toggleOption(agent_toggle);
+        });
+
 
 
         // Install event handlers
@@ -411,6 +424,11 @@ var ui = {
             $("a#auto-toggle").addClass("disabled-option");
         }
 
+        if ($.cookie("clustering") === "true") {
+            $("a#agent-toggle").addClass("active-option");
+        } else {
+            $("a#agent-toggle").addClass("disabled-option");
+        }
     },
 
     /**
@@ -796,6 +814,13 @@ var mainDisplay = {
             );
         }
 
+        if ($.cookie("clustering") === "true") {
+            params = params.concat(
+                { name: "clustering", value: "true" }
+            );
+        }
+
+
         // Rewrite image paths (if necessary)
         if(params.length > 0) {
             var query_string = $.param(params);

examples/features/visualization/roles.spthy

@@ -0,0 +1,180 @@
+theory NSPK3_roles
+begin
+
+builtins: asymmetric-encryption
+
+/*
+   Protocol:    The classic three message version of the
+                flawed Needham-Schroeder Public Key Protocol
+   Modeler:     Simon Meier
+   Date:        September 2012
+
+   Source:      Gavin Lowe. Breaking and fixing the Needham-Schroeder
+                public-key protocol using FDR. In Tiziana Margaria and
+                Bernhard Steffen, editors, TACAS, volume 1055 of Lecture Notes
+                in Computer Science, pages 147–166.  Springer, 1996.
+
+   Status:      working
+
+   Note that we are using explicit global constants for discerning the
+   different encryption instead of the implicit sources.
+
+   From examples/classic/NSPK3.spthy, but with added roles, to illustrate
+   graph clustering using roles.
+ */
+
+
+// Public key infrastructure
+rule Register_pk:
+  [ Fr(~ltkA) ]
+  -->
+  [ !Ltk($A, ~ltkA), !Pk($A, pk(~ltkA)), Out(pk(~ltkA)) ]
+
+rule Reveal_ltk:
+  [ !Ltk(A, ltkA) ] --[ RevLtk(A)    ]-> [ Out(ltkA) ]
+
+
+/* We formalize the following protocol
+
+  protocol NSPK3 {
+    1. I -> R: {'1',ni,I}pk(R)
+    2. I <- R: {'2',ni,nr}pk(I)
+    3. I -> R: {'3',nr}pk(R)
+  }
+*/
+
+rule I_1 [role="Initiator",color=#ffff00]:
+  let m1 = aenc{'1', ~ni, $I}pkR
+  in
+    [ Fr(~ni)
+    , !Pk($R, pkR)
+    ]
+  --[ OUT_I_1(m1)
+    ]->
+    [ Out( m1 )
+    , St_I_1($I, $R, ~ni)
+    ]
+
+rule R_1 [role="Responder"]:
+  let m1 = aenc{'1', ni, I}pk(ltkR)
+      m2 = aenc{'2', ni, ~nr}pkI
+  in
+    [ !Ltk($R, ltkR)
+    , In( m1 )
+    , !Pk(I, pkI)
+    , Fr(~nr)
+    ]
+  --[ IN_R_1_ni( ni, m1 )
+    , OUT_R_1( m2 )
+    , Running(I, $R, <'init',ni,~nr>)
+    ]->
+    [ Out( m2 )
+    , St_R_1($R, I, ni, ~nr)
+    ]
+
+rule I_2 [role="Initiator"]:
+  let m2 = aenc{'2', ni, nr}pk(ltkI)
+      m3 = aenc{'3', nr}pkR
+  in
+    [ St_I_1(I, R, ni)
+    , !Ltk(I, ltkI)
+    , In( m2 )
+    , !Pk(R, pkR)
+    ]
+  --[ IN_I_2_nr( nr, m2)
+    , Commit (I, R, <'init',ni,nr>)  // need to log identities explicitely to
+    , Running(R, I, <'resp',ni,nr>)  // specify that they must not be
+                                     // compromised in the property.
+    ]->
+    [ Out( m3 )
+    , Secret(I,R,nr)
+    , Secret(I,R,ni)
+    ]
+
+rule R_2 [role="Responder"]:
+    [ St_R_1(R, I, ni, nr)
+    , !Ltk(R, ltkR)
+    , In( aenc{'3', nr}pk(ltkR) )
+    ]
+  --[ Commit (R, I, <'resp',ni,nr>)
+    ]->
+    [ Secret(R,I,nr)
+    , Secret(R,I,ni)
+    ]
+
+/* TODO: Also model session-key reveals and adapt security properties. */
+rule Secrecy_claim:
+  [ Secret(A, B, m) ] --[ Secret(A, B, m) ]-> []
+
+
+
+/* Note that we are using an untyped protocol model. For proofs, we therefore
+require a protocol specific type invariant for proof construction. In
+principle, such an invariant is not required for attack search, but does help
+a lot.
+
+See 'NSLPK3.spthy' for a detailed explanation of the construction of this
+invariant.
+*/
+lemma types [sources]:
+  " (All ni m1 #i.
+       IN_R_1_ni( ni, m1) @ i
+       ==>
+       ( (Ex #j. KU(ni) @ j & j < i)
+       | (Ex #j. OUT_I_1( m1 ) @ j)
+       )
+    )
+  & (All nr m2 #i.
+       IN_I_2_nr( nr, m2) @ i
+       ==>
+       ( (Ex #j. KU(nr) @ j & j < i)
+       | (Ex #j. OUT_R_1( m2 ) @ j)
+       )
+    )
+  "
+
+// Nonce secrecy from the perspective of both the initiator and the responder.
+lemma nonce_secrecy:
+  " /* It cannot be that */
+    not(
+        Ex A B s #i.
+          /* somebody claims to have setup a shared secret, */
+          Secret(A, B, s) @ i
+          /* but the adversary knows it */
+        & (Ex #j. K(s) @ j)
+          /* without having performed a long-term key reveal. */
+        & not (Ex #r. RevLtk(A) @ r)
+        & not (Ex #r. RevLtk(B) @ r)
+       )"
+
+// Injective agreement from the perspective of both the initiator and the responder.
+lemma injective_agree:
+  " /* Whenever somebody commits to running a session, then*/
+    All actor peer params #i.
+        Commit(actor, peer, params) @ i
+      ==>
+        /* there is somebody running a session with the same parameters */
+          (Ex #j. Running(actor, peer, params) @ j & j < i
+            /* and there is no other commit on the same parameters */
+            & not(Ex actor2 peer2 #i2.
+                    Commit(actor2, peer2, params) @ i2 & not(#i = #i2)
+                 )
+          )
+        /* or the adversary perform a long-term key reveal on actor or peer */
+        | (Ex #r. RevLtk(actor) @ r)
+        | (Ex #r. RevLtk(peer)  @ r)
+  "
+
+// Consistency check: ensure that secrets can be shared between honest agents.
+lemma session_key_setup_possible:
+  exists-trace
+  " /* It is possible that */
+    Ex A B s #i.
+      /* somebody claims to have setup a shared secret, */
+      Secret(A, B, s) @ i
+      /* without the adversary having performed a long-term key reveal. */
+    & not (Ex #r. RevLtk(A) @ r)
+    & not (Ex #r. RevLtk(B) @ r)
+  "
+
+end