| ?-  ptime(g).


Begin trace
initialization.

step([init], {}).

init.

step([time(A),fresh(B),init(1),resp(2)], {B>=0.0,A>=0.0}).

alice_starts.

step([fresh(A),resp(2),time(B),init(1,tuple(2,C,B)),enc(sv(1),tuple(2,C,B))], {C-A<-0.0,C>-0.0,B>=0.0}).

server_forwards.

step([time(A),enc(sk(2),tuple(1,B,A)),init(1,tuple(2,B,A)),fresh(C),resp(2)], {B-C<-0.0,B>-0.0,A>=0.0}).

tock.

step([time(A),enc(sk(2),tuple(1,B,C)),init(1,tuple(2,B,C)),fresh(D),resp(2)], {C-A<-0.0,B-D<-0.0,B>-0.0,C>=-0.0}).

impersonate.

step([enc(sv(2),tuple(1,A,B)),time(C),init(1,tuple(2,A,B)),fresh(D),resp(2)], {B-C<-0.0,A-D<-0.0,A>-0.0,B>=-0.0}).

server_forwards.

step([time(A),enc(sk(1),tuple(2,B,A)),init(1,tuple(2,B,C)),fresh(D),resp(2)], {C-A<-0.0,B-D<-0.0,B>-0.0,C>=-0.0,C-A>= -1.0}).

tock.

step([time(A),enc(sk(1),tuple(2,B,C)),init(1,tuple(2,B,D)),fresh(E),resp(2)], {C-A<-0.0,B-E<-0.0,C-D=<1.0,B>-0.0,C-D>-0.0,D>=0.0}).

impersonate.

step([enc(sv(1),tuple(2,A,B)),time(C),init(1,tuple(2,A,D)),fresh(E),resp(2)], {D-B<-0.0,B-C<-0.0,A-E<-0.0,A>-0.0,D>=-0.0,D-B>= -1.0}).

server_forwards.

step([time(A),enc(sk(2),tuple(1,B,A)),init(1,tuple(2,B,C)),fresh(D),resp(2)], {C-A<-0.0,B-D<-0.0,B>-0.0,C>=-0.0,C-A>= -2.0}).

tock.

step([time(A),enc(sk(2),tuple(1,B,C)),init(1,tuple(2,B,D)),fresh(E),resp(2)], {C-A<-0.0,B-E<-0.0,C-D=<2.0,B>-0.0,C-D>-0.0,D>=0.0}).

bob_receives.

step([time(A),resp(2,tuple(1,B,A)),init(1,tuple(2,B,C)),fresh(D)], {C-A<-0.0,B-D<-0.0,B>-0.0,C>=-0.0,C-A>= -3.0}).

goal.

step([time(A),resp(2,tuple(1,B,A)),init(1,tuple(2,B,C)),fresh(D)], {C-A<-0.0,B-D<-0.0,B>-0.0,C>=-0.0,C-A>= -3.0}).
End trace


Execution time 0.3