Santiagos-MacBook-Pro:prototype-20121204 sescobar$ examples/secret06-command 
Wed Dec  5 02:36:45 CET 2012
		     \||||||||||||||||||/
		   --- Welcome to Maude ---
		     /||||||||||||||||||\
	    Maude alpha96b built: Nov  9 2012 18:20:01
	    Copyright 1997-2011 SRI International
		   Wed Dec  5 02:36:45 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: 7359423 in 10548ms cpu (10630ms real) (697707 rewrites/second)
result GrammarList: (
grl #0:Msg inL => pk(i, #0:Msg) inL . ; 
grl #0:Msg inL => sk(#1:Key, #0:Msg) inL . ; 
grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; 
grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; 
grl #0:Msg notInI, #0:Msg notLeq (#1:Elm ; #2:Elm) => (#0:Msg ; #3:Msg) inL .)
| (
grl #0:Msg inL => pk(i, #0:Msg) inL . ; 
grl #0:Msg inL => sk(#1:Key, #0:Msg) inL . ; 
grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; 
grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; 
grl #0:Msg notInI, (#0:Msg notLeq n(a, #1:Fresh)), #0:Msg notLeq (#2:Elm ; #3:Elm) => (#0:Msg ; #4:Elm) inL . ; 
grl #0:Msg notInI, (#0:Msg notLeq n(a, #1:Fresh)), #0:Msg notLeq (#2:Elm ; #3:Elm) => (#4:Msg ; #0:Msg) inL .)
| (errorNoHeuristicApplied {
grl empty => (#1:Msg ; #2:Msg) inL .,none,
grl empty => (#1:Msg,#2:Msg) inL .,none,
grl empty => (#1:Msg,#2:Msg) inL .} usingGrammar 
grl empty => (#1:Msg ; #2:Msg) inL .)
| (
grl #0:Msg inL => pk(i, #0:Msg) inL . ; 
grl #0:Msg inL => sk(#1:Key, #0:Msg) inL . ; 
grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; 
grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; 
grl (n(#0:Name, #1:Fresh) notLeq n(s, #2:Fresh)), n(#0:Name, #1:Fresh) notLeq n(a, #3:Fresh) => n(#0:Name, #1:Fresh) inL .)
| (errorNoHeuristicApplied {
grl #50:Key notInI => pk(#50:Key, #60:Msg) inL .,none,
grl #50:Key notInI => #60:Msg inL .,none,
grl #50:Key notInI => #60:Msg inL .} usingGrammar 
grl #50:Key notInI => pk(#50:Key, #60:Msg) inL .)
| (
grl #0:Msg inL => pk(i, #0:Msg) inL . ; 
grl #0:Msg inL => sk(#1:Key, #0:Msg) inL . ; 
grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; 
grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; 
grl #0:Msg notInI => pk(#1:Key, #0:Msg) inL .)
| (errorNoHeuristicApplied {
grl empty => pk(#1:Key, #2:Msg) inL .,none,
grl empty => #2:Msg inL .,none,
grl empty => #2:Msg inL .} usingGrammar 
grl empty => pk(#1:Key, #2:Msg) inL .)
| (
grl #0:Msg inL => pk(i, #0:Msg) inL . ; 
grl #0:Msg inL => sk(#1:Key, #0:Msg) inL . ; 
grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; 
grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; 
grl #0:Key notInI => sk(#0:Key, #1:Msg) inL .)
| (
grl #0:Msg inL => pk(i, #0:Msg) inL . ; 
grl #0:Msg inL => sk(#1:Key, #0:Msg) inL . ; 
grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; 
grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; 
grl #0:Msg notInI, (#0:Msg notLeq (#1:Nonce ; s)), #0:Msg notLeq ((b ; n(a, #2:Fresh)) ; s) => sk(#3:Key, #0:Msg) inL .)
| 
grl #0:Msg inL => pk(i, #0:Msg) inL . ; 
grl #0:Msg inL => sk(#1:Key, #0:Msg) inL . ; 
grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; 
grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; 
grl (sk(#0:Key, #1:Msg) notLeq sk(a, #2:Nonce ; s)), (sk(#0:Key, #1:Msg) notLeq sk(a, (b ; n(a, #3:Fresh)) ; s)), sk(#0:Key, #1:Msg) notLeq sk(i, #4:Msg) => sk(#0:Key, #1:Msg) inL .
==========================================
reduce in MAUDE-NPA : run(0) .
rewrites: 2361 in 19ms cpu (29ms real) (119853 rewrites/second)
result IdSystem: < 1 > 
:: nil ::
[ nil, 
   -(sk(a, X:Msg ; s)), 
   -(sk(a, (b ; N:Nonce) ; s)) | nil] 
|| empty
|| 
nil
|| 
nil
|| 
nil
==========================================
reduce in MAUDE-NPA : summary(1) .
rewrites: 1271524 in 2541ms cpu (2562ms real) (500388 rewrites/second)
result Summary: States>> 2 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(2) .
rewrites: 536004 in 1372ms cpu (1382ms real) (390570 rewrites/second)
result Summary: States>> 3 Solutions>> 1
==========================================
reduce in MAUDE-NPA : summary(3) .
rewrites: 243212 in 553ms cpu (566ms real) (439029 rewrites/second)
result Summary: States>> 2 Solutions>> 2
==========================================
reduce in MAUDE-NPA : run(1) .
rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second)
result IdSystemSet: (< 1 . 9 > (
:: nil ::
[ nil | 
   -(sk(a, #2:Msg ; s)), 
   -(sk(a, (b ; n(a, #0:Fresh)) ; s)), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(#1:Nonce), 
   +(sk(a, #1:Nonce ; s)) | 
   +(sk(a, (b ; n(a, #0:Fresh)) ; s)), nil] )
|| 
sk(a, (b ; n(a, #0:Fresh)) ; s) !inI,
sk(a, #2:Msg ; s) inI
|| 
+(sk(a, (b ; n(a, #0:Fresh)) ; s)), 
-(sk(a, #2:Msg ; s)), 
-(sk(a, (b ; n(a, #0:Fresh)) ; s))
|| 
nil
|| 
nil)
< 1 . 10 > (
:: nil ::
[ nil | 
   -(sk(a, #1:Nonce ; s)), 
   -(sk(a, (b ; #2:Nonce) ; s)), nil]  & 
:: #0:Fresh ::
[ nil | 
   -(#1:Nonce), 
   +(sk(a, #1:Nonce ; s)), nil] )
|| 
#1:Nonce !inI,
sk(a, #1:Nonce ; s) !inI,
sk(a, (b ; #2:Nonce) ; s) inI,
inst(#1:Nonce)
|| 
generatedByIntruder(#1:Nonce), 
-(#1:Nonce), 
+(sk(a, #1:Nonce ; s)), 
-(sk(a, #1:Nonce ; s)), 
-(sk(a, (b ; #2:Nonce) ; s))
|| 
nil
|| 
nil
==========================================
reduce in MAUDE-NPA : run(2) .
rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second)
result IdSystemSet: (< 1 . 9 . 1 > (
:: nil ::
[ nil | 
   -(sk(a, #2:Msg ; s)), 
   -(sk(a, (b ; n(a, #0:Fresh)) ; s)), nil]  & 
:: #0:Fresh ::
[ nil | 
   -(#1:Nonce), 
   +(sk(a, #1:Nonce ; s)), 
   +(sk(a, (b ; n(a, #0:Fresh)) ; s)), nil] )
|| 
#1:Nonce !inI,
sk(a, (b ; n(a, #0:Fresh)) ; s) !inI,
sk(a, #2:Msg ; s) inI
|| 
generatedByIntruder(#1:Nonce), 
-(#1:Nonce), 
+(sk(a, #1:Nonce ; s)), 
+(sk(a, (b ; n(a, #0:Fresh)) ; s)), 
-(sk(a, #2:Msg ; s)), 
-(sk(a, (b ; n(a, #0:Fresh)) ; s))
|| 
nil
|| 
nil)
(< 1 . 9 . 2 > (
:: nil ::
[ nil | 
   -(sk(a, #1:Nonce ; s)), 
   -(sk(a, (b ; n(a, #0:Fresh)) ; s)), nil]  & 
:: #0:Fresh ::
[ nil | 
   -(#1:Nonce), 
   +(sk(a, #1:Nonce ; s)), 
   +(sk(a, (b ; n(a, #0:Fresh)) ; s)), nil] )
|| 
#1:Nonce !inI,
sk(a, #1:Nonce ; s) !inI,
sk(a, (b ; n(a, #0:Fresh)) ; s) !inI,
inst(#1:Nonce)
|| 
generatedByIntruder(#1:Nonce), 
-(#1:Nonce), 
+(sk(a, #1:Nonce ; s)), 
+(sk(a, (b ; n(a, #0:Fresh)) ; s)), 
-(sk(a, #1:Nonce ; s)), 
-(sk(a, (b ; n(a, #0:Fresh)) ; s))
|| 
nil
|| 
nil)
< 1 . 9 . 7 > (
:: nil ::
[ nil | 
   -(sk(a, #3:Nonce ; s)), 
   -(sk(a, (b ; n(a, #0:Fresh)) ; s)), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(#1:Nonce), 
   +(sk(a, #1:Nonce ; s)) | 
   +(sk(a, (b ; n(a, #0:Fresh)) ; s)), nil]  & 
:: #2:Fresh ::
[ nil | 
   -(#3:Nonce), 
   +(sk(a, #3:Nonce ; s)), nil] )
|| 
#3:Nonce !inI,
sk(a, #3:Nonce ; s) !inI,
sk(a, (b ; n(a, #0:Fresh)) ; s) !inI,
inst(#3:Nonce)
|| 
generatedByIntruder(#3:Nonce), 
-(#3:Nonce), 
+(sk(a, #3:Nonce ; s)), 
+(sk(a, (b ; n(a, #0:Fresh)) ; s)), 
-(sk(a, #3:Nonce ; s)), 
-(sk(a, (b ; n(a, #0:Fresh)) ; s))
|| 
nil
|| 
nil
==========================================
reduce in MAUDE-NPA : run(3) .
rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second)
result IdSystemSet: (< 1 . 9 . 2 > (
:: nil ::
[ nil | 
   -(sk(a, #1:Nonce ; s)), 
   -(sk(a, (b ; n(a, #0:Fresh)) ; s)), nil]  & 
:: #0:Fresh ::
[ nil | 
   -(#1:Nonce), 
   +(sk(a, #1:Nonce ; s)), 
   +(sk(a, (b ; n(a, #0:Fresh)) ; s)), nil] )
|| 
#1:Nonce !inI,
sk(a, #1:Nonce ; s) !inI,
sk(a, (b ; n(a, #0:Fresh)) ; s) !inI,
inst(#1:Nonce)
|| 
generatedByIntruder(#1:Nonce), 
-(#1:Nonce), 
+(sk(a, #1:Nonce ; s)), 
+(sk(a, (b ; n(a, #0:Fresh)) ; s)), 
-(sk(a, #1:Nonce ; s)), 
-(sk(a, (b ; n(a, #0:Fresh)) ; s))
|| 
nil
|| 
nil)
< 1 . 9 . 1 . 5 > (
:: nil ::
[ nil | 
   -(sk(a, #1:Nonce ; s)), 
   -(sk(a, (b ; n(a, #2:Fresh)) ; s)), nil]  & 
:: #0:Fresh ::
[ nil | 
   -(#1:Nonce), 
   +(sk(a, #1:Nonce ; s)), nil]  & 
:: #2:Fresh ::
[ nil | 
   -(#3:Nonce), 
   +(sk(a, #3:Nonce ; s)), 
   +(sk(a, (b ; n(a, #2:Fresh)) ; s)), nil] )
|| 
#3:Nonce !inI,
#1:Nonce !inI,
sk(a, #1:Nonce ; s) !inI,
sk(a, (b ; n(a, #2:Fresh)) ; s) !inI,
inst(#3:Nonce)
|| 
generatedByIntruder(#1:Nonce), 
-(#1:Nonce), 
+(sk(a, #1:Nonce ; s)), 
generatedByIntruder(#3:Nonce), 
-(#3:Nonce), 
+(sk(a, #3:Nonce ; s)), 
+(sk(a, (b ; n(a, #2:Fresh)) ; s)), 
-(sk(a, #1:Nonce ; s)), 
-(sk(a, (b ; n(a, #2:Fresh)) ; s))
|| 
nil
|| 
nil
Maude> Bye.
Wed Dec  5 02:37:01 CET 2012
Santiagos-MacBook-Pro:prototype-20121204 sescobar$