Santiagos-MacBook-Pro:prototype-20121204 sescobar$ examples/Needham_Schroeder_Lowe-command 
Wed Dec  5 02:00:52 CET 2012
		     \||||||||||||||||||/
		   --- Welcome to Maude ---
		     /||||||||||||||||||\
	    Maude alpha96b built: Nov  9 2012 18:20:01
	    Copyright 1997-2011 SRI International
		   Wed Dec  5 02:00:52 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: 7737969 in 11267ms cpu (11357ms real) (686740 rewrites/second)
result GrammarList: (
grl #0:Msg inL => pk(#1:Name, #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(#1:Name, #2:Fresh) => (#0:Msg ; #3:Msg) inL . ; 
grl #0:Msg notInI, #0:Msg notLeq n(#1:Name, #2:Fresh) => (#3:Name ; #0:Msg) inL .)
| (
grl #0:Msg inL => pk(#1:Name, #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(#1:Name, #2:Fresh)), #0:Msg notLeq n(#3:Name, #4:Fresh) ; #3:Name => (#5: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 .)
| (errorInconsistentExceptionsInGrammarRule 
grl n(#0:Name, #1:Fresh) notLeq #1:Nonce => n(#0:Name, #1:Fresh) inL . inGrammar 
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 #5:Msg inL => pk(#3:Name, #5:Msg) inL . ; 
grl n(#0:Name, #1:Fresh) notLeq #1:Nonce => 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(#1:Name, #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), (#0:Msg notLeq #2:Name ; n(#2:Name, #3:Fresh)), #0:Msg notLeq #4:Nonce ; n(#5:Name, #6:Fresh) ; #5:Name => pk(#7: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(#1:Name, #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(#1:Name, #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 => sk(#1:Key, #0:Msg) inL .)
| 
grl #0:Msg inL => pk(#1:Name, #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(i, #2:Msg) => sk(#0:Key, #1:Msg) inL .
==========================================
reduce in MAUDE-NPA : run(0) .
rewrites: 2530 in 29ms cpu (30ms real) (85216 rewrites/second)
result IdSystem: < 1 > 
:: r:Fresh ::
[ nil, 
   -(pk(b, a ; N:Nonce)), 
   +(pk(a, N:Nonce ; n(b, r:Fresh) ; b)), 
   -(pk(b, n(b, r:Fresh))) | nil] 
|| 
n(b, r:Fresh) inI
|| 
nil
|| 
nil
|| 
nil
==========================================
reduce in MAUDE-NPA : summary(1) .
rewrites: 735726 in 1187ms cpu (1193ms real) (619394 rewrites/second)
result Summary: States>> 4 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(2) .
rewrites: 1283417 in 2290ms cpu (2309ms real) (560411 rewrites/second)
result Summary: States>> 7 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(3) .
rewrites: 2563812 in 5050ms cpu (5090ms real) (507662 rewrites/second)
result Summary: States>> 6 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(4) .
rewrites: 2049944 in 4326ms cpu (4361ms real) (473819 rewrites/second)
result Summary: States>> 2 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(5) .
rewrites: 500208 in 1133ms cpu (1152ms real) (441165 rewrites/second)
result Summary: States>> 0 Solutions>> 0
==========================================
reduce in MAUDE-NPA : run(1) .
rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second)
result IdSystemSet: (< 1 . 2 > (
:: nil ::
[ nil | 
   -(pk(i, n(b, #0:Fresh))), 
   +(n(b, #0:Fresh)), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #1:Nonce)), 
   +(pk(a, #1:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil] )
|| 
n(b, #0:Fresh) !inI,
pk(b, n(b, #0:Fresh)) inI,
pk(i, n(b, #0:Fresh)) inI
|| 
-(pk(i, n(b, #0:Fresh))), 
+(n(b, #0:Fresh)), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 5 > (
:: nil ::
[ nil | 
   -(n(b, #0:Fresh)), 
   +(pk(b, n(b, #0:Fresh))), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #1:Nonce)), 
   +(pk(a, #1:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil] )
|| 
pk(b, n(b, #0:Fresh)) !inI,
n(b, #0:Fresh) inI
|| 
-(n(b, #0:Fresh)), 
+(pk(b, n(b, #0:Fresh))), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 7 > (
:: nil ::
[ nil | 
   -(#0:Msg ; n(b, #1:Fresh)), 
   +(n(b, #1:Fresh)), nil]  & 
:: #1:Fresh ::
[ nil, 
   -(pk(b, a ; #2:Nonce)), 
   +(pk(a, #2:Nonce ; n(b, #1:Fresh) ; b)) | 
   -(pk(b, n(b, #1:Fresh))), nil] )
|| 
n(b, #1:Fresh) !inI,
pk(b, n(b, #1:Fresh)) inI,
(#0:Msg ; n(b, #1:Fresh)) inI
|| 
-(#0:Msg ; n(b, #1:Fresh)), 
+(n(b, #1:Fresh)), 
-(pk(b, n(b, #1:Fresh)))
|| 
nil
|| 
nil)
< 1 . 9 > (
:: nil ::
[ nil | 
   -(n(b, #0:Fresh) ; #1:Msg), 
   +(n(b, #0:Fresh)), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #2:Nonce)), 
   +(pk(a, #2:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil] )
|| 
n(b, #0:Fresh) !inI,
pk(b, n(b, #0:Fresh)) inI,
(n(b, #0:Fresh) ; #1:Msg) inI
|| 
-(n(b, #0:Fresh) ; #1:Msg), 
+(n(b, #0:Fresh)), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil
==========================================
reduce in MAUDE-NPA : run(2) .
rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second)
result IdSystemSet: (< 1 . 2 . 9 > (
:: nil ::
[ nil | 
   -(pk(i, n(b, #0:Fresh))), 
   +(n(b, #0:Fresh)), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #1:Nonce)), 
   +(pk(a, #1:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil]  & 
:: #2:Fresh ::
[ nil, 
   +(pk(i, #3:Name ; n(#3:Name, #2:Fresh))) | 
   -(pk(#3:Name, n(#3:Name, #2:Fresh) ; n(b, #0:Fresh) ; i)), 
   +(pk(i, n(b, #0:Fresh))), nil] )
|| 
pk(i, n(b, #0:Fresh)) !inI,
n(b, #0:Fresh) !inI,
pk(b, n(b, #0:Fresh)) inI,
pk(#3:Name, n(#3:Name, #2:Fresh) ; n(b, #0:Fresh) ; i) inI
|| 
-(pk(#3:Name, n(#3:Name, #2:Fresh) ; n(b, #0:Fresh) ; i)), 
+(pk(i, n(b, #0:Fresh))), 
-(pk(i, n(b, #0:Fresh))), 
+(n(b, #0:Fresh)), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 5 . 2 > (
:: nil ::
[ nil | 
   -(pk(i, n(b, #0:Fresh))), 
   +(n(b, #0:Fresh)), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #0:Fresh)), 
   +(pk(b, n(b, #0:Fresh))), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #1:Nonce)), 
   +(pk(a, #1:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil] )
|| 
pk(b, n(b, #0:Fresh)) !inI,
n(b, #0:Fresh) !inI,
pk(i, n(b, #0:Fresh)) inI
|| 
-(pk(i, n(b, #0:Fresh))), 
+(n(b, #0:Fresh)), 
-(n(b, #0:Fresh)), 
+(pk(b, n(b, #0:Fresh))), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 5 . 4 > (
:: nil ::
[ nil | 
   -(n(b, #0:Fresh)), 
   +(pk(b, n(b, #0:Fresh))), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #0:Fresh) ; #1:Msg), 
   +(n(b, #0:Fresh)), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #2:Nonce)), 
   +(pk(a, #2:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil] )
|| 
pk(b, n(b, #0:Fresh)) !inI,
n(b, #0:Fresh) !inI,
(n(b, #0:Fresh) ; #1:Msg) inI
|| 
-(n(b, #0:Fresh) ; #1:Msg), 
+(n(b, #0:Fresh)), 
-(n(b, #0:Fresh)), 
+(pk(b, n(b, #0:Fresh))), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 5 . 5 > (
:: nil ::
[ nil | 
   -(n(b, #1:Fresh)), 
   +(pk(b, n(b, #1:Fresh))), nil]  & 
:: nil ::
[ nil | 
   -(#0:Msg ; n(b, #1:Fresh)), 
   +(n(b, #1:Fresh)), nil]  & 
:: #1:Fresh ::
[ nil, 
   -(pk(b, a ; #2:Nonce)), 
   +(pk(a, #2:Nonce ; n(b, #1:Fresh) ; b)) | 
   -(pk(b, n(b, #1:Fresh))), nil] )
|| 
pk(b, n(b, #1:Fresh)) !inI,
n(b, #1:Fresh) !inI,
(#0:Msg ; n(b, #1:Fresh)) inI
|| 
-(#0:Msg ; n(b, #1:Fresh)), 
+(n(b, #1:Fresh)), 
-(n(b, #1:Fresh)), 
+(pk(b, n(b, #1:Fresh))), 
-(pk(b, n(b, #1:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 7 . 4 > (
:: nil ::
[ nil | 
   -(pk(i, #0:Msg ; n(b, #1:Fresh))), 
   +(#0:Msg ; n(b, #1:Fresh)), nil]  & 
:: nil ::
[ nil | 
   -(#0:Msg ; n(b, #1:Fresh)), 
   +(n(b, #1:Fresh)), nil]  & 
:: #1:Fresh ::
[ nil, 
   -(pk(b, a ; #2:Nonce)), 
   +(pk(a, #2:Nonce ; n(b, #1:Fresh) ; b)) | 
   -(pk(b, n(b, #1:Fresh))), nil] )
|| 
n(b, #1:Fresh) !inI,
(#0:Msg ; n(b, #1:Fresh)) !inI,
pk(b, n(b, #1:Fresh)) inI,
pk(i, #0:Msg ; n(b, #1:Fresh)) inI
|| 
-(pk(i, #0:Msg ; n(b, #1:Fresh))), 
+(#0:Msg ; n(b, #1:Fresh)), 
-(#0:Msg ; n(b, #1:Fresh)), 
+(n(b, #1:Fresh)), 
-(pk(b, n(b, #1:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 9 . 3 > (
:: nil ::
[ nil | 
   -(pk(i, n(b, #0:Fresh) ; #1:Msg)), 
   +(n(b, #0:Fresh) ; #1:Msg), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #0:Fresh) ; #1:Msg), 
   +(n(b, #0:Fresh)), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #2:Nonce)), 
   +(pk(a, #2:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil] )
|| 
n(b, #0:Fresh) !inI,
(n(b, #0:Fresh) ; #1:Msg) !inI,
pk(b, n(b, #0:Fresh)) inI,
pk(i, n(b, #0:Fresh) ; #1:Msg) inI
|| 
-(pk(i, n(b, #0:Fresh) ; #1:Msg)), 
+(n(b, #0:Fresh) ; #1:Msg), 
-(n(b, #0:Fresh) ; #1:Msg), 
+(n(b, #0:Fresh)), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil)
< 1 . 9 . 9 > (
:: nil ::
[ nil | 
   -(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), 
   +(n(b, #1:Fresh) ; #2:Msg), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #1:Fresh) ; #2:Msg), 
   +(n(b, #1:Fresh)), nil]  & 
:: #1:Fresh ::
[ nil, 
   -(pk(b, a ; #3:Nonce)), 
   +(pk(a, #3:Nonce ; n(b, #1:Fresh) ; b)) | 
   -(pk(b, n(b, #1:Fresh))), nil] )
|| 
n(b, #1:Fresh) !inI,
(n(b, #1:Fresh) ; #2:Msg) !inI,
pk(b, n(b, #1:Fresh)) inI,
(#0:Msg ; n(b, #1:Fresh) ; #2:Msg) inI
|| 
-(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), 
+(n(b, #1:Fresh) ; #2:Msg), 
-(n(b, #1:Fresh) ; #2:Msg), 
+(n(b, #1:Fresh)), 
-(pk(b, n(b, #1:Fresh)))
|| 
nil
|| 
nil
==========================================
reduce in MAUDE-NPA : run(3) .
rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second)
result IdSystemSet: (< 1 . 5 . 2 . 5 > (
:: nil ::
[ nil | 
   -(pk(i, n(b, #0:Fresh))), 
   +(n(b, #0:Fresh)), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #0:Fresh)), 
   +(pk(b, n(b, #0:Fresh))), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #1:Nonce)), 
   +(pk(a, #1:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil]  & 
:: #2:Fresh ::
[ nil, 
   +(pk(i, #3:Name ; n(#3:Name, #2:Fresh))) | 
   -(pk(#3:Name, n(#3:Name, #2:Fresh) ; n(b, #0:Fresh) ; i)), 
   +(pk(i, n(b, #0:Fresh))), nil] )
|| 
pk(b, n(b, #0:Fresh)) !inI,
pk(i, n(b, #0:Fresh)) !inI,
n(b, #0:Fresh) !inI,
pk(#3:Name, n(#3:Name, #2:Fresh) ; n(b, #0:Fresh) ; i) inI
|| 
-(pk(#3:Name, n(#3:Name, #2:Fresh) ; n(b, #0:Fresh) ; i)), 
+(pk(i, n(b, #0:Fresh))), 
-(pk(i, n(b, #0:Fresh))), 
+(n(b, #0:Fresh)), 
-(n(b, #0:Fresh)), 
+(pk(b, n(b, #0:Fresh))), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 5 . 4 . 2 > (
:: nil ::
[ nil | 
   -(pk(i, n(b, #0:Fresh) ; #1:Msg)), 
   +(n(b, #0:Fresh) ; #1:Msg), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #0:Fresh)), 
   +(pk(b, n(b, #0:Fresh))), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #0:Fresh) ; #1:Msg), 
   +(n(b, #0:Fresh)), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #2:Nonce)), 
   +(pk(a, #2:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil] )
|| 
pk(b, n(b, #0:Fresh)) !inI,
n(b, #0:Fresh) !inI,
(n(b, #0:Fresh) ; #1:Msg) !inI,
pk(i, n(b, #0:Fresh) ; #1:Msg) inI
|| 
-(pk(i, n(b, #0:Fresh) ; #1:Msg)), 
+(n(b, #0:Fresh) ; #1:Msg), 
-(n(b, #0:Fresh) ; #1:Msg), 
+(n(b, #0:Fresh)), 
-(n(b, #0:Fresh)), 
+(pk(b, n(b, #0:Fresh))), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 5 . 4 . 6 > (
:: nil ::
[ nil | 
   -(n(b, #1:Fresh)), 
   +(pk(b, n(b, #1:Fresh))), nil]  & 
:: nil ::
[ nil | 
   -(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), 
   +(n(b, #1:Fresh) ; #2:Msg), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #1:Fresh) ; #2:Msg), 
   +(n(b, #1:Fresh)), nil]  & 
:: #1:Fresh ::
[ nil, 
   -(pk(b, a ; #3:Nonce)), 
   +(pk(a, #3:Nonce ; n(b, #1:Fresh) ; b)) | 
   -(pk(b, n(b, #1:Fresh))), nil] )
|| 
pk(b, n(b, #1:Fresh)) !inI,
n(b, #1:Fresh) !inI,
(n(b, #1:Fresh) ; #2:Msg) !inI,
(#0:Msg ; n(b, #1:Fresh) ; #2:Msg) inI
|| 
-(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), 
+(n(b, #1:Fresh) ; #2:Msg), 
-(n(b, #1:Fresh) ; #2:Msg), 
+(n(b, #1:Fresh)), 
-(n(b, #1:Fresh)), 
+(pk(b, n(b, #1:Fresh))), 
-(pk(b, n(b, #1:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 5 . 5 . 3 > (
:: nil ::
[ nil | 
   -(pk(i, #0:Msg ; n(b, #1:Fresh))), 
   +(#0:Msg ; n(b, #1:Fresh)), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #1:Fresh)), 
   +(pk(b, n(b, #1:Fresh))), nil]  & 
:: nil ::
[ nil | 
   -(#0:Msg ; n(b, #1:Fresh)), 
   +(n(b, #1:Fresh)), nil]  & 
:: #1:Fresh ::
[ nil, 
   -(pk(b, a ; #2:Nonce)), 
   +(pk(a, #2:Nonce ; n(b, #1:Fresh) ; b)) | 
   -(pk(b, n(b, #1:Fresh))), nil] )
|| 
pk(b, n(b, #1:Fresh)) !inI,
n(b, #1:Fresh) !inI,
(#0:Msg ; n(b, #1:Fresh)) !inI,
pk(i, #0:Msg ; n(b, #1:Fresh)) inI
|| 
-(pk(i, #0:Msg ; n(b, #1:Fresh))), 
+(#0:Msg ; n(b, #1:Fresh)), 
-(#0:Msg ; n(b, #1:Fresh)), 
+(n(b, #1:Fresh)), 
-(n(b, #1:Fresh)), 
+(pk(b, n(b, #1:Fresh))), 
-(pk(b, n(b, #1:Fresh)))
|| 
nil
|| 
nil)
(< 1 . 9 . 3 . 9 > (
:: nil ::
[ nil | 
   -(pk(i, n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name)), 
   +(n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name), 
   +(n(b, #0:Fresh)), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #1:Nonce)), 
   +(pk(a, #1:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil]  & 
:: #2:Fresh ::
[ nil | 
   -(pk(#3:Name, i ; n(b, #0:Fresh))), 
   +(pk(i, n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name)), nil] )
|| 
pk(i, n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name) !inI,
n(b, #0:Fresh) !inI,
(n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name) !inI,
pk(b, n(b, #0:Fresh)) inI,
pk(#3:Name, i ; n(b, #0:Fresh)) inI
|| 
-(pk(#3:Name, i ; n(b, #0:Fresh))), 
+(pk(i, n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name)), 
-(pk(i, n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name)), 
+(n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name), 
-(n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name), 
+(n(b, #0:Fresh)), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil)
< 1 . 9 . 9 . 4 > (
:: nil ::
[ nil | 
   -(pk(i, #0:Msg ; n(b, #1:Fresh) ; #2:Msg)), 
   +(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), nil]  & 
:: nil ::
[ nil | 
   -(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), 
   +(n(b, #1:Fresh) ; #2:Msg), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #1:Fresh) ; #2:Msg), 
   +(n(b, #1:Fresh)), nil]  & 
:: #1:Fresh ::
[ nil, 
   -(pk(b, a ; #3:Nonce)), 
   +(pk(a, #3:Nonce ; n(b, #1:Fresh) ; b)) | 
   -(pk(b, n(b, #1:Fresh))), nil] )
|| 
n(b, #1:Fresh) !inI,
(#0:Msg ; n(b, #1:Fresh) ; #2:Msg) !inI,
(n(b, #1:Fresh) ; #2:Msg) !inI,
pk(b, n(b, #1:Fresh)) inI,
pk(i, #0:Msg ; n(b, #1:Fresh) ; #2:Msg) inI
|| 
-(pk(i, #0:Msg ; n(b, #1:Fresh) ; #2:Msg)), 
+(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), 
-(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), 
+(n(b, #1:Fresh) ; #2:Msg), 
-(n(b, #1:Fresh) ; #2:Msg), 
+(n(b, #1:Fresh)), 
-(pk(b, n(b, #1:Fresh)))
|| 
nil
|| 
nil
==========================================
reduce in MAUDE-NPA : run(4) .
rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second)
result IdSystemSet: (< 1 . 5 . 4 . 2 . 5 > (
:: nil ::
[ nil | 
   -(pk(i, n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name)), 
   +(n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #0:Fresh)), 
   +(pk(b, n(b, #0:Fresh))), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name), 
   +(n(b, #0:Fresh)), nil]  & 
:: #0:Fresh ::
[ nil, 
   -(pk(b, a ; #1:Nonce)), 
   +(pk(a, #1:Nonce ; n(b, #0:Fresh) ; b)) | 
   -(pk(b, n(b, #0:Fresh))), nil]  & 
:: #2:Fresh ::
[ nil | 
   -(pk(#3:Name, i ; n(b, #0:Fresh))), 
   +(pk(i, n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name)), nil] )
|| 
pk(b, n(b, #0:Fresh)) !inI,
pk(i, n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name) !inI,
n(b, #0:Fresh) !inI,
(n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name) !inI,
pk(#3:Name, i ; n(b, #0:Fresh)) inI
|| 
-(pk(#3:Name, i ; n(b, #0:Fresh))), 
+(pk(i, n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name)), 
-(pk(i, n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name)), 
+(n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name), 
-(n(b, #0:Fresh) ; n(#3:Name, #2:Fresh) ; #3:Name), 
+(n(b, #0:Fresh)), 
-(n(b, #0:Fresh)), 
+(pk(b, n(b, #0:Fresh))), 
-(pk(b, n(b, #0:Fresh)))
|| 
nil
|| 
nil)
< 1 . 5 . 4 . 6 . 3 > (
:: nil ::
[ nil | 
   -(pk(i, #0:Msg ; n(b, #1:Fresh) ; #2:Msg)), 
   +(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #1:Fresh)), 
   +(pk(b, n(b, #1:Fresh))), nil]  & 
:: nil ::
[ nil | 
   -(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), 
   +(n(b, #1:Fresh) ; #2:Msg), nil]  & 
:: nil ::
[ nil | 
   -(n(b, #1:Fresh) ; #2:Msg), 
   +(n(b, #1:Fresh)), nil]  & 
:: #1:Fresh ::
[ nil, 
   -(pk(b, a ; #3:Nonce)), 
   +(pk(a, #3:Nonce ; n(b, #1:Fresh) ; b)) | 
   -(pk(b, n(b, #1:Fresh))), nil] )
|| 
pk(b, n(b, #1:Fresh)) !inI,
n(b, #1:Fresh) !inI,
(#0:Msg ; n(b, #1:Fresh) ; #2:Msg) !inI,
(n(b, #1:Fresh) ; #2:Msg) !inI,
pk(i, #0:Msg ; n(b, #1:Fresh) ; #2:Msg) inI
|| 
-(pk(i, #0:Msg ; n(b, #1:Fresh) ; #2:Msg)), 
+(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), 
-(#0:Msg ; n(b, #1:Fresh) ; #2:Msg), 
+(n(b, #1:Fresh) ; #2:Msg), 
-(n(b, #1:Fresh) ; #2:Msg), 
+(n(b, #1:Fresh)), 
-(n(b, #1:Fresh)), 
+(pk(b, n(b, #1:Fresh))), 
-(pk(b, n(b, #1:Fresh)))
|| 
nil
|| 
nil
==========================================
reduce in MAUDE-NPA : run(5) .
rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second)
result IdSystemSet: (empty).IdSystemSet
Maude> Bye.
Wed Dec  5 02:01:19 CET 2012
Santiagos-MacBook-Pro:prototype-20121204 sescobar$