\||||||||||||||||||/
		   --- Welcome to Maude ---
		     /||||||||||||||||||\
	     Maude alpha128 built: Mar 10 2020 14:45:05
	     Copyright 1997-2020 SRI International
		   Mon Jul  6 00:20:09 2020

	    Maude-NPA Version: 3.1.4 (June 2nd 2020)
	    with direct composition, irreducibility constraints and time
	    (To be run with Maude alpha 121 or above)
	    Copyright (c) 2020, University of Illinois
	    All rights reserved.

 Commands:
 red unification? .           returns the unification algorithm to be used
 red new-strands? .           returns the actual protocol strands
 red displayGrammars .        for generating grammars
 red run(X,Y).                for Y backwards analysis steps for attack pattern
    X
 red debug(X,Y).              more information than run command
 red digest(X,Y).             less information than run command
 red summary(X,Y).            for summary of analysis steps
 red ids(X,Y).                for set of state ids
 red initials(X,Y).           for showing only initial steps
==========================================
reduce in MAUDE-NPA : summary(0, 0) .
rewrites: 150766344 in 169776ms cpu (169776ms real) (888030 rewrites/second)
result Summary: States>> 1 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(0, 1) .
rewrites: 3325539 in 3208ms cpu (3207ms real) (1036639 rewrites/second)
result Summary: States>> 1 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(0, 2) .
rewrites: 755175 in 488ms cpu (486ms real) (1547489 rewrites/second)
result Summary: States>> 1 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(0, 3) .
rewrites: 416401 in 304ms cpu (303ms real) (1369740 rewrites/second)
result Summary: States>> 1 Solutions>> 1
==========================================
reduce in MAUDE-NPA : initials(0,3) .
rewrites: 180 in 0ms cpu (0ms real) (~ rewrites/second)
result ShortIdSystem: < 1 . 1 . 2 . 1 > (
:: #1:Fresh,#0:Fresh ::
[ nil | 
   +(hs ;
     n(client, #0:Fresh) ;
     g1 ;
     gen(g1) ;
     exp(g1, gen(g1), n(client, #1:Fresh))), 
   -(hs ;
     n(server, #2:Fresh) ;
     g1 ;
     gen(g1) ;
     exp(g1, gen(g1), n(server, #3:Fresh)) ;
     e(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
       authreq ;
       sig(server,
           hs ;
           n(client, #0:Fresh) ;
           n(server, #2:Fresh) ;
           g1 ;
           gen(g1) ;
           exp(g1, gen(g1), n(client, #1:Fresh)) ;
           exp(g1, gen(g1), n(server, #3:Fresh)) ;
           authreq)  ;
       mac(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
           hs ;
           n(client, #0:Fresh) ;
           n(server, #2:Fresh) ;
           g1 ;
           gen(g1) ;
           exp(g1, gen(g1), n(client, #1:Fresh)) ;
           exp(g1, gen(g1), n(server, #3:Fresh)) ;
           authreq) ) ), 
   authreq eq authreq, 
   +(e(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
       sig(client,
           hs ;
           n(client, #0:Fresh) ;
           n(server, #2:Fresh) ;
           g1 ;
           gen(g1) ;
           exp(g1, gen(g1), n(client, #1:Fresh)) ;
           exp(g1, gen(g1), n(server, #3:Fresh)) ;
           authreq ;
           sig(server,
               hs ;
               n(client, #0:Fresh) ;
               n(server, #2:Fresh) ;
               g1 ;
               gen(g1) ;
               exp(g1, gen(g1), n(client, #1:Fresh)) ;
               exp(g1, gen(g1), n(server, #3:Fresh)) ;
               authreq)  ;
           mac(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
               hs ;
               n(client, #0:Fresh) ;
               n(server, #2:Fresh) ;
               g1 ;
               gen(g1) ;
               exp(g1, gen(g1), n(client, #1:Fresh)) ;
               exp(g1, gen(g1), n(server, #3:Fresh)) ;
               authreq) )  ;
       mac(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
           hs ;
           n(client, #0:Fresh) ;
           n(server, #2:Fresh) ;
           g1 ;
           gen(g1) ;
           exp(g1, gen(g1), n(client, #1:Fresh)) ;
           exp(g1, gen(g1), n(server, #3:Fresh)) ;
           authreq ;
           sig(server,
               hs ;
               n(client, #0:Fresh) ;
               n(server, #2:Fresh) ;
               g1 ;
               gen(g1) ;
               exp(g1, gen(g1), n(client, #1:Fresh)) ;
               exp(g1, gen(g1), n(server, #3:Fresh)) ;
               authreq)  ;
           mac(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
               hs ;
               n(client, #0:Fresh) ;
               n(server, #2:Fresh) ;
               g1 ;
               gen(g1) ;
               exp(g1, gen(g1), n(client, #1:Fresh)) ;
               exp(g1, gen(g1), n(server, #3:Fresh)) ;
               authreq) ) ) ), nil]  & 
:: #2:Fresh,#3:Fresh ::
[ nil | 
   -(hs ;
     n(client, #0:Fresh) ;
     g1 ;
     gen(g1) ;
     exp(g1, gen(g1), n(client, #1:Fresh))), 
   +(hs ;
     n(server, #2:Fresh) ;
     g1 ;
     gen(g1) ;
     exp(g1, gen(g1), n(server, #3:Fresh)) ;
     e(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
       authreq ;
       sig(server,
           hs ;
           n(client, #0:Fresh) ;
           n(server, #2:Fresh) ;
           g1 ;
           gen(g1) ;
           exp(g1, gen(g1), n(client, #1:Fresh)) ;
           exp(g1, gen(g1), n(server, #3:Fresh)) ;
           authreq)  ;
       mac(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
           hs ;
           n(client, #0:Fresh) ;
           n(server, #2:Fresh) ;
           g1 ;
           gen(g1) ;
           exp(g1, gen(g1), n(client, #1:Fresh)) ;
           exp(g1, gen(g1), n(server, #3:Fresh)) ;
           authreq) ) ), 
   authreq eq authreq, 
   -(e(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
       sig(client,
           hs ;
           n(client, #0:Fresh) ;
           n(server, #2:Fresh) ;
           g1 ;
           gen(g1) ;
           exp(g1, gen(g1), n(client, #1:Fresh)) ;
           exp(g1, gen(g1), n(server, #3:Fresh)) ;
           authreq ;
           sig(server,
               hs ;
               n(client, #0:Fresh) ;
               n(server, #2:Fresh) ;
               g1 ;
               gen(g1) ;
               exp(g1, gen(g1), n(client, #1:Fresh)) ;
               exp(g1, gen(g1), n(server, #3:Fresh)) ;
               authreq)  ;
           mac(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
               hs ;
               n(client, #0:Fresh) ;
               n(server, #2:Fresh) ;
               g1 ;
               gen(g1) ;
               exp(g1, gen(g1), n(client, #1:Fresh)) ;
               exp(g1, gen(g1), n(server, #3:Fresh)) ;
               authreq) )  ;
       mac(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
           hs ;
           n(client, #0:Fresh) ;
           n(server, #2:Fresh) ;
           g1 ;
           gen(g1) ;
           exp(g1, gen(g1), n(client, #1:Fresh)) ;
           exp(g1, gen(g1), n(server, #3:Fresh)) ;
           authreq ;
           sig(server,
               hs ;
               n(client, #0:Fresh) ;
               n(server, #2:Fresh) ;
               g1 ;
               gen(g1) ;
               exp(g1, gen(g1), n(client, #1:Fresh)) ;
               exp(g1, gen(g1), n(server, #3:Fresh)) ;
               authreq)  ;
           mac(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
               hs ;
               n(client, #0:Fresh) ;
               n(server, #2:Fresh) ;
               g1 ;
               gen(g1) ;
               exp(g1, gen(g1), n(client, #1:Fresh)) ;
               exp(g1, gen(g1), n(server, #3:Fresh)) ;
               authreq) ) ) ), nil] )
| 
e(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
  sig(client,
      hs ;
      n(client, #0:Fresh) ;
      n(server, #2:Fresh) ;
      g1 ;
      gen(g1) ;
      exp(g1, gen(g1), n(client, #1:Fresh)) ;
      exp(g1, gen(g1), n(server, #3:Fresh)) ;
      authreq ;
      sig(server,
          hs ;
          n(client, #0:Fresh) ;
          n(server, #2:Fresh) ;
          g1 ;
          gen(g1) ;
          exp(g1, gen(g1), n(client, #1:Fresh)) ;
          exp(g1, gen(g1), n(server, #3:Fresh)) ;
          authreq)  ;
      mac(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
          hs ;
          n(client, #0:Fresh) ;
          n(server, #2:Fresh) ;
          g1 ;
          gen(g1) ;
          exp(g1, gen(g1), n(client, #1:Fresh)) ;
          exp(g1, gen(g1), n(server, #3:Fresh)) ;
          authreq) )  ;
  mac(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
      hs ;
      n(client, #0:Fresh) ;
      n(server, #2:Fresh) ;
      g1 ;
      gen(g1) ;
      exp(g1, gen(g1), n(client, #1:Fresh)) ;
      exp(g1, gen(g1), n(server, #3:Fresh)) ;
      authreq ;
      sig(server,
          hs ;
          n(client, #0:Fresh) ;
          n(server, #2:Fresh) ;
          g1 ;
          gen(g1) ;
          exp(g1, gen(g1), n(client, #1:Fresh)) ;
          exp(g1, gen(g1), n(server, #3:Fresh)) ;
          authreq)  ;
      mac(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
          hs ;
          n(client, #0:Fresh) ;
          n(server, #2:Fresh) ;
          g1 ;
          gen(g1) ;
          exp(g1, gen(g1), n(client, #1:Fresh)) ;
          exp(g1, gen(g1), n(server, #3:Fresh)) ;
          authreq) ) )  !inI,
(hs ;
n(server, #2:Fresh) ;
g1 ;
gen(g1) ;
exp(g1, gen(g1), n(server, #3:Fresh)) ;
e(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
  authreq ;
  sig(server,
      hs ;
      n(client, #0:Fresh) ;
      n(server, #2:Fresh) ;
      g1 ;
      gen(g1) ;
      exp(g1, gen(g1), n(client, #1:Fresh)) ;
      exp(g1, gen(g1), n(server, #3:Fresh)) ;
      authreq)  ;
  mac(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
      hs ;
      n(client, #0:Fresh) ;
      n(server, #2:Fresh) ;
      g1 ;
      gen(g1) ;
      exp(g1, gen(g1), n(client, #1:Fresh)) ;
      exp(g1, gen(g1), n(server, #3:Fresh)) ;
      authreq) ) ) !inI,
(hs ;
n(client, #0:Fresh) ;
g1 ;
gen(g1) ;
exp(g1, gen(g1), n(client, #1:Fresh))) !inI
| 
+(hs ;
  n(client, #0:Fresh) ;
  g1 ;
  gen(g1) ;
  exp(g1, gen(g1), n(client, #1:Fresh))), 
-(hs ;
  n(client, #0:Fresh) ;
  g1 ;
  gen(g1) ;
  exp(g1, gen(g1), n(client, #1:Fresh))), 
+(hs ;
  n(server, #2:Fresh) ;
  g1 ;
  gen(g1) ;
  exp(g1, gen(g1), n(server, #3:Fresh)) ;
  e(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
    authreq ;
    sig(server,
        hs ;
        n(client, #0:Fresh) ;
        n(server, #2:Fresh) ;
        g1 ;
        gen(g1) ;
        exp(g1, gen(g1), n(client, #1:Fresh)) ;
        exp(g1, gen(g1), n(server, #3:Fresh)) ;
        authreq)  ;
    mac(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
        hs ;
        n(client, #0:Fresh) ;
        n(server, #2:Fresh) ;
        g1 ;
        gen(g1) ;
        exp(g1, gen(g1), n(client, #1:Fresh)) ;
        exp(g1, gen(g1), n(server, #3:Fresh)) ;
        authreq) ) ), 
-(hs ;
  n(server, #2:Fresh) ;
  g1 ;
  gen(g1) ;
  exp(g1, gen(g1), n(server, #3:Fresh)) ;
  e(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
    authreq ;
    sig(server,
        hs ;
        n(client, #0:Fresh) ;
        n(server, #2:Fresh) ;
        g1 ;
        gen(g1) ;
        exp(g1, gen(g1), n(client, #1:Fresh)) ;
        exp(g1, gen(g1), n(server, #3:Fresh)) ;
        authreq)  ;
    mac(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
        hs ;
        n(client, #0:Fresh) ;
        n(server, #2:Fresh) ;
        g1 ;
        gen(g1) ;
        exp(g1, gen(g1), n(client, #1:Fresh)) ;
        exp(g1, gen(g1), n(server, #3:Fresh)) ;
        authreq) ) ), 
+(e(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
    sig(client,
        hs ;
        n(client, #0:Fresh) ;
        n(server, #2:Fresh) ;
        g1 ;
        gen(g1) ;
        exp(g1, gen(g1), n(client, #1:Fresh)) ;
        exp(g1, gen(g1), n(server, #3:Fresh)) ;
        authreq ;
        sig(server,
            hs ;
            n(client, #0:Fresh) ;
            n(server, #2:Fresh) ;
            g1 ;
            gen(g1) ;
            exp(g1, gen(g1), n(client, #1:Fresh)) ;
            exp(g1, gen(g1), n(server, #3:Fresh)) ;
            authreq)  ;
        mac(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
            hs ;
            n(client, #0:Fresh) ;
            n(server, #2:Fresh) ;
            g1 ;
            gen(g1) ;
            exp(g1, gen(g1), n(client, #1:Fresh)) ;
            exp(g1, gen(g1), n(server, #3:Fresh)) ;
            authreq) )  ;
    mac(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
        hs ;
        n(client, #0:Fresh) ;
        n(server, #2:Fresh) ;
        g1 ;
        gen(g1) ;
        exp(g1, gen(g1), n(client, #1:Fresh)) ;
        exp(g1, gen(g1), n(server, #3:Fresh)) ;
        authreq ;
        sig(server,
            hs ;
            n(client, #0:Fresh) ;
            n(server, #2:Fresh) ;
            g1 ;
            gen(g1) ;
            exp(g1, gen(g1), n(client, #1:Fresh)) ;
            exp(g1, gen(g1), n(server, #3:Fresh)) ;
            authreq)  ;
        mac(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
            hs ;
            n(client, #0:Fresh) ;
            n(server, #2:Fresh) ;
            g1 ;
            gen(g1) ;
            exp(g1, gen(g1), n(client, #1:Fresh)) ;
            exp(g1, gen(g1), n(server, #3:Fresh)) ;
            authreq) ) ) ), 
-(e(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
    sig(client,
        hs ;
        n(client, #0:Fresh) ;
        n(server, #2:Fresh) ;
        g1 ;
        gen(g1) ;
        exp(g1, gen(g1), n(client, #1:Fresh)) ;
        exp(g1, gen(g1), n(server, #3:Fresh)) ;
        authreq ;
        sig(server,
            hs ;
            n(client, #0:Fresh) ;
            n(server, #2:Fresh) ;
            g1 ;
            gen(g1) ;
            exp(g1, gen(g1), n(client, #1:Fresh)) ;
            exp(g1, gen(g1), n(server, #3:Fresh)) ;
            authreq)  ;
        mac(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
            hs ;
            n(client, #0:Fresh) ;
            n(server, #2:Fresh) ;
            g1 ;
            gen(g1) ;
            exp(g1, gen(g1), n(client, #1:Fresh)) ;
            exp(g1, gen(g1), n(server, #3:Fresh)) ;
            authreq) )  ;
    mac(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
        hs ;
        n(client, #0:Fresh) ;
        n(server, #2:Fresh) ;
        g1 ;
        gen(g1) ;
        exp(g1, gen(g1), n(client, #1:Fresh)) ;
        exp(g1, gen(g1), n(server, #3:Fresh)) ;
        authreq ;
        sig(server,
            hs ;
            n(client, #0:Fresh) ;
            n(server, #2:Fresh) ;
            g1 ;
            gen(g1) ;
            exp(g1, gen(g1), n(client, #1:Fresh)) ;
            exp(g1, gen(g1), n(server, #3:Fresh)) ;
            authreq)  ;
        mac(exp(g1, gen(g1), n(server, #3:Fresh) * n(client, #1:Fresh)),
            hs ;
            n(client, #0:Fresh) ;
            n(server, #2:Fresh) ;
            g1 ;
            gen(g1) ;
            exp(g1, gen(g1), n(client, #1:Fresh)) ;
            exp(g1, gen(g1), n(server, #3:Fresh)) ;
            authreq) ) ) )
| 
nil
Bye.