Santiagos-MacBook-Pro:prototype-20121204 sescobar$ examples/Carlsen_Secret_Key_Initiator-command Wed Dec 5 10:19:18 CET 2012 \||||||||||||||||||/ --- Welcome to Maude --- /||||||||||||||||||\ Maude alpha96b built: Nov 9 2012 18:20:01 Copyright 1997-2011 SRI International Wed Dec 5 10:19:18 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: 53899085 in 70140ms cpu (70413ms real) (768448 rewrites/second) result GrammarList: ( grl #0:Msg inL => e(#1:Key, #0:Msg) inL . ; grl #0:Msg inL => d(#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:UName, #2:Fresh)), (#0:Msg notLeq e(#3:Sessionkey, #4:Nonce)), (#0:Msg notLeq e(mkey(s, #5:UName), seskey(#6:UName, #5:UName, n(#7:UName, #8:Fresh)) ; #9:Nonce ; #6:UName)), (#0:Msg notLeq e( mkey(s, #10:UName), #11:Nonce ; #12:UName ; seskey(#10:UName, #12:UName, n(#13:UName, #14:Fresh)))), (#0:Msg notLeq #15:Nonce ; #16:UName ; n(#16:UName, #17:Fresh)), (#0:Msg notLeq e(#18:Sessionkey, #19:Nonce) ; n(#20:UName, #21:Fresh)), #0:Msg notLeq seskey(#22:UName, #23:UName, n(#24:UName, #25:Fresh)) => (#0:Msg ; #26:Msg) inL . ; grl #0:Msg notInI, (#0:Msg notLeq n(#1:UName, #2:Fresh)), (#0:Msg notLeq e(#3:Sessionkey, #4:Nonce)), (#0:Msg notLeq e(mkey(s, #5:UName), seskey(#6:UName, #5:UName, n(#7:UName, #8:Fresh)) ; #9:Nonce ; #6:UName)), (#0:Msg notLeq e( mkey(s, #10:UName), #11:Nonce ; #12:UName ; seskey(#10:UName, #12:UName, n(#13:UName, #14:Fresh)))), (#0:Msg notLeq #15:Nonce ; #16:UName ; n(#16:UName, #17:Fresh)), (#0:Msg notLeq e(#18:Sessionkey, #19:Nonce) ; n(#20:UName, #21:Fresh)), #0:Msg notLeq seskey(#22:UName, #23:UName, n(#24:UName, #25:Fresh)) => (#26:UName ; #0:Msg) inL . ; grl #0:Msg notInI, (#0:Msg notLeq n(#1:UName, #2:Fresh)), (#0:Msg notLeq e(#3:Sessionkey, #4:Nonce)), (#0:Msg notLeq e(mkey(s, #5:UName), seskey(#6:UName, #5:UName, n(#7:UName, #8:Fresh)) ; #9:Nonce ; #6:UName)), (#0:Msg notLeq e( mkey(s, #10:UName), #11:Nonce ; #12:UName ; seskey(#10:UName, #12:UName, n(#13:UName, #14:Fresh)))), (#0:Msg notLeq #15:Nonce ; #16:UName ; n(#16:UName, #17:Fresh)), (#0:Msg notLeq e(#18:Sessionkey, #19:Nonce) ; n(#20:UName, #21:Fresh)), #0:Msg notLeq seskey(#22:UName, #23:UName, n(#24:UName, #25:Fresh)) => (e(mkey(s, #26:UName), #27:Sessionkey ; n(#26:UName, #28:Fresh) ; #29:UName) ; #0:Msg) inL .) | ( grl #0:Msg inL => e(#1:Key, #0:Msg) inL . ; grl #0:Msg inL => d(#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:UName, #2:Fresh)), (#0:Msg notLeq e(mkey(s, #3:UName), #4:Nonce ; #5:UName ; seskey(#3:UName, #5:UName, n(#6:UName, #7:Fresh)))), (#0:Msg notLeq #8:UName ; n(#8:UName, #9:Fresh)), (#0:Msg notLeq #10:UName ; seskey(#11:UName, #10:UName, n(#12:UName, #13:Fresh))), (#0:Msg notLeq #14:Nonce ; #15:UName), (#0:Msg notLeq #16:Nonce ; #17:UName ; n(#17:UName, #18:Fresh)), (#0:Msg notLeq e(#19:Sessionkey, #20:Nonce) ; n( #21:UName, #22:Fresh)), #0:Msg notLeq seskey(#23:UName, #24:UName, n(#25:UName, #26:Fresh)) => (#27: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 => e(#1:Key, #0:Msg) inL . ; grl #0:Msg inL => d(#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 => d(#0:Key, #1:Msg) inL .) | ( grl #0:Msg inL => e(#1:Key, #0:Msg) inL . ; grl #0:Msg inL => d(#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 => d(#1:Key, #0:Msg) inL .) | (errorNoHeuristicApplied { grl empty => d(#1:Key, #2:Msg) inL .,none, grl empty => (#2:Msg,#1:Key) inL .,none, grl empty => (#2:Msg,#1:Key) inL .} usingGrammar grl empty => d(#1:Key, #2:Msg) inL .) | ( grl #0:Msg inL => e(#1:Key, #0:Msg) inL . ; grl #0:Msg inL => d(#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 mkey(s, #1:UName) => (#0:Msg ; n(#2:UName, #3:Fresh) ; #4:UName) inL . ; grl #0:Key notInI, (#0:Key notLeq mkey(s, #1:UName)), #0:Key notLeq seskey(#2:UName, #3:UName, n(#4:UName, #5:Fresh)) => e(#0:Key, #6:Msg) inL .) | ( grl #0:Msg inL => e(#1:Key, #0:Msg) inL . ; grl #0:Msg inL => d(#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:Nonce ; #3:UName ; seskey(#4:UName, #3:UName, n(#5:UName, #6:Fresh))), (#0:Msg notLeq #7:Nonce ; #8:UName ; n(#8:UName, #9:Fresh)), (#0:Msg notLeq e(#10:Sessionkey, #11:Nonce) ; n(#12:UName, #13:Fresh)), (#0:Msg notLeq seskey(#14:UName, #15:UName, n(#16:UName, #17:Fresh)) ; #18:Nonce ; #14:UName), #0:Msg notLeq seskey(#19:UName, #20:UName, n(#21:UName, #22:Fresh)) => e(#23:Key, #0:Msg) inL . ;
