Santiagos-MacBook-Pro:prototype-20121204 sescobar$ examples/secret07-command 
Wed Dec  5 02:37:19 CET 2012
		     \||||||||||||||||||/
		   --- Welcome to Maude ---
		     /||||||||||||||||||\
	    Maude alpha96b built: Nov  9 2012 18:20:01
	    Copyright 1997-2011 SRI International
		   Wed Dec  5 02:37:19 2012
Maude> 
	    Maude-NPA Version:  Dec 4 2012 with direct composition
	    Copyright (c) 2012, University of Illinois
	    All rights reserved.

 Commands:
 red unification? .           for getting the unification algorithm
 red genGrammars .            for generating grammars
 red run(X,Y).                for Y backwards analysis steps for attack pattern X
 red summary(X,Y).            for summary of analysis steps
 red initials(X,Y).           for showing only initial steps
==========================================
reduce in MAUDE-NPA : genGrammars .
rewrites: 508642 in 970ms cpu (987ms real) (524236 rewrites/second)
result GrammarList: (
grl #0:NeNonceSet notInI, (#0:NeNonceSet notLeq n(i, #1:Fresh)), #0:NeNonceSet notLeq #2:NeNonceSet * #3:NeNonceSet => (#4:NeNonceSet * #0:NeNonceSet) inL . ; 
grl (#1:NeNonceSet * #0:NeNonceSet) notInI, (#0:NeNonceSet notLeq n(i, #2:Fresh)), (#1:NeNonceSet * #0:NeNonceSet) notLeq #3:NeNonceSet * #4:NeNonceSet => #0:NeNonceSet inL .)
| (errorNoHeuristicApplied {
grl empty => (#1:NeNonceSet * #2:NeNonceSet) inL .,none,
grl empty => (#1:NeNonceSet,#2:NeNonceSet) inL .,none,
grl empty => (#1:NeNonceSet,#2:NeNonceSet) inL .} usingGrammar 
grl empty => (#1:NeNonceSet * #2:NeNonceSet) inL .)
| 
grl #50:GenvExp notInI => exp(#50:GenvExp, #60:NeNonceSet) inL .
| 
grl #0:NeNonceSet notInI, (#0:NeNonceSet notLeq n(a, #1:Fresh)), (#0:NeNonceSet notLeq n(b, #2:Fresh)), #0:NeNonceSet notLeq #3:NeNonceSet * #4:NeNonceSet => exp(#5:GenvExp, #0:NeNonceSet) inL .
| (errorNoHeuristicApplied {
grl empty => exp(#1:GenvExp, #2:NeNonceSet) inL .,none,
grl empty => (#2:NeNonceSet,#1:GenvExp) inL .,none,
grl empty => (#2:NeNonceSet,#1:GenvExp) inL .} usingGrammar 
grl empty => exp(#1:GenvExp, #2:NeNonceSet) inL .)
| 
grl n(#0:Name, #1:Fresh) notLeq n(i, #2:Fresh) => n(#0:Name, #1:Fresh) inL .
==========================================
reduce in MAUDE-NPA : run(0) .
rewrites: 2624 in 28ms cpu (29ms real) (92472 rewrites/second)
result IdSystem: < 1 > 
:: r:Fresh ::
[ nil, 
   +(a), 
   +(b), 
   +(exp(g, n(a, r:Fresh))), 
   -(b), 
   -(a), 
   -(exp(g, NS:NeNonceSet)) | nil] 
|| 
exp(g, NS:NeNonceSet * n(a, r:Fresh)) inI
|| 
nil
|| 
nil
|| 
nil
==========================================
reduce in MAUDE-NPA : summary(0) .
rewrites: 34 in 0ms cpu (0ms real) (~ rewrites/second)
result Summary: States>> 1 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(1) .
rewrites: 515022 in 883ms cpu (892ms real) (582784 rewrites/second)
result Summary: States>> 5 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(2) .
rewrites: 1309533 in 1965ms cpu (1986ms real) (666404 rewrites/second)
result Summary: States>> 1 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(3) .
rewrites: 39043 in 36ms cpu (44ms real) (1055986 rewrites/second)
result Summary: States>> 1 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(4) .
rewrites: 40191 in 42ms cpu (46ms real) (948885 rewrites/second)
result Summary: States>> 1 Solutions>> 1
==========================================
reduce in MAUDE-NPA : run(0) .
rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second)
result IdSystem: < 1 > 
:: r:Fresh ::
[ nil, 
   +(a), 
   +(b), 
   +(exp(g, n(a, r:Fresh))), 
   -(b), 
   -(a), 
   -(exp(g, NS:NeNonceSet)) | nil] 
|| 
exp(g, NS:NeNonceSet * n(a, r:Fresh)) inI
|| 
nil
|| 
nil
|| 
nil
==========================================
reduce in MAUDE-NPA : run(1) .
rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second)
result IdSystemSet: (< 1 . 1 > (
:: nil ::
[ nil | 
   -(g), 
   -(#0:NeNonceSet), 
   +(exp(g, #0:NeNonceSet)), nil]  & 
:: #1:Fresh ::
[ nil, 
   +(a), 
   +(b), 
   +(exp(g, n(a, #1:Fresh))) | 
   -(b), 
   -(a), 
   -(exp(g, #0:NeNonceSet)), nil] )
|| 
exp(g, #0:NeNonceSet) !inI,
exp(g, #0:NeNonceSet * n(a, #1:Fresh)) inI
|| 
-(g), 
-(#0:NeNonceSet), 
+(exp(g, #0:NeNonceSet)), 
-(b), 
-(a), 
-(exp(g, #0:NeNonceSet))
|| 
ghost( #0:NeNonceSet,
   :: nil ::
   [ nil | 
      -(g), 
      -(#0:NeNonceSet), 
      +(exp(g, #0:NeNonceSet)), nil]  & 
   :: #1:Fresh ::
   [ nil, 
      +(a), 
      +(b), 
      +(exp(g, n(a, #1:Fresh))) | 
      -(b), 
      -(a), 
      -(exp(g, #0:NeNonceSet)), nil] ,    
   exp(g, #0:NeNonceSet) !inI,
   exp(g, #0:NeNonceSet * n(a, #1:Fresh)) inI,    
   -(g), 
   -(#0:NeNonceSet), 
   +(exp(g, #0:NeNonceSet)), 
   -(b), 
   -(a), 
   -(exp(g, #0:NeNonceSet)),    
   nil )
|| 
nil)
(< 1 . 2 > (
:: nil ::
[ nil | 
   -(g), 
   -(#0:NeNonceSet * n(a, #1:Fresh)), 
   +(exp(g, #0:NeNonceSet * n(a, #1:Fresh))), nil]  & 
:: #1:Fresh ::
[ nil, 
   +(a), 
   +(b), 
   +(exp(g, n(a, #1:Fresh))) | 
   -(b), 
   -(a), 
   -(exp(g, #0:NeNonceSet)), nil] )
|| 
exp(g, #0:NeNonceSet * n(a, #1:Fresh)) !inI,
(#0:NeNonceSet * n(a, #1:Fresh)) inI
|| 
-(g), 
-(#0:NeNonceSet * n(a, #1:Fresh)), 
+(exp(g, #0:NeNonceSet * n(a, #1:Fresh))), 
-(b), 
-(a), 
-(exp(g, #0:NeNonceSet))
|| 
ghost( exp(g, #0:NeNonceSet),
   :: nil ::
   [ nil | 
      -(g), 
      -(#0:NeNonceSet * n(a, #1:Fresh)), 
      +(exp(g, #0:NeNonceSet * n(a, #1:Fresh))), nil]  & 
   :: #1:Fresh ::
   [ nil, 
      +(a), 
      +(b), 
      +(exp(g, n(a, #1:Fresh))) | 
      -(b), 
      -(a), 
      -(exp(g, #0:NeNonceSet)), nil] ,    
   exp(g, #0:NeNonceSet * n(a, #1:Fresh)) !inI,
   (#0:NeNonceSet * n(a, #1:Fresh)) inI,    
   -(g), 
   -(#0:NeNonceSet * n(a, #1:Fresh)), 
   +(exp(g, #0:NeNonceSet * n(a, #1:Fresh))), 
   -(b), 
   -(a), 
   -(exp(g, #0:NeNonceSet)),    
   nil )
|| 
nil)
(< 1 . 5 > (
:: nil ::
[ nil | 
   -(exp(g, #0:NeNonceSet)), 
   -(#1:NeNonceSet * n(a, #2:Fresh)), 
   +(exp(g, #1:NeNonceSet * #0:NeNonceSet * n(a, #2:Fresh))), nil]  & 
:: #2:Fresh ::
[ nil, 
   +(a), 
   +(b), 
   +(exp(g, n(a, #2:Fresh))) | 
   -(b), 
   -(a), 
   -(exp(g, #1:NeNonceSet * #0:NeNonceSet)), nil] )
|| 
exp(g, #0:NeNonceSet) !inI,
exp(g, #1:NeNonceSet * #0:NeNonceSet * n(a, #2:Fresh)) !inI,
(#1:NeNonceSet * n(a, #2:Fresh)) inI
|| 
generatedByIntruder(exp(g, #0:NeNonceSet)), 
-(exp(g, #0:NeNonceSet)), 
-(#1:NeNonceSet * n(a, #2:Fresh)), 
+(exp(g, #1:NeNonceSet * #0:NeNonceSet * n(a, #2:Fresh))), 
-(b), 
-(a), 
-(exp(g, #1:NeNonceSet * #0:NeNonceSet))
|| 
ghost( exp(g, #1:NeNonceSet * #0:NeNonceSet),
   :: nil ::
   [ nil | 
      -(exp(g, #0:NeNonceSet)), 
      -(#1:NeNonceSet * n(a, #2:Fresh)), 
      +(exp(g, #1:NeNonceSet * #0:NeNonceSet * n(a, #2:Fresh))), nil]  & 
   :: #2:Fresh ::
   [ nil, 
      +(a), 
      +(b), 
      +(exp(g, n(a, #2:Fresh))) | 
      -(b), 
      -(a), 
      -(exp(g, #1:NeNonceSet * #0:NeNonceSet)), nil] ,    
   exp(g, #1:NeNonceSet * #0:NeNonceSet * n(a, #2:Fresh)) !inI,
   (#1:NeNonceSet * n(a, #2:Fresh)) inI,    
   -(exp(g, #0:NeNonceSet)), 
   -(#1:NeNonceSet * n(a, #2:Fresh)), 
   +(exp(g, #1:NeNonceSet * #0:NeNonceSet * n(a, #2:Fresh))), 
   -(b), 
   -(a), 
   -(exp(g, #1:NeNonceSet * #0:NeNonceSet)),    
   nil )
|| 
nil)
(< 1 . 6 > (
:: nil ::
[ nil | 
   -(exp(g, n(a, #0:Fresh))), 
   -(#1:NeNonceSet), 
   +(exp(g, #1:NeNonceSet * n(a, #0:Fresh))), nil]  & 
:: #0:Fresh ::
[ nil, 
   +(a), 
   +(b), 
   +(exp(g, n(a, #0:Fresh))) | 
   -(b), 
   -(a), 
   -(exp(g, #1:NeNonceSet)), nil] )
|| 
#1:NeNonceSet !inI,
exp(g, #1:NeNonceSet) !inI,
exp(g, #1:NeNonceSet * n(a, #0:Fresh)) !inI,
exp(g, n(a, #0:Fresh)) inI
|| 
generatedByIntruder(#1:NeNonceSet), 
generatedByIntruder(exp(g, #1:NeNonceSet)), 
-(exp(g, n(a, #0:Fresh))), 
-(#1:NeNonceSet), 
+(exp(g, #1:NeNonceSet * n(a, #0:Fresh))), 
-(b), 
-(a), 
-(exp(g, #1:NeNonceSet))
|| 
nil
|| 
nil)
< 1 . 7 > (
:: nil ::
[ nil | 
   -(exp(g, #0:NeNonceSet * n(a, #1:Fresh))), 
   -(#2:NeNonceSet), 
   +(exp(g, #2:NeNonceSet * #0:NeNonceSet * n(a, #1:Fresh))), nil]  & 
:: #1:Fresh ::
[ nil, 
   +(a), 
   +(b), 
   +(exp(g, n(a, #1:Fresh))) | 
   -(b), 
   -(a), 
   -(exp(g, #2:NeNonceSet * #0:NeNonceSet)), nil] )
|| 
#2:NeNonceSet !inI,
exp(g, #2:NeNonceSet * #0:NeNonceSet * n(a, #1:Fresh)) !inI,
exp(g, #0:NeNonceSet * n(a, #1:Fresh)) inI,
inst(#2:NeNonceSet)
|| 
generatedByIntruder(#2:NeNonceSet), 
-(exp(g, #0:NeNonceSet * n(a, #1:Fresh))), 
-(#2:NeNonceSet), 
+(exp(g, #2:NeNonceSet * #0:NeNonceSet * n(a, #1:Fresh))), 
-(b), 
-(a), 
-(exp(g, #2:NeNonceSet * #0:NeNonceSet))
|| 
ghost( exp(g, #2:NeNonceSet * #0:NeNonceSet),
   :: nil ::
   [ nil | 
      -(exp(g, #0:NeNonceSet * n(a, #1:Fresh))), 
      -(#2:NeNonceSet), 
      +(exp(g, #2:NeNonceSet * #0:NeNonceSet * n(a, #1:Fresh))), nil]  & 
   :: #1:Fresh ::
   [ nil, 
      +(a), 
      +(b), 
      +(exp(g, n(a, #1:Fresh))) | 
      -(b), 
      -(a), 
      -(exp(g, #2:NeNonceSet * #0:NeNonceSet)), nil] ,    
   exp(g, #2:NeNonceSet * #0:NeNonceSet * n(a, #1:Fresh)) !inI,
   exp(g, #0:NeNonceSet * n(a, #1:Fresh)) inI,
   inst(#2:NeNonceSet),    
   -(exp(g, #0:NeNonceSet * n(a, #1:Fresh))), 
   -(#2:NeNonceSet), 
   +(exp(g, #2:NeNonceSet * #0:NeNonceSet * n(a, #1:Fresh))), 
   -(b), 
   -(a), 
   -(exp(g, #2:NeNonceSet * #0:NeNonceSet)),    
   nil )
|| 
nil
==========================================
reduce in MAUDE-NPA : run(2) .
rewrites: 18 in 0ms cpu (0ms real) (253521 rewrites/second)
result IdSystem: < 1 . 6 . 1 > (
:: nil ::
[ nil | 
   -(exp(g, n(a, #0:Fresh))), 
   -(#1:NeNonceSet), 
   +(exp(g, #1:NeNonceSet * n(a, #0:Fresh))), nil]  & 
:: #0:Fresh ::
[ nil, 
   +(a), 
   +(b) | 
   +(exp(g, n(a, #0:Fresh))), 
   -(b), 
   -(a), 
   -(exp(g, #1:NeNonceSet)), nil] )
|| 
#1:NeNonceSet !inI,
exp(g, #1:NeNonceSet) !inI,
exp(g, n(a, #0:Fresh)) !inI,
exp(g, #1:NeNonceSet * n(a, #0:Fresh)) !inI
|| 
+(exp(g, n(a, #0:Fresh))), 
generatedByIntruder(#1:NeNonceSet), 
generatedByIntruder(exp(g, #1:NeNonceSet)), 
-(exp(g, n(a, #0:Fresh))), 
-(#1:NeNonceSet), 
+(exp(g, #1:NeNonceSet * n(a, #0:Fresh))), 
-(b), 
-(a), 
-(exp(g, #1:NeNonceSet))
|| 
nil
|| 
nil
==========================================
reduce in MAUDE-NPA : run(3) .
rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second)
result IdSystem: < 1 . 6 . 1 . 1 > (
:: nil ::
[ nil | 
   -(exp(g, n(a, #0:Fresh))), 
   -(#1:NeNonceSet), 
   +(exp(g, #1:NeNonceSet * n(a, #0:Fresh))), nil]  & 
:: #0:Fresh ::
[ nil, 
   +(a) | 
   +(b), 
   +(exp(g, n(a, #0:Fresh))), 
   -(b), 
   -(a), 
   -(exp(g, #1:NeNonceSet)), nil] )
|| 
#1:NeNonceSet !inI,
exp(g, #1:NeNonceSet) !inI,
exp(g, n(a, #0:Fresh)) !inI,
exp(g, #1:NeNonceSet * n(a, #0:Fresh)) !inI
|| 
+(b), 
+(exp(g, n(a, #0:Fresh))), 
generatedByIntruder(#1:NeNonceSet), 
generatedByIntruder(exp(g, #1:NeNonceSet)), 
-(exp(g, n(a, #0:Fresh))), 
-(#1:NeNonceSet), 
+(exp(g, #1:NeNonceSet * n(a, #0:Fresh))), 
-(b), 
-(a), 
-(exp(g, #1:NeNonceSet))
|| 
nil
|| 
nil
==========================================
reduce in MAUDE-NPA : run(4) .
rewrites: 18 in 0ms cpu (0ms real) (600000 rewrites/second)
result IdSystem: < 1 . 6 . 1 . 1 . 1 > (
:: nil ::
[ nil | 
   -(exp(g, n(a, #0:Fresh))), 
   -(#1:NeNonceSet), 
   +(exp(g, #1:NeNonceSet * n(a, #0:Fresh))), nil]  & 
:: #0:Fresh ::
[ nil | 
   +(a), 
   +(b), 
   +(exp(g, n(a, #0:Fresh))), 
   -(b), 
   -(a), 
   -(exp(g, #1:NeNonceSet)), nil] )
|| 
#1:NeNonceSet !inI,
exp(g, #1:NeNonceSet) !inI,
exp(g, n(a, #0:Fresh)) !inI,
exp(g, #1:NeNonceSet * n(a, #0:Fresh)) !inI
|| 
+(a), 
+(b), 
+(exp(g, n(a, #0:Fresh))), 
generatedByIntruder(#1:NeNonceSet), 
generatedByIntruder(exp(g, #1:NeNonceSet)), 
-(exp(g, n(a, #0:Fresh))), 
-(#1:NeNonceSet), 
+(exp(g, #1:NeNonceSet * n(a, #0:Fresh))), 
-(b), 
-(a), 
-(exp(g, #1:NeNonceSet))
|| 
nil
|| 
nil
Maude> Bye.
Wed Dec  5 02:37:25 CET 2012
Santiagos-MacBook-Pro:prototype-20121204 sescobar$