(1)  Proving unicity of nonces sessions (see technical report)
We perform a backward search starting from the unsafe states:

unsafe([ 
  unsafe([
           step1(pk(A),tuple(nonce(NA),pk(B))),
	   step1(pk(C),tuple(nonce(NA),pk(D))) 
         ], 
	  {})
]).


We obtain:

| ?- go.

Step1
.
Step2

--------------------------------------------------------
The fixpoint has been reached!
Search for the initial configuration using :-ls.
yes

| ?- init(K,L).
no

---------------

(2) Proving non-injective agreement (see technical report)
We perform a backward search starting from the unsafe states:


unsafe([ 
  unsafe([step4(pk(2),tuple(nonce(1),nonce(2),pk(1)))], 
	  {})	
]).


| ?- ptime(go).

Step1
.
Step2
..
Step3
.......
Step4
....
Step5
....................
Step6
.........................................
Step7
..................
Step8
...
Step9

--------------------------------------------------------
The fixpoint has been reached!
Search for the initial configuration using :-ls.
Execution time 17.5
yes

To find the potential initial configurations:

| ?- init(K,L).

K = 4,
L = 15 ? ;
no

By using :-ls we find that node 5 contains the initiator state: step1(pk(1),tuple(nonce(1),pk(2))
(This test can be easily automated, though I still have to do it).

Now, by using 

|- ? selpaths(15,5). 
yes

we find there are no paths that from node 15 lead to responder's state 
that DO NOT go though node 5.
Thus, non-injective agreement holds.

Together with unicity we obtain a proof of agreement.