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 . ; 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)) => (#23:UName ; #0:Msg) inL .) | (errorNoHeuristicApplied { grl empty => e(#1:Key, #2:Msg) inL .,none, grl empty => (#2:Msg,#1:Key) inL .,none, grl empty => (#2:Msg,#1:Key) inL .} usingGrammar grl empty => e(#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 (mkey(#0:Name, #1:Name) notLeq mkey(i, s)), mkey(#0:Name, #1:Name) notLeq mkey(i, #2:UName) => mkey(#0:Name, #1:Name) inL .) | (errorInconsistentExceptionsInGrammarRule grl mr(#0:Name, #1:Fresh) notLeq #7:Nonce => mr(#0:Name, #1:Fresh) inL . inGrammar 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 mr(#0:Name, #1:Fresh) notLeq #7:Nonce => mr(#0:Name, #1:Fresh) inL .) | (errorInconsistentExceptionsInGrammarRule grl n(#0:Name, #1:Fresh) notLeq #7:Nonce => n(#0:Name, #1:Fresh) inL . inGrammar 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 n(#0:Name, #1:Fresh) notLeq #7:Nonce => n(#0:Name, #1:Fresh) 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 => p(#0:Msg) inL .) | (errorNoHeuristicApplied { grl empty => p(#1:Msg) inL .,none, grl empty => #1:Msg inL .,none, grl empty => #1:Msg inL .} usingGrammar grl empty => p(#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:Nonce notInI, #0:Nonce notLeq n(#1:UName, #2:Fresh) => seskey(#3:Name, #4:Name, #0:Nonce) 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 seskey(#0:Name, #1:Name, #2:Nonce) notLeq seskey(#3:UName, #4:UName, n(#5:UName, #6:Fresh)) => seskey(#0:Name, #1:Name, #2:Nonce) inL . ========================================== reduce in MAUDE-NPA : run(0) . rewrites: 3736 in 31ms cpu (35ms real) (120488 rewrites/second) result IdSystem: < 1 > :: r:Fresh,r1:Fresh :: [ nil, -(a ; NA:Nonce), +(a ; NA:Nonce ; b ; n(b, r:Fresh)), -(e(mkey(b, s), SK:Sessionkey ; n(b, r:Fresh) ; a) ; MA:Msg), +(MA:Msg ; e(SK:Sessionkey, NA:Nonce) ; n(b, r1:Fresh)), -(e(SK:Sessionkey, n(b, r1:Fresh))) | nil] || empty || nil || nil || nil ========================================== reduce in MAUDE-NPA : summary(1) . rewrites: 4756508 in 6291ms cpu (6304ms real) (756012 rewrites/second) result Summary: States>> 3 Solutions>> 0 ========================================== reduce in MAUDE-NPA : summary(2) . rewrites: 9642982 in 14194ms cpu (14229ms real) (679348 rewrites/second) result Summary: States>> 7 Solutions>> 0 ========================================== reduce in MAUDE-NPA : summary(3) . rewrites: 16333520 in 25396ms cpu (25480ms real) (643146 rewrites/second) result Summary: States>> 11 Solutions>> 0 ========================================== reduce in MAUDE-NPA : summary(4) . rewrites: 29338861 in 44465ms cpu (44611ms real) (659813 rewrites/second) result Summary: States>> 21 Solutions>> 0 ========================================== reduce in MAUDE-NPA : summary(5) . rewrites: 55564651 in 98705ms cpu (99218ms real) (562932 rewrites/second) result Summary: States>> 19 Solutions>> 1 ========================================== reduce in MAUDE-NPA : run(1) . rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second) result IdSystemSet: (< 1 . 1 > ( :: nil :: [ nil | -(#0:Sessionkey), -(n(b, #1:Fresh)), +(e(#0:Sessionkey, n(b, #1:Fresh))), nil] & :: #1:Fresh,#2:Fresh :: [ nil, -(a ; #3:Nonce), +(a ; #3:Nonce ; b ; n(b, #2:Fresh)), -(e(mkey(b, s), #0:Sessionkey ; n(b, #2:Fresh) ; a) ; #4:Msg), +(#4:Msg ; e(#0:Sessionkey, #3:Nonce) ; n(b, #1:Fresh)) | -(e(#0:Sessionkey, n(b, #1:Fresh))), nil] ) || e(#0:Sessionkey, n(b, #1:Fresh)) !inI, n(b, #1:Fresh) inI || -(#0:Sessionkey), -(n(b, #1:Fresh)), +(e(#0:Sessionkey, n(b, #1:Fresh))), -(e(#0:Sessionkey, n(b, #1:Fresh))) || ghost( #0:Sessionkey, :: nil :: [ nil | -(#0:Sessionkey), -(n(b, #1:Fresh)), +(e(#0:Sessionkey, n(b, #1:Fresh))), nil] & :: #1:Fresh,#2:Fresh :: [ nil, -(a ; #3:Nonce), +(a ; #3:Nonce ; b ; n(b, #2:Fresh)), -(e(mkey(b, s), #0:Sessionkey ; n(b, #2:Fresh) ; a) ; #4:Msg), +(#4:Msg ; e(#0:Sessionkey, #3:Nonce) ; n(b, #1:Fresh)) | -(e(#0:Sessionkey, n(b, #1:Fresh))), nil] , e(#0:Sessionkey, n(b, #1:Fresh)) !inI, n(b, #1:Fresh) inI, -(#0:Sessionkey), -(n(b, #1:Fresh)), +(e(#0:Sessionkey, n(b, #1:Fresh))), -(e(#0:Sessionkey, n(b, #1:Fresh))), nil ) || nil) (< 1 . 5 > ( :: nil :: [ nil | -(e(#0:Sessionkey, n(b, #1:Fresh)) ; #2:Msg), +(e(#0:Sessionkey, n(b, #1:Fresh))), nil] & :: #1:Fresh,#3:Fresh :: [ nil, -(a ; #4:Nonce), +(a ; #4:Nonce ; b ; n(b, #3:Fresh)), -(e(mkey(b, s), #0:Sessionkey ; n(b, #3:Fresh) ; a) ; #5:Msg), +(#5:Msg ; e(#0:Sessionkey, #4:Nonce) ; n(b, #1:Fresh)) | -(e(#0:Sessionkey, n(b, #1:Fresh))), nil] ) || e(#0:Sessionkey, n(b, #1:Fresh)) !inI, (e(#0:Sessionkey, n(b, #1:Fresh)) ; #2:Msg) inI || -(e(#0:Sessionkey, n(b, #1:Fresh)) ; #2:Msg), +(e(#0:Sessionkey, n(b, #1:Fresh))), -(e(#0:Sessionkey, n(b, #1:Fresh))) || nil || nil) < 1 . 6 > ( :: #0:Fresh :: [ nil, +(#1:UName ; n(#1:UName, #0:Fresh)) | -(e(mkey(s, #1:UName), n(#1:UName, #0:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#1:UName, #0:Fresh)) ; n(b, #4:Fresh)), +(e(#3:Sessionkey, n(b, #4:Fresh))), nil] & :: #4:Fresh,#5:Fresh :: [ nil, -(a ; #6:Nonce), +(a ; #6:Nonce ; b ; n(b, #5:Fresh)), -(e(mkey(b, s), #3:Sessionkey ; n(b, #5:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#3:Sessionkey, #6:Nonce) ; n(b, #4:Fresh)) | -(e(#3:Sessionkey, n(b, #4:Fresh))), nil] ) || e(#3:Sessionkey, n(b, #4:Fresh)) !inI, (e(mkey(s, #1:UName), n(#1:UName, #0:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#1:UName, #0:Fresh)) ; n(b, #4:Fresh)) inI || -(e(mkey(s, #1:UName), n(#1:UName, #0:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#1:UName, #0:Fresh)) ; n(b, #4:Fresh)), +(e(#3:Sessionkey, n(b, #4:Fresh))), -(e(#3:Sessionkey, n(b, #4:Fresh))) || nil || nil ========================================== reduce in MAUDE-NPA : run(2) . rewrites: 18 in 0ms cpu (0ms real) (18000000 rewrites/second) result IdSystemSet: (< 1 . 1 . 2 > ( :: nil :: [ nil | -(#4:Sessionkey), -(n(b, #0:Fresh)), +(e(#4:Sessionkey, n(b, #0:Fresh))), nil] & :: nil :: [ nil | -(n(b, #0:Fresh) ; #1:Msg), +(n(b, #0:Fresh)), nil] & :: #0:Fresh,#2:Fresh :: [ nil, -(a ; #3:Nonce), +(a ; #3:Nonce ; b ; n(b, #2:Fresh)), -(e(mkey(b, s), #4:Sessionkey ; n(b, #2:Fresh) ; a) ; #5:Msg), +(#5:Msg ; e(#4:Sessionkey, #3:Nonce) ; n(b, #0:Fresh)) | -(e(#4:Sessionkey, n(b, #0:Fresh))), nil] ) || n(b, #0:Fresh) !inI, e(#4:Sessionkey, n(b, #0:Fresh)) !inI, (n(b, #0:Fresh) ; #1:Msg) inI || -(n(b, #0:Fresh) ; #1:Msg), +(n(b, #0:Fresh)), -(#4:Sessionkey), -(n(b, #0:Fresh)), +(e(#4:Sessionkey, n(b, #0:Fresh))), -(e(#4:Sessionkey, n(b, #0:Fresh))) || ghost( #4:Sessionkey, :: nil :: [ nil | -(#4:Sessionkey), -(n(b, #0:Fresh)), +(e(#4:Sessionkey, n(b, #0:Fresh))), nil] & :: #0:Fresh,#2:Fresh :: [ nil, -(a ; #3:Nonce), +(a ; #3:Nonce ; b ; n(b, #2:Fresh)), -(e(mkey(b, s), #4:Sessionkey ; n(b, #2:Fresh) ; a) ; #5:Msg), +(#5:Msg ; e(#4:Sessionkey, #3:Nonce) ; n(b, #0:Fresh)) | -(e(#4:Sessionkey, n(b, #0:Fresh))), nil] , e(#4:Sessionkey, n(b, #0:Fresh)) !inI, n(b, #0:Fresh) inI, -(#4:Sessionkey), -(n(b, #0:Fresh)), +(e(#4:Sessionkey, n(b, #0:Fresh))), -(e(#4:Sessionkey, n(b, #0:Fresh))), nil ) || nil) (< 1 . 1 . 3 > ( :: nil :: [ nil | -(#4:Sessionkey), -(n(b, #1:Fresh)), +(e(#4:Sessionkey, n(b, #1:Fresh))), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, n(b, #1:Fresh))), +(n(b, #1:Fresh)), nil] & :: #1:Fresh,#2:Fresh :: [ nil, -(a ; #3:Nonce), +(a ; #3:Nonce ; b ; n(b, #2:Fresh)), -(e(mkey(b, s), #4:Sessionkey ; n(b, #2:Fresh) ; a) ; #5:Msg), +(#5:Msg ; e(#4:Sessionkey, #3:Nonce) ; n(b, #1:Fresh)) | -(e(#4:Sessionkey, n(b, #1:Fresh))), nil] ) || n(b, #1:Fresh) !inI, e(#4:Sessionkey, n(b, #1:Fresh)) !inI, e(#0:Key, n(b, #1:Fresh)) inI || -(#0:Key), -(e(#0:Key, n(b, #1:Fresh))), +(n(b, #1:Fresh)), -(#4:Sessionkey), -(n(b, #1:Fresh)), +(e(#4:Sessionkey, n(b, #1:Fresh))), -(e(#4:Sessionkey, n(b, #1:Fresh))) || ghost( #0:Key, :: nil :: [ nil | -(#4:Sessionkey), -(n(b, #1:Fresh)), +(e(#4:Sessionkey, n(b, #1:Fresh))), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, n(b, #1:Fresh))), +(n(b, #1:Fresh)), nil] & :: #1:Fresh,#2:Fresh :: [ nil, -(a ; #3:Nonce), +(a ; #3:Nonce ; b ; n(b, #2:Fresh)), -(e(mkey(b, s), #4:Sessionkey ; n(b, #2:Fresh) ; a) ; #5:Msg), +(#5:Msg ; e(#4:Sessionkey, #3:Nonce) ; n(b, #1:Fresh)) | -(e(#4:Sessionkey, n(b, #1:Fresh))), nil] , n(b, #1:Fresh) !inI, e(#4:Sessionkey, n(b, #1:Fresh)) !inI, e(#0:Key, n(b, #1:Fresh)) inI, -(#0:Key), -(e(#0:Key, n(b, #1:Fresh))), +(n(b, #1:Fresh)), -(#4:Sessionkey), -(n(b, #1:Fresh)), +(e(#4:Sessionkey, n(b, #1:Fresh))), -(e(#4:Sessionkey, n(b, #1:Fresh))), nil ), ghost( #4:Sessionkey, :: nil :: [ nil | -(#4:Sessionkey), -(n(b, #1:Fresh)), +(e(#4:Sessionkey, n(b, #1:Fresh))), nil] & :: #1:Fresh,#2:Fresh :: [ nil, -(a ; #3:Nonce), +(a ; #3:Nonce ; b ; n(b, #2:Fresh)), -(e(mkey(b, s), #4:Sessionkey ; n(b, #2:Fresh) ; a) ; #5:Msg), +(#5:Msg ; e(#4:Sessionkey, #3:Nonce) ; n(b, #1:Fresh)) | -(e(#4:Sessionkey, n(b, #1:Fresh))), nil] , e(#4:Sessionkey, n(b, #1:Fresh)) !inI, n(b, #1:Fresh) inI, -(#4:Sessionkey), -(n(b, #1:Fresh)), +(e(#4:Sessionkey, n(b, #1:Fresh))), -(e(#4:Sessionkey, n(b, #1:Fresh))), nil ) || nil) (< 1 . 1 . 5 > ( :: nil :: [ nil | -(#4:Sessionkey), -(n(b, #1:Fresh)), +(e(#4:Sessionkey, n(b, #1:Fresh))), nil] & :: nil :: [ nil | -(#0:Msg ; n(b, #1:Fresh)), +(n(b, #1:Fresh)), nil] & :: #1:Fresh,#2:Fresh :: [ nil, -(a ; #3:Nonce), +(a ; #3:Nonce ; b ; n(b, #2:Fresh)), -(e(mkey(b, s), #4:Sessionkey ; n(b, #2:Fresh) ; a) ; #5:Msg), +(#5:Msg ; e(#4:Sessionkey, #3:Nonce) ; n(b, #1:Fresh)) | -(e(#4:Sessionkey, n(b, #1:Fresh))), nil] ) || n(b, #1:Fresh) !inI, e(#4:Sessionkey, n(b, #1:Fresh)) !inI, (#0:Msg ; n(b, #1:Fresh)) inI || -(#0:Msg ; n(b, #1:Fresh)), +(n(b, #1:Fresh)), -(#4:Sessionkey), -(n(b, #1:Fresh)), +(e(#4:Sessionkey, n(b, #1:Fresh))), -(e(#4:Sessionkey, n(b, #1:Fresh))) || ghost( #4:Sessionkey, :: nil :: [ nil | -(#4:Sessionkey), -(n(b, #1:Fresh)), +(e(#4:Sessionkey, n(b, #1:Fresh))), nil] & :: #1:Fresh,#2:Fresh :: [ nil, -(a ; #3:Nonce), +(a ; #3:Nonce ; b ; n(b, #2:Fresh)), -(e(mkey(b, s), #4:Sessionkey ; n(b, #2:Fresh) ; a) ; #5:Msg), +(#5:Msg ; e(#4:Sessionkey, #3:Nonce) ; n(b, #1:Fresh)) | -(e(#4:Sessionkey, n(b, #1:Fresh))), nil] , e(#4:Sessionkey, n(b, #1:Fresh)) !inI, n(b, #1:Fresh) inI, -(#4:Sessionkey), -(n(b, #1:Fresh)), +(e(#4:Sessionkey, n(b, #1:Fresh))), -(e(#4:Sessionkey, n(b, #1:Fresh))), nil ) || nil) (< 1 . 5 . 4 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg)), +(e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg), nil] & :: nil :: [ nil | -(e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg), +(e(#1:Sessionkey, n(b, #2:Fresh))), nil] & :: #2:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #1:Sessionkey ; n(b, #4:Fresh) ; a) ; #6:Msg), +(#6:Msg ; e(#1:Sessionkey, #5:Nonce) ; n(b, #2:Fresh)) | -(e(#1:Sessionkey, n(b, #2:Fresh))), nil] ) || e(#1:Sessionkey, n(b, #2:Fresh)) !inI, (e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg) !inI, e(#0:Key, e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg) inI || -(#0:Key), -(e(#0:Key, e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg)), +(e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg), -(e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg), +(e(#1:Sessionkey, n(b, #2:Fresh))), -(e(#1:Sessionkey, n(b, #2:Fresh))) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg)), +(e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg), nil] & :: nil :: [ nil | -(e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg), +(e(#1:Sessionkey, n(b, #2:Fresh))), nil] & :: #2:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #1:Sessionkey ; n(b, #4:Fresh) ; a) ; #6:Msg), +(#6:Msg ; e(#1:Sessionkey, #5:Nonce) ; n(b, #2:Fresh)) | -(e(#1:Sessionkey, n(b, #2:Fresh))), nil] , e(#1:Sessionkey, n(b, #2:Fresh)) !inI, (e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg) !inI, e(#0:Key, e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg) inI, -(#0:Key), -(e(#0:Key, e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg)), +(e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg), -(e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg), +(e(#1:Sessionkey, n(b, #2:Fresh))), -(e(#1:Sessionkey, n(b, #2:Fresh))), nil ) || nil) (< 1 . 5 . 6 > ( :: nil :: [ nil | -(#0:Msg ; e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg), +(e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg), nil] & :: nil :: [ nil | -(e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg), +(e(#1:Sessionkey, n(b, #2:Fresh))), nil] & :: #2:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #1:Sessionkey ; n(b, #4:Fresh) ; a) ; #6:Msg), +(#6:Msg ; e(#1:Sessionkey, #5:Nonce) ; n(b, #2:Fresh)) | -(e(#1:Sessionkey, n(b, #2:Fresh))), nil] ) || e(#1:Sessionkey, n(b, #2:Fresh)) !inI, (e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg) !inI, (#0:Msg ; e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg) inI || -(#0:Msg ; e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg), +(e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg), -(e(#1:Sessionkey, n(b, #2:Fresh)) ; #3:Msg), +(e(#1:Sessionkey, n(b, #2:Fresh))), -(e(#1:Sessionkey, n(b, #2:Fresh))) || nil || nil) (< 1 . 5 . 7 > ( :: nil :: [ nil | -(e(#0:Sessionkey, n(b, #1:Fresh)) ; #2:Msg), +(e(#0:Sessionkey, n(b, #1:Fresh))), nil] & :: nil :: [ nil | -((e(#0:Sessionkey, n(b, #1:Fresh)) ; #2:Msg) ; #3:Msg), +(e(#0:Sessionkey, n(b, #1:Fresh)) ; #2:Msg), nil] & :: #1:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #0:Sessionkey ; n(b, #4:Fresh) ; a) ; #6:Msg), +(#6:Msg ; e(#0:Sessionkey, #5:Nonce) ; n(b, #1:Fresh)) | -(e(#0:Sessionkey, n(b, #1:Fresh))), nil] ) || e(#0:Sessionkey, n(b, #1:Fresh)) !inI, (e(#0:Sessionkey, n(b, #1:Fresh)) ; #2:Msg) !inI, ((e(#0:Sessionkey, n(b, #1:Fresh)) ; #2:Msg) ; #3:Msg) inI || -((e(#0:Sessionkey, n(b, #1:Fresh)) ; #2:Msg) ; #3:Msg), +(e(#0:Sessionkey, n(b, #1:Fresh)) ; #2:Msg), -(e(#0:Sessionkey, n(b, #1:Fresh)) ; #2:Msg), +(e(#0:Sessionkey, n(b, #1:Fresh))), -(e(#0:Sessionkey, n(b, #1:Fresh))) || nil || nil) < 1 . 6 . 3 > ( :: #0:Fresh :: [ nil, +(#1:UName ; n(#1:UName, #0:Fresh)) | -(e(mkey(s, #1:UName), n(#1:UName, #0:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#1:UName, #0:Fresh)) ; n(b, #4:Fresh)), +(e(#3:Sessionkey, n(b, #4:Fresh))), nil] & :: #4:Fresh,#5:Fresh :: [ nil, -(a ; n(#1:UName, #0:Fresh)), +(a ; n(#1:UName, #0:Fresh) ; b ; n(b, #5:Fresh)) | -(e(mkey(b, s), #3:Sessionkey ; n(b, #5:Fresh) ; a) ; e(mkey(s, #1:UName), n(#1:UName, #0:Fresh) ; #2:UName ; #3:Sessionkey)), +(e(mkey(s, #1:UName), n(#1:UName, #0:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#1:UName, #0:Fresh)) ; n(b, #4:Fresh)), -(e(#3:Sessionkey, n(b, #4:Fresh))), nil] ) || e(#3:Sessionkey, n(b, #4:Fresh)) !inI, (e(mkey(s, #1:UName), n(#1:UName, #0:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#1:UName, #0:Fresh)) ; n(b, #4:Fresh)) !inI, (e(mkey(b, s), #3:Sessionkey ; n(b, #5:Fresh) ; a) ; e(mkey(s, #1:UName), n(#1:UName, #0:Fresh) ; #2:UName ; #3:Sessionkey)) inI, inst(#1:UName), inst(#2:UName), inst(#3:Sessionkey) || -(e(mkey(b, s), #3:Sessionkey ; n(b, #5:Fresh) ; a) ; e(mkey(s, #1:UName), n(#1:UName, #0:Fresh) ; #2:UName ; #3:Sessionkey)), +(e(mkey(s, #1:UName), n(#1:UName, #0:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#1:UName, #0:Fresh)) ; n(b, #4:Fresh)), -(e(mkey(s, #1:UName), n(#1:UName, #0:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#1:UName, #0:Fresh)) ; n(b, #4:Fresh)), +(e(#3:Sessionkey, n(b, #4:Fresh))), -(e(#3:Sessionkey, n(b, #4:Fresh))) || nil || nil ========================================== reduce in MAUDE-NPA : run(3) . rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second) result IdSystemSet: (< 1 . 1 . 2 . 5 > ( :: nil :: [ nil | -(#5:Sessionkey), -(n(b, #0:Fresh)), +(e(#5:Sessionkey, n(b, #0:Fresh))), nil] & :: nil :: [ nil | -(n(b, #0:Fresh) ; #1:Msg), +(n(b, #0:Fresh)), nil] & :: nil :: [ nil | -((n(b, #0:Fresh) ; #1:Msg) ; #2:Msg), +(n(b, #0:Fresh) ; #1:Msg), nil] & :: #0:Fresh,#3:Fresh :: [ nil, -(a ; #4:Nonce), +(a ; #4:Nonce ; b ; n(b, #3:Fresh)), -(e(mkey(b, s), #5:Sessionkey ; n(b, #3:Fresh) ; a) ; #6:Msg), +(#6:Msg ; e(#5:Sessionkey, #4:Nonce) ; n(b, #0:Fresh)) | -(e(#5:Sessionkey, n(b, #0:Fresh))), nil] ) || n(b, #0:Fresh) !inI, e(#5:Sessionkey, n(b, #0:Fresh)) !inI, (n(b, #0:Fresh) ; #1:Msg) !inI, ((n(b, #0:Fresh) ; #1:Msg) ; #2:Msg) inI || -((n(b, #0:Fresh) ; #1:Msg) ; #2:Msg), +(n(b, #0:Fresh) ; #1:Msg), -(n(b, #0:Fresh) ; #1:Msg), +(n(b, #0:Fresh)), -(#5:Sessionkey), -(n(b, #0:Fresh)), +(e(#5:Sessionkey, n(b, #0:Fresh))), -(e(#5:Sessionkey, n(b, #0:Fresh))) || ghost( #5:Sessionkey, :: nil :: [ nil | -(#5:Sessionkey), -(n(b, #0:Fresh)), +(e(#5:Sessionkey, n(b, #0:Fresh))), nil] & :: #0:Fresh,#3:Fresh :: [ nil, -(a ; #4:Nonce), +(a ; #4:Nonce ; b ; n(b, #3:Fresh)), -(e(mkey(b, s), #5:Sessionkey ; n(b, #3:Fresh) ; a) ; #6:Msg), +(#6:Msg ; e(#5:Sessionkey, #4:Nonce) ; n(b, #0:Fresh)) | -(e(#5:Sessionkey, n(b, #0:Fresh))), nil] , e(#5:Sessionkey, n(b, #0:Fresh)) !inI, n(b, #0:Fresh) inI, -(#5:Sessionkey), -(n(b, #0:Fresh)), +(e(#5:Sessionkey, n(b, #0:Fresh))), -(e(#5:Sessionkey, n(b, #0:Fresh))), nil ) || nil) (< 1 . 1 . 2 . 6 > ( :: nil :: [ nil | -(#5:Sessionkey), -(n(b, #1:Fresh)), +(e(#5:Sessionkey, n(b, #1:Fresh))), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, 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,#3:Fresh :: [ nil, -(a ; #4:Nonce), +(a ; #4:Nonce ; b ; n(b, #3:Fresh)), -(e(mkey(b, s), #5:Sessionkey ; n(b, #3:Fresh) ; a) ; #6:Msg), +(#6:Msg ; e(#5:Sessionkey, #4:Nonce) ; n(b, #1:Fresh)) | -(e(#5:Sessionkey, n(b, #1:Fresh))), nil] ) || n(b, #1:Fresh) !inI, e(#5:Sessionkey, n(b, #1:Fresh)) !inI, (n(b, #1:Fresh) ; #2:Msg) !inI, e(#0:Key, n(b, #1:Fresh) ; #2:Msg) inI || -(#0:Key), -(e(#0:Key, n(b, #1:Fresh) ; #2:Msg)), +(n(b, #1:Fresh) ; #2:Msg), -(n(b, #1:Fresh) ; #2:Msg), +(n(b, #1:Fresh)), -(#5:Sessionkey), -(n(b, #1:Fresh)), +(e(#5:Sessionkey, n(b, #1:Fresh))), -(e(#5:Sessionkey, n(b, #1:Fresh))) || ghost( #0:Key, :: nil :: [ nil | -(#5:Sessionkey), -(n(b, #1:Fresh)), +(e(#5:Sessionkey, n(b, #1:Fresh))), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, 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,#3:Fresh :: [ nil, -(a ; #4:Nonce), +(a ; #4:Nonce ; b ; n(b, #3:Fresh)), -(e(mkey(b, s), #5:Sessionkey ; n(b, #3:Fresh) ; a) ; #6:Msg), +(#6:Msg ; e(#5:Sessionkey, #4:Nonce) ; n(b, #1:Fresh)) | -(e(#5:Sessionkey, n(b, #1:Fresh))), nil] , n(b, #1:Fresh) !inI, e(#5:Sessionkey, n(b, #1:Fresh)) !inI, (n(b, #1:Fresh) ; #2:Msg) !inI, e(#0:Key, n(b, #1:Fresh) ; #2:Msg) inI, -(#0:Key), -(e(#0:Key, n(b, #1:Fresh) ; #2:Msg)), +(n(b, #1:Fresh) ; #2:Msg), -(n(b, #1:Fresh) ; #2:Msg), +(n(b, #1:Fresh)), -(#5:Sessionkey), -(n(b, #1:Fresh)), +(e(#5:Sessionkey, n(b, #1:Fresh))), -(e(#5:Sessionkey, n(b, #1:Fresh))), nil ), ghost( #5:Sessionkey, :: nil :: [ nil | -(#5:Sessionkey), -(n(b, #1:Fresh)), +(e(#5:Sessionkey, n(b, #1:Fresh))), nil] & :: #1:Fresh,#3:Fresh :: [ nil, -(a ; #4:Nonce), +(a ; #4:Nonce ; b ; n(b, #3:Fresh)), -(e(mkey(b, s), #5:Sessionkey ; n(b, #3:Fresh) ; a) ; #6:Msg), +(#6:Msg ; e(#5:Sessionkey, #4:Nonce) ; n(b, #1:Fresh)) | -(e(#5:Sessionkey, n(b, #1:Fresh))), nil] , e(#5:Sessionkey, n(b, #1:Fresh)) !inI, n(b, #1:Fresh) inI, -(#5:Sessionkey), -(n(b, #1:Fresh)), +(e(#5:Sessionkey, n(b, #1:Fresh))), -(e(#5:Sessionkey, n(b, #1:Fresh))), nil ) || nil) (< 1 . 1 . 2 . 8 > ( :: nil :: [ nil | -(#5:Sessionkey), -(n(b, #1:Fresh)), +(e(#5:Sessionkey, 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,#3:Fresh :: [ nil, -(a ; #4:Nonce), +(a ; #4:Nonce ; b ; n(b, #3:Fresh)), -(e(mkey(b, s), #5:Sessionkey ; n(b, #3:Fresh) ; a) ; #6:Msg), +(#6:Msg ; e(#5:Sessionkey, #4:Nonce) ; n(b, #1:Fresh)) | -(e(#5:Sessionkey, n(b, #1:Fresh))), nil] ) || n(b, #1:Fresh) !inI, e(#5:Sessionkey, 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)), -(#5:Sessionkey), -(n(b, #1:Fresh)), +(e(#5:Sessionkey, n(b, #1:Fresh))), -(e(#5:Sessionkey, n(b, #1:Fresh))) || ghost( #5:Sessionkey, :: nil :: [ nil | -(#5:Sessionkey), -(n(b, #1:Fresh)), +(e(#5:Sessionkey, n(b, #1:Fresh))), nil] & :: #1:Fresh,#3:Fresh :: [ nil, -(a ; #4:Nonce), +(a ; #4:Nonce ; b ; n(b, #3:Fresh)), -(e(mkey(b, s), #5:Sessionkey ; n(b, #3:Fresh) ; a) ; #6:Msg), +(#6:Msg ; e(#5:Sessionkey, #4:Nonce) ; n(b, #1:Fresh)) | -(e(#5:Sessionkey, n(b, #1:Fresh))), nil] , e(#5:Sessionkey, n(b, #1:Fresh)) !inI, n(b, #1:Fresh) inI, -(#5:Sessionkey), -(n(b, #1:Fresh)), +(e(#5:Sessionkey, n(b, #1:Fresh))), -(e(#5:Sessionkey, n(b, #1:Fresh))), nil ) || nil) (< 1 . 1 . 3 . 4 > ( :: nil :: [ nil | -(#5:Sessionkey), -(n(b, #1:Fresh)), +(e(#5:Sessionkey, n(b, #1:Fresh))), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, n(b, #1:Fresh))), +(n(b, #1:Fresh)), nil] & :: nil :: [ nil | -(e(#0:Key, n(b, #1:Fresh)) ; #2:Msg), +(e(#0:Key, n(b, #1:Fresh))), nil] & :: #1:Fresh,#3:Fresh :: [ nil, -(a ; #4:Nonce), +(a ; #4:Nonce ; b ; n(b, #3:Fresh)), -(e(mkey(b, s), #5:Sessionkey ; n(b, #3:Fresh) ; a) ; #6:Msg), +(#6:Msg ; e(#5:Sessionkey, #4:Nonce) ; n(b, #1:Fresh)) | -(e(#5:Sessionkey, n(b, #1:Fresh))), nil] ) || n(b, #1:Fresh) !inI, e(#5:Sessionkey, n(b, #1:Fresh)) !inI, e(#0:Key, n(b, #1:Fresh)) !inI, (e(#0:Key, n(b, #1:Fresh)) ; #2:Msg) inI || -(e(#0:Key, n(b, #1:Fresh)) ; #2:Msg), +(e(#0:Key, n(b, #1:Fresh))), -(#0:Key), -(e(#0:Key, n(b, #1:Fresh))), +(n(b, #1:Fresh)), -(#5:Sessionkey), -(n(b, #1:Fresh)), +(e(#5:Sessionkey, n(b, #1:Fresh))), -(e(#5:Sessionkey, n(b, #1:Fresh))) || ghost( #0:Key, :: nil :: [ nil | -(#5:Sessionkey), -(n(b, #1:Fresh)), +(e(#5:Sessionkey, n(b, #1:Fresh))), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, n(b, #1:Fresh))), +(n(b, #1:Fresh)), nil] & :: #1:Fresh,#3:Fresh :: [ nil, -(a ; #4:Nonce), +(a ; #4:Nonce ; b ; n(b, #3:Fresh)), -(e(mkey(b, s), #5:Sessionkey ; n(b, #3:Fresh) ; a) ; #6:Msg), +(#6:Msg ; e(#5:Sessionkey, #4:Nonce) ; n(b, #1:Fresh)) | -(e(#5:Sessionkey, n(b, #1:Fresh))), nil] , n(b, #1:Fresh) !inI, e(#5:Sessionkey, n(b, #1:Fresh)) !inI, e(#0:Key, n(b, #1:Fresh)) inI, -(#0:Key), -(e(#0:Key, n(b, #1:Fresh))), +(n(b, #1:Fresh)), -(#5:Sessionkey), -(n(b, #1:Fresh)), +(e(#5:Sessionkey, n(b, #1:Fresh))), -(e(#5:Sessionkey, n(b, #1:Fresh))), nil ), ghost( #5:Sessionkey, :: nil :: [ nil | -(#5:Sessionkey), -(n(b, #1:Fresh)), +(e(#5:Sessionkey, n(b, #1:Fresh))), nil] & :: #1:Fresh,#3:Fresh :: [ nil, -(a ; #4:Nonce), +(a ; #4:Nonce ; b ; n(b, #3:Fresh)), -(e(mkey(b, s), #5:Sessionkey ; n(b, #3:Fresh) ; a) ; #6:Msg), +(#6:Msg ; e(#5:Sessionkey, #4:Nonce) ; n(b, #1:Fresh)) | -(e(#5:Sessionkey, n(b, #1:Fresh))), nil] , e(#5:Sessionkey, n(b, #1:Fresh)) !inI, n(b, #1:Fresh) inI, -(#5:Sessionkey), -(n(b, #1:Fresh)), +(e(#5:Sessionkey, n(b, #1:Fresh))), -(e(#5:Sessionkey, n(b, #1:Fresh))), nil ) || nil) (< 1 . 1 . 5 . 4 > ( :: nil :: [ nil | -(#5:Sessionkey), -(n(b, #1:Fresh)), +(e(#5:Sessionkey, n(b, #1:Fresh))), nil] & :: nil :: [ nil | -(#0:Msg ; n(b, #1:Fresh)), +(n(b, #1:Fresh)), nil] & :: nil :: [ nil | -((#0:Msg ; n(b, #1:Fresh)) ; #2:Msg), +(#0:Msg ; n(b, #1:Fresh)), nil] & :: #1:Fresh,#3:Fresh :: [ nil, -(a ; #4:Nonce), +(a ; #4:Nonce ; b ; n(b, #3:Fresh)), -(e(mkey(b, s), #5:Sessionkey ; n(b, #3:Fresh) ; a) ; #6:Msg), +(#6:Msg ; e(#5:Sessionkey, #4:Nonce) ; n(b, #1:Fresh)) | -(e(#5:Sessionkey, n(b, #1:Fresh))), nil] ) || n(b, #1:Fresh) !inI, e(#5:Sessionkey, n(b, #1:Fresh)) !inI, (#0:Msg ; n(b, #1:Fresh)) !inI, ((#0:Msg ; n(b, #1:Fresh)) ; #2:Msg) inI || -((#0:Msg ; n(b, #1:Fresh)) ; #2:Msg), +(#0:Msg ; n(b, #1:Fresh)), -(#0:Msg ; n(b, #1:Fresh)), +(n(b, #1:Fresh)), -(#5:Sessionkey), -(n(b, #1:Fresh)), +(e(#5:Sessionkey, n(b, #1:Fresh))), -(e(#5:Sessionkey, n(b, #1:Fresh))) || ghost( #5:Sessionkey, :: nil :: [ nil | -(#5:Sessionkey), -(n(b, #1:Fresh)), +(e(#5:Sessionkey, n(b, #1:Fresh))), nil] & :: #1:Fresh,#3:Fresh :: [ nil, -(a ; #4:Nonce), +(a ; #4:Nonce ; b ; n(b, #3:Fresh)), -(e(mkey(b, s), #5:Sessionkey ; n(b, #3:Fresh) ; a) ; #6:Msg), +(#6:Msg ; e(#5:Sessionkey, #4:Nonce) ; n(b, #1:Fresh)) | -(e(#5:Sessionkey, n(b, #1:Fresh))), nil] , e(#5:Sessionkey, n(b, #1:Fresh)) !inI, n(b, #1:Fresh) inI, -(#5:Sessionkey), -(n(b, #1:Fresh)), +(e(#5:Sessionkey, n(b, #1:Fresh))), -(e(#5:Sessionkey, n(b, #1:Fresh))), nil ) || nil) (< 1 . 1 . 5 . 5 > ( :: nil :: [ nil | -(#5:Sessionkey), -(n(b, #2:Fresh)), +(e(#5:Sessionkey, n(b, #2:Fresh))), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, #1:Msg ; n(b, #2:Fresh))), +(#1:Msg ; n(b, #2:Fresh)), nil] & :: nil :: [ nil | -(#1:Msg ; n(b, #2:Fresh)), +(n(b, #2:Fresh)), nil] & :: #2:Fresh,#3:Fresh :: [ nil, -(a ; #4:Nonce), +(a ; #4:Nonce ; b ; n(b, #3:Fresh)), -(e(mkey(b, s), #5:Sessionkey ; n(b, #3:Fresh) ; a) ; #6:Msg), +(#6:Msg ; e(#5:Sessionkey, #4:Nonce) ; n(b, #2:Fresh)) | -(e(#5:Sessionkey, n(b, #2:Fresh))), nil] ) || n(b, #2:Fresh) !inI, e(#5:Sessionkey, n(b, #2:Fresh)) !inI, (#1:Msg ; n(b, #2:Fresh)) !inI, e(#0:Key, #1:Msg ; n(b, #2:Fresh)) inI || -(#0:Key), -(e(#0:Key, #1:Msg ; n(b, #2:Fresh))), +(#1:Msg ; n(b, #2:Fresh)), -(#1:Msg ; n(b, #2:Fresh)), +(n(b, #2:Fresh)), -(#5:Sessionkey), -(n(b, #2:Fresh)), +(e(#5:Sessionkey, n(b, #2:Fresh))), -(e(#5:Sessionkey, n(b, #2:Fresh))) || ghost( #0:Key, :: nil :: [ nil | -(#5:Sessionkey), -(n(b, #2:Fresh)), +(e(#5:Sessionkey, n(b, #2:Fresh))), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, #1:Msg ; n(b, #2:Fresh))), +(#1:Msg ; n(b, #2:Fresh)), nil] & :: nil :: [ nil | -(#1:Msg ; n(b, #2:Fresh)), +(n(b, #2:Fresh)), nil] & :: #2:Fresh,#3:Fresh :: [ nil, -(a ; #4:Nonce), +(a ; #4:Nonce ; b ; n(b, #3:Fresh)), -(e(mkey(b, s), #5:Sessionkey ; n(b, #3:Fresh) ; a) ; #6:Msg), +(#6:Msg ; e(#5:Sessionkey, #4:Nonce) ; n(b, #2:Fresh)) | -(e(#5:Sessionkey, n(b, #2:Fresh))), nil] , n(b, #2:Fresh) !inI, e(#5:Sessionkey, n(b, #2:Fresh)) !inI, (#1:Msg ; n(b, #2:Fresh)) !inI, e(#0:Key, #1:Msg ; n(b, #2:Fresh)) inI, -(#0:Key), -(e(#0:Key, #1:Msg ; n(b, #2:Fresh))), +(#1:Msg ; n(b, #2:Fresh)), -(#1:Msg ; n(b, #2:Fresh)), +(n(b, #2:Fresh)), -(#5:Sessionkey), -(n(b, #2:Fresh)), +(e(#5:Sessionkey, n(b, #2:Fresh))), -(e(#5:Sessionkey, n(b, #2:Fresh))), nil ), ghost( #5:Sessionkey, :: nil :: [ nil | -(#5:Sessionkey), -(n(b, #2:Fresh)), +(e(#5:Sessionkey, n(b, #2:Fresh))), nil] & :: #2:Fresh,#3:Fresh :: [ nil, -(a ; #4:Nonce), +(a ; #4:Nonce ; b ; n(b, #3:Fresh)), -(e(mkey(b, s), #5:Sessionkey ; n(b, #3:Fresh) ; a) ; #6:Msg), +(#6:Msg ; e(#5:Sessionkey, #4:Nonce) ; n(b, #2:Fresh)) | -(e(#5:Sessionkey, n(b, #2:Fresh))), nil] , e(#5:Sessionkey, n(b, #2:Fresh)) !inI, n(b, #2:Fresh) inI, -(#5:Sessionkey), -(n(b, #2:Fresh)), +(e(#5:Sessionkey, n(b, #2:Fresh))), -(e(#5:Sessionkey, n(b, #2:Fresh))), nil ) || nil) (< 1 . 1 . 5 . 7 > ( :: nil :: [ nil | -(#5:Sessionkey), -(n(b, #2:Fresh)), +(e(#5:Sessionkey, n(b, #2:Fresh))), nil] & :: nil :: [ nil | -(#0:Msg ; #1:Msg ; n(b, #2:Fresh)), +(#1:Msg ; n(b, #2:Fresh)), nil] & :: nil :: [ nil | -(#1:Msg ; n(b, #2:Fresh)), +(n(b, #2:Fresh)), nil] & :: #2:Fresh,#3:Fresh :: [ nil, -(a ; #4:Nonce), +(a ; #4:Nonce ; b ; n(b, #3:Fresh)), -(e(mkey(b, s), #5:Sessionkey ; n(b, #3:Fresh) ; a) ; #6:Msg), +(#6:Msg ; e(#5:Sessionkey, #4:Nonce) ; n(b, #2:Fresh)) | -(e(#5:Sessionkey, n(b, #2:Fresh))), nil] ) || n(b, #2:Fresh) !inI, e(#5:Sessionkey, n(b, #2:Fresh)) !inI, (#1:Msg ; n(b, #2:Fresh)) !inI, (#0:Msg ; #1:Msg ; n(b, #2:Fresh)) inI || -(#0:Msg ; #1:Msg ; n(b, #2:Fresh)), +(#1:Msg ; n(b, #2:Fresh)), -(#1:Msg ; n(b, #2:Fresh)), +(n(b, #2:Fresh)), -(#5:Sessionkey), -(n(b, #2:Fresh)), +(e(#5:Sessionkey, n(b, #2:Fresh))), -(e(#5:Sessionkey, n(b, #2:Fresh))) || ghost( #5:Sessionkey, :: nil :: [ nil | -(#5:Sessionkey), -(n(b, #2:Fresh)), +(e(#5:Sessionkey, n(b, #2:Fresh))), nil] & :: #2:Fresh,#3:Fresh :: [ nil, -(a ; #4:Nonce), +(a ; #4:Nonce ; b ; n(b, #3:Fresh)), -(e(mkey(b, s), #5:Sessionkey ; n(b, #3:Fresh) ; a) ; #6:Msg), +(#6:Msg ; e(#5:Sessionkey, #4:Nonce) ; n(b, #2:Fresh)) | -(e(#5:Sessionkey, n(b, #2:Fresh))), nil] , e(#5:Sessionkey, n(b, #2:Fresh)) !inI, n(b, #2:Fresh) inI, -(#5:Sessionkey), -(n(b, #2:Fresh)), +(e(#5:Sessionkey, n(b, #2:Fresh))), -(e(#5:Sessionkey, n(b, #2:Fresh))), nil ) || nil) (< 1 . 5 . 6 . 1 > ( :: nil :: [ nil | -(#3:Msg ; e(#2:Sessionkey, n(b, #0:Fresh)) ; n(b, #0:Fresh)), +(e(#2:Sessionkey, n(b, #0:Fresh)) ; n(b, #0:Fresh)), nil] & :: nil :: [ nil | -(e(#2:Sessionkey, n(b, #0:Fresh)) ; n(b, #0:Fresh)), +(e(#2:Sessionkey, n(b, #0:Fresh))), nil] & :: #0:Fresh,#1:Fresh :: [ nil, -(a ; n(b, #0:Fresh)), +(a ; n(b, #0:Fresh) ; b ; n(b, #1:Fresh)) | -(e(mkey(b, s), #2:Sessionkey ; n(b, #1:Fresh) ; a) ; #3:Msg), +(#3:Msg ; e(#2:Sessionkey, n(b, #0:Fresh)) ; n(b, #0:Fresh)), -(e(#2:Sessionkey, n(b, #0:Fresh))), nil] ) || e(#2:Sessionkey, n(b, #0:Fresh)) !inI, (#3:Msg ; e(#2:Sessionkey, n(b, #0:Fresh)) ; n(b, #0:Fresh)) !inI, (e(#2:Sessionkey, n(b, #0:Fresh)) ; n(b, #0:Fresh)) !inI, (e(mkey(b, s), #2:Sessionkey ; n(b, #1:Fresh) ; a) ; #3:Msg) inI || -(e(mkey(b, s), #2:Sessionkey ; n(b, #1:Fresh) ; a) ; #3:Msg), +(#3:Msg ; e(#2:Sessionkey, n(b, #0:Fresh)) ; n(b, #0:Fresh)), -(#3:Msg ; e(#2:Sessionkey, n(b, #0:Fresh)) ; n(b, #0:Fresh)), +(e(#2:Sessionkey, n(b, #0:Fresh)) ; n(b, #0:Fresh)), -(e(#2:Sessionkey, n(b, #0:Fresh)) ; n(b, #0:Fresh)), +(e(#2:Sessionkey, n(b, #0:Fresh))), -(e(#2:Sessionkey, n(b, #0:Fresh))) || nil || nil) (< 1 . 5 . 6 . 8 > ( :: nil :: [ nil | -(#9:Msg ; e(#3:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), nil] & :: nil :: [ nil | -(e(#3:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh))), nil] & :: #0:Fresh,#1:Fresh :: [ nil, -(a ; #2:Nonce), +(a ; #2:Nonce ; b ; n(b, #1:Fresh)), -(e(mkey(b, s), #3:Sessionkey ; n(b, #1:Fresh) ; a) ; #4:Msg), +(#4:Msg ; e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)) | -(e(#3:Sessionkey, n(b, #0:Fresh))), nil] & :: #5:Fresh,#6:Fresh :: [ nil, -(#7:UName ; n(b, #0:Fresh)), +(#7:UName ; n(b, #0:Fresh) ; #8:UName ; n(#8:UName, #6:Fresh)) | -(e(mkey(s, #8:UName), #3:Sessionkey ; n(#8:UName, #6:Fresh) ; #7:UName) ; #9:Msg), +(#9:Msg ; e(#3:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), nil] ) || e(#3:Sessionkey, n(b, #0:Fresh)) !inI, (#9:Msg ; e(#3:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)) !inI, (e(#3:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)) !inI, (e(mkey(s, #8:UName), #3:Sessionkey ; n(#8:UName, #6:Fresh) ; #7:UName) ; #9:Msg) inI || -(e(mkey(s, #8:UName), #3:Sessionkey ; n(#8:UName, #6:Fresh) ; #7:UName) ; #9:Msg), +(#9:Msg ; e(#3:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), -(#9:Msg ; e(#3:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), -(e(#3:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh))), -(e(#3:Sessionkey, n(b, #0:Fresh))) || nil || nil) (< 1 . 6 . 3 . 5 > ( :: nil :: [ nil | -(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), -(e(mkey(b, s), #3:Sessionkey ; n(b, #4:Fresh) ; a)), +(e(mkey(b, s), #3:Sessionkey ; n(b, #4:Fresh) ; a) ; e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), nil] & :: #1:Fresh :: [ nil, +(#0:UName ; n(#0:UName, #1:Fresh)) | -(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#0:UName, #1:Fresh)) ; n(b, #5:Fresh)), +(e(#3:Sessionkey, n(b, #5:Fresh))), nil] & :: #4:Fresh,#5:Fresh :: [ nil, -(a ; n(#0:UName, #1:Fresh)), +(a ; n(#0:UName, #1:Fresh) ; b ; n(b, #4:Fresh)) | -(e(mkey(b, s), #3:Sessionkey ; n(b, #4:Fresh) ; a) ; e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), +(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#0:UName, #1:Fresh)) ; n(b, #5:Fresh)), -(e(#3:Sessionkey, n(b, #5:Fresh))), nil] ) || e(#3:Sessionkey, n(b, #5:Fresh)) !inI, (e(mkey(b, s), #3:Sessionkey ; n(b, #4:Fresh) ; a) ; e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)) !inI, (e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#0:UName, #1:Fresh)) ; n(b, #5:Fresh)) !inI, e(mkey(b, s), #3:Sessionkey ; n(b, #4:Fresh) ; a) inI, e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) inI, inst(#0:UName), inst(#2:UName), inst(#3:Sessionkey) || -(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), -(e(mkey(b, s), #3:Sessionkey ; n(b, #4:Fresh) ; a)), +(e(mkey(b, s), #3:Sessionkey ; n(b, #4:Fresh) ; a) ; e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), -(e(mkey(b, s), #3:Sessionkey ; n(b, #4:Fresh) ; a) ; e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), +(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#0:UName, #1:Fresh)) ; n(b, #5:Fresh)), -(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#0:UName, #1:Fresh)) ; n(b, #5:Fresh)), +(e(#3:Sessionkey, n(b, #5:Fresh))), -(e(#3:Sessionkey, n(b, #5:Fresh))) || nil || nil) < 1 . 6 . 3 . 8 > ( :: #0:Fresh :: [ nil, +(a ; n(a, #0:Fresh)) | -(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)), +(e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh))), nil] & :: #2:Fresh :: [ nil | -(a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))), nil] & :: #3:Fresh,#4:Fresh :: [ nil, -(a ; n(a, #0:Fresh)), +(a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)) | -(e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))), +(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)), -(e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh))), nil] ) || e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh)) !inI, (e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)) !inI, (e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))) !inI, (a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)) inI, inst(#1:UName) || -(a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))), -(e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))), +(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)), -(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)), +(e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh))), -(e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh))) || nil || nil ========================================== reduce in MAUDE-NPA : run(4) . rewrites: 18 in 0ms cpu (0ms real) (18000000 rewrites/second) result IdSystemSet: (< 1 . 1 . 2 . 6 . 3 > ( :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #1:Fresh)), +(e(#6:Sessionkey, n(b, #1:Fresh))), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, 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] & :: nil :: [ nil | -(e(#0:Key, n(b, #1:Fresh) ; #2:Msg) ; #3:Msg), +(e(#0:Key, n(b, #1:Fresh) ; #2:Msg)), nil] & :: #1:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #1:Fresh)) | -(e(#6:Sessionkey, n(b, #1:Fresh))), nil] ) || n(b, #1:Fresh) !inI, e(#6:Sessionkey, n(b, #1:Fresh)) !inI, e(#0:Key, n(b, #1:Fresh) ; #2:Msg) !inI, (n(b, #1:Fresh) ; #2:Msg) !inI, (e(#0:Key, n(b, #1:Fresh) ; #2:Msg) ; #3:Msg) inI || -(e(#0:Key, n(b, #1:Fresh) ; #2:Msg) ; #3:Msg), +(e(#0:Key, n(b, #1:Fresh) ; #2:Msg)), -(#0:Key), -(e(#0:Key, n(b, #1:Fresh) ; #2:Msg)), +(n(b, #1:Fresh) ; #2:Msg), -(n(b, #1:Fresh) ; #2:Msg), +(n(b, #1:Fresh)), -(#6:Sessionkey), -(n(b, #1:Fresh)), +(e(#6:Sessionkey, n(b, #1:Fresh))), -(e(#6:Sessionkey, n(b, #1:Fresh))) || ghost( #0:Key, :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #1:Fresh)), +(e(#6:Sessionkey, n(b, #1:Fresh))), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, 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,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #1:Fresh)) | -(e(#6:Sessionkey, n(b, #1:Fresh))), nil] , n(b, #1:Fresh) !inI, e(#6:Sessionkey, n(b, #1:Fresh)) !inI, (n(b, #1:Fresh) ; #2:Msg) !inI, e(#0:Key, n(b, #1:Fresh) ; #2:Msg) inI, -(#0:Key), -(e(#0:Key, n(b, #1:Fresh) ; #2:Msg)), +(n(b, #1:Fresh) ; #2:Msg), -(n(b, #1:Fresh) ; #2:Msg), +(n(b, #1:Fresh)), -(#6:Sessionkey), -(n(b, #1:Fresh)), +(e(#6:Sessionkey, n(b, #1:Fresh))), -(e(#6:Sessionkey, n(b, #1:Fresh))), nil ), ghost( #6:Sessionkey, :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #1:Fresh)), +(e(#6:Sessionkey, n(b, #1:Fresh))), nil] & :: #1:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #1:Fresh)) | -(e(#6:Sessionkey, n(b, #1:Fresh))), nil] , e(#6:Sessionkey, n(b, #1:Fresh)) !inI, n(b, #1:Fresh) inI, -(#6:Sessionkey), -(n(b, #1:Fresh)), +(e(#6:Sessionkey, n(b, #1:Fresh))), -(e(#6:Sessionkey, n(b, #1:Fresh))), nil ) || nil) (< 1 . 1 . 2 . 6 . 6 > ( :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, n(b, #2:Fresh) ; #3:Msg)), +(n(b, #2:Fresh) ; #3:Msg), nil] & :: nil :: [ nil | -(#0:Msg ; e(#1:Key, n(b, #2:Fresh) ; #3:Msg)), +(e(#1:Key, n(b, #2:Fresh) ; #3:Msg)), nil] & :: nil :: [ nil | -(n(b, #2:Fresh) ; #3:Msg), +(n(b, #2:Fresh)), nil] & :: #2:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #2:Fresh)) | -(e(#6:Sessionkey, n(b, #2:Fresh))), nil] ) || n(b, #2:Fresh) !inI, e(#6:Sessionkey, n(b, #2:Fresh)) !inI, e(#1:Key, n(b, #2:Fresh) ; #3:Msg) !inI, (n(b, #2:Fresh) ; #3:Msg) !inI, (#0:Msg ; e(#1:Key, n(b, #2:Fresh) ; #3:Msg)) inI || -(#0:Msg ; e(#1:Key, n(b, #2:Fresh) ; #3:Msg)), +(e(#1:Key, n(b, #2:Fresh) ; #3:Msg)), -(#1:Key), -(e(#1:Key, n(b, #2:Fresh) ; #3:Msg)), +(n(b, #2:Fresh) ; #3:Msg), -(n(b, #2:Fresh) ; #3:Msg), +(n(b, #2:Fresh)), -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), -(e(#6:Sessionkey, n(b, #2:Fresh))) || ghost( #1:Key, :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, n(b, #2:Fresh) ; #3:Msg)), +(n(b, #2:Fresh) ; #3:Msg), nil] & :: nil :: [ nil | -(n(b, #2:Fresh) ; #3:Msg), +(n(b, #2:Fresh)), nil] & :: #2:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #2:Fresh)) | -(e(#6:Sessionkey, n(b, #2:Fresh))), nil] , n(b, #2:Fresh) !inI, e(#6:Sessionkey, n(b, #2:Fresh)) !inI, (n(b, #2:Fresh) ; #3:Msg) !inI, e(#1:Key, n(b, #2:Fresh) ; #3:Msg) inI, -(#1:Key), -(e(#1:Key, n(b, #2:Fresh) ; #3:Msg)), +(n(b, #2:Fresh) ; #3:Msg), -(n(b, #2:Fresh) ; #3:Msg), +(n(b, #2:Fresh)), -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), -(e(#6:Sessionkey, n(b, #2:Fresh))), nil ), ghost( #6:Sessionkey, :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), nil] & :: #2:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #2:Fresh)) | -(e(#6:Sessionkey, n(b, #2:Fresh))), nil] , e(#6:Sessionkey, n(b, #2:Fresh)) !inI, n(b, #2:Fresh) inI, -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), -(e(#6:Sessionkey, n(b, #2:Fresh))), nil ) || nil) (< 1 . 1 . 2 . 8 . 5 > ( :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, #1:Msg ; n(b, #2:Fresh) ; #3:Msg)), +(#1:Msg ; n(b, #2:Fresh) ; #3:Msg), nil] & :: nil :: [ nil | -(#1:Msg ; n(b, #2:Fresh) ; #3:Msg), +(n(b, #2:Fresh) ; #3:Msg), nil] & :: nil :: [ nil | -(n(b, #2:Fresh) ; #3:Msg), +(n(b, #2:Fresh)), nil] & :: #2:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #2:Fresh)) | -(e(#6:Sessionkey, n(b, #2:Fresh))), nil] ) || n(b, #2:Fresh) !inI, e(#6:Sessionkey, n(b, #2:Fresh)) !inI, (#1:Msg ; n(b, #2:Fresh) ; #3:Msg) !inI, (n(b, #2:Fresh) ; #3:Msg) !inI, e(#0:Key, #1:Msg ; n(b, #2:Fresh) ; #3:Msg) inI || -(#0:Key), -(e(#0:Key, #1:Msg ; n(b, #2:Fresh) ; #3:Msg)), +(#1:Msg ; n(b, #2:Fresh) ; #3:Msg), -(#1:Msg ; n(b, #2:Fresh) ; #3:Msg), +(n(b, #2:Fresh) ; #3:Msg), -(n(b, #2:Fresh) ; #3:Msg), +(n(b, #2:Fresh)), -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), -(e(#6:Sessionkey, n(b, #2:Fresh))) || ghost( #0:Key, :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, #1:Msg ; n(b, #2:Fresh) ; #3:Msg)), +(#1:Msg ; n(b, #2:Fresh) ; #3:Msg), nil] & :: nil :: [ nil | -(#1:Msg ; n(b, #2:Fresh) ; #3:Msg), +(n(b, #2:Fresh) ; #3:Msg), nil] & :: nil :: [ nil | -(n(b, #2:Fresh) ; #3:Msg), +(n(b, #2:Fresh)), nil] & :: #2:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #2:Fresh)) | -(e(#6:Sessionkey, n(b, #2:Fresh))), nil] , n(b, #2:Fresh) !inI, e(#6:Sessionkey, n(b, #2:Fresh)) !inI, (#1:Msg ; n(b, #2:Fresh) ; #3:Msg) !inI, (n(b, #2:Fresh) ; #3:Msg) !inI, e(#0:Key, #1:Msg ; n(b, #2:Fresh) ; #3:Msg) inI, -(#0:Key), -(e(#0:Key, #1:Msg ; n(b, #2:Fresh) ; #3:Msg)), +(#1:Msg ; n(b, #2:Fresh) ; #3:Msg), -(#1:Msg ; n(b, #2:Fresh) ; #3:Msg), +(n(b, #2:Fresh) ; #3:Msg), -(n(b, #2:Fresh) ; #3:Msg), +(n(b, #2:Fresh)), -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), -(e(#6:Sessionkey, n(b, #2:Fresh))), nil ), ghost( #6:Sessionkey, :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), nil] & :: #2:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #2:Fresh)) | -(e(#6:Sessionkey, n(b, #2:Fresh))), nil] , e(#6:Sessionkey, n(b, #2:Fresh)) !inI, n(b, #2:Fresh) inI, -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), -(e(#6:Sessionkey, n(b, #2:Fresh))), nil ) || nil) (< 1 . 1 . 3 . 4 . 5 > ( :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #1:Fresh)), +(e(#6:Sessionkey, n(b, #1:Fresh))), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, n(b, #1:Fresh))), +(n(b, #1:Fresh)), nil] & :: nil :: [ nil | -(e(#0:Key, n(b, #1:Fresh)) ; #2:Msg), +(e(#0:Key, n(b, #1:Fresh))), nil] & :: nil :: [ nil | -((e(#0:Key, n(b, #1:Fresh)) ; #2:Msg) ; #3:Msg), +(e(#0:Key, n(b, #1:Fresh)) ; #2:Msg), nil] & :: #1:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #1:Fresh)) | -(e(#6:Sessionkey, n(b, #1:Fresh))), nil] ) || n(b, #1:Fresh) !inI, e(#6:Sessionkey, n(b, #1:Fresh)) !inI, e(#0:Key, n(b, #1:Fresh)) !inI, (e(#0:Key, n(b, #1:Fresh)) ; #2:Msg) !inI, ((e(#0:Key, n(b, #1:Fresh)) ; #2:Msg) ; #3:Msg) inI || -((e(#0:Key, n(b, #1:Fresh)) ; #2:Msg) ; #3:Msg), +(e(#0:Key, n(b, #1:Fresh)) ; #2:Msg), -(e(#0:Key, n(b, #1:Fresh)) ; #2:Msg), +(e(#0:Key, n(b, #1:Fresh))), -(#0:Key), -(e(#0:Key, n(b, #1:Fresh))), +(n(b, #1:Fresh)), -(#6:Sessionkey), -(n(b, #1:Fresh)), +(e(#6:Sessionkey, n(b, #1:Fresh))), -(e(#6:Sessionkey, n(b, #1:Fresh))) || ghost( #0:Key, :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #1:Fresh)), +(e(#6:Sessionkey, n(b, #1:Fresh))), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, n(b, #1:Fresh))), +(n(b, #1:Fresh)), nil] & :: #1:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #1:Fresh)) | -(e(#6:Sessionkey, n(b, #1:Fresh))), nil] , n(b, #1:Fresh) !inI, e(#6:Sessionkey, n(b, #1:Fresh)) !inI, e(#0:Key, n(b, #1:Fresh)) inI, -(#0:Key), -(e(#0:Key, n(b, #1:Fresh))), +(n(b, #1:Fresh)), -(#6:Sessionkey), -(n(b, #1:Fresh)), +(e(#6:Sessionkey, n(b, #1:Fresh))), -(e(#6:Sessionkey, n(b, #1:Fresh))), nil ), ghost( #6:Sessionkey, :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #1:Fresh)), +(e(#6:Sessionkey, n(b, #1:Fresh))), nil] & :: #1:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #1:Fresh)) | -(e(#6:Sessionkey, n(b, #1:Fresh))), nil] , e(#6:Sessionkey, n(b, #1:Fresh)) !inI, n(b, #1:Fresh) inI, -(#6:Sessionkey), -(n(b, #1:Fresh)), +(e(#6:Sessionkey, n(b, #1:Fresh))), -(e(#6:Sessionkey, n(b, #1:Fresh))), nil ) || nil) (< 1 . 1 . 3 . 4 . 6 > ( :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(#1:Key, n(b, #2:Fresh)) ; #3:Msg)), +(e(#1:Key, n(b, #2:Fresh)) ; #3:Msg), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, n(b, #2:Fresh))), +(n(b, #2:Fresh)), nil] & :: nil :: [ nil | -(e(#1:Key, n(b, #2:Fresh)) ; #3:Msg), +(e(#1:Key, n(b, #2:Fresh))), nil] & :: #2:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #2:Fresh)) | -(e(#6:Sessionkey, n(b, #2:Fresh))), nil] ) || n(b, #2:Fresh) !inI, e(#6:Sessionkey, n(b, #2:Fresh)) !inI, e(#1:Key, n(b, #2:Fresh)) !inI, (e(#1:Key, n(b, #2:Fresh)) ; #3:Msg) !inI, e(#0:Key, e(#1:Key, n(b, #2:Fresh)) ; #3:Msg) inI || -(#0:Key), -(e(#0:Key, e(#1:Key, n(b, #2:Fresh)) ; #3:Msg)), +(e(#1:Key, n(b, #2:Fresh)) ; #3:Msg), -(e(#1:Key, n(b, #2:Fresh)) ; #3:Msg), +(e(#1:Key, n(b, #2:Fresh))), -(#1:Key), -(e(#1:Key, n(b, #2:Fresh))), +(n(b, #2:Fresh)), -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), -(e(#6:Sessionkey, n(b, #2:Fresh))) || ghost( #0:Key, :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(#1:Key, n(b, #2:Fresh)) ; #3:Msg)), +(e(#1:Key, n(b, #2:Fresh)) ; #3:Msg), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, n(b, #2:Fresh))), +(n(b, #2:Fresh)), nil] & :: nil :: [ nil | -(e(#1:Key, n(b, #2:Fresh)) ; #3:Msg), +(e(#1:Key, n(b, #2:Fresh))), nil] & :: #2:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #2:Fresh)) | -(e(#6:Sessionkey, n(b, #2:Fresh))), nil] , n(b, #2:Fresh) !inI, e(#6:Sessionkey, n(b, #2:Fresh)) !inI, e(#1:Key, n(b, #2:Fresh)) !inI, (e(#1:Key, n(b, #2:Fresh)) ; #3:Msg) !inI, e(#0:Key, e(#1:Key, n(b, #2:Fresh)) ; #3:Msg) inI, -(#0:Key), -(e(#0:Key, e(#1:Key, n(b, #2:Fresh)) ; #3:Msg)), +(e(#1:Key, n(b, #2:Fresh)) ; #3:Msg), -(e(#1:Key, n(b, #2:Fresh)) ; #3:Msg), +(e(#1:Key, n(b, #2:Fresh))), -(#1:Key), -(e(#1:Key, n(b, #2:Fresh))), +(n(b, #2:Fresh)), -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), -(e(#6:Sessionkey, n(b, #2:Fresh))), nil ), ghost( #1:Key, :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, n(b, #2:Fresh))), +(n(b, #2:Fresh)), nil] & :: #2:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #2:Fresh)) | -(e(#6:Sessionkey, n(b, #2:Fresh))), nil] , n(b, #2:Fresh) !inI, e(#6:Sessionkey, n(b, #2:Fresh)) !inI, e(#1:Key, n(b, #2:Fresh)) inI, -(#1:Key), -(e(#1:Key, n(b, #2:Fresh))), +(n(b, #2:Fresh)), -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), -(e(#6:Sessionkey, n(b, #2:Fresh))), nil ), ghost( #6:Sessionkey, :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), nil] & :: #2:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #2:Fresh)) | -(e(#6:Sessionkey, n(b, #2:Fresh))), nil] , e(#6:Sessionkey, n(b, #2:Fresh)) !inI, n(b, #2:Fresh) inI, -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), -(e(#6:Sessionkey, n(b, #2:Fresh))), nil ) || nil) (< 1 . 1 . 3 . 4 . 8 > ( :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, n(b, #2:Fresh))), +(n(b, #2:Fresh)), nil] & :: nil :: [ nil | -(#0:Msg ; e(#1:Key, n(b, #2:Fresh)) ; #3:Msg), +(e(#1:Key, n(b, #2:Fresh)) ; #3:Msg), nil] & :: nil :: [ nil | -(e(#1:Key, n(b, #2:Fresh)) ; #3:Msg), +(e(#1:Key, n(b, #2:Fresh))), nil] & :: #2:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #2:Fresh)) | -(e(#6:Sessionkey, n(b, #2:Fresh))), nil] ) || n(b, #2:Fresh) !inI, e(#6:Sessionkey, n(b, #2:Fresh)) !inI, e(#1:Key, n(b, #2:Fresh)) !inI, (e(#1:Key, n(b, #2:Fresh)) ; #3:Msg) !inI, (#0:Msg ; e(#1:Key, n(b, #2:Fresh)) ; #3:Msg) inI || -(#0:Msg ; e(#1:Key, n(b, #2:Fresh)) ; #3:Msg), +(e(#1:Key, n(b, #2:Fresh)) ; #3:Msg), -(e(#1:Key, n(b, #2:Fresh)) ; #3:Msg), +(e(#1:Key, n(b, #2:Fresh))), -(#1:Key), -(e(#1:Key, n(b, #2:Fresh))), +(n(b, #2:Fresh)), -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), -(e(#6:Sessionkey, n(b, #2:Fresh))) || ghost( #1:Key, :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, n(b, #2:Fresh))), +(n(b, #2:Fresh)), nil] & :: #2:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #2:Fresh)) | -(e(#6:Sessionkey, n(b, #2:Fresh))), nil] , n(b, #2:Fresh) !inI, e(#6:Sessionkey, n(b, #2:Fresh)) !inI, e(#1:Key, n(b, #2:Fresh)) inI, -(#1:Key), -(e(#1:Key, n(b, #2:Fresh))), +(n(b, #2:Fresh)), -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), -(e(#6:Sessionkey, n(b, #2:Fresh))), nil ), ghost( #6:Sessionkey, :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), nil] & :: #2:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #2:Fresh)) | -(e(#6:Sessionkey, n(b, #2:Fresh))), nil] , e(#6:Sessionkey, n(b, #2:Fresh)) !inI, n(b, #2:Fresh) inI, -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), -(e(#6:Sessionkey, n(b, #2:Fresh))), nil ) || nil) (< 1 . 1 . 5 . 7 . 1 > ( :: nil :: [ nil | -(#3:Sessionkey), -(n(b, #0:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh))), nil] & :: nil :: [ nil | -(#4:Msg ; e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)), +(e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)), nil] & :: nil :: [ nil | -(e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)), +(n(b, #0:Fresh)), nil] & :: #0:Fresh,#1:Fresh :: [ nil, -(a ; #2:Nonce), +(a ; #2:Nonce ; b ; n(b, #1:Fresh)) | -(e(mkey(b, s), #3:Sessionkey ; n(b, #1:Fresh) ; a) ; #4:Msg), +(#4:Msg ; e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)), -(e(#3:Sessionkey, n(b, #0:Fresh))), nil] ) || n(b, #0:Fresh) !inI, e(#3:Sessionkey, n(b, #0:Fresh)) !inI, (#4:Msg ; e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)) !inI, (e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)) !inI, (e(mkey(b, s), #3:Sessionkey ; n(b, #1:Fresh) ; a) ; #4:Msg) inI || -(e(mkey(b, s), #3:Sessionkey ; n(b, #1:Fresh) ; a) ; #4:Msg), +(#4:Msg ; e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)), -(#4:Msg ; e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)), +(e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)), -(e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)), +(n(b, #0:Fresh)), -(#3:Sessionkey), -(n(b, #0:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh))), -(e(#3:Sessionkey, n(b, #0:Fresh))) || ghost( #3:Sessionkey, :: nil :: [ nil | -(#3:Sessionkey), -(n(b, #0:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh))), nil] & :: #0:Fresh,#1:Fresh :: [ nil, -(a ; #2:Nonce), +(a ; #2:Nonce ; b ; n(b, #1:Fresh)), -(e(mkey(b, s), #3:Sessionkey ; n(b, #1:Fresh) ; a) ; #4:Msg), +(#4:Msg ; e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)) | -(e(#3:Sessionkey, n(b, #0:Fresh))), nil] , e(#3:Sessionkey, n(b, #0:Fresh)) !inI, n(b, #0:Fresh) inI, -(#3:Sessionkey), -(n(b, #0:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh))), -(e(#3:Sessionkey, n(b, #0:Fresh))), nil ) || nil) (< 1 . 1 . 5 . 7 . 5 > ( :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), nil] & :: nil :: [ nil | -(#0:Msg ; #1:Msg ; n(b, #2:Fresh)), +(#1:Msg ; n(b, #2:Fresh)), nil] & :: nil :: [ nil | -(#1:Msg ; n(b, #2:Fresh)), +(n(b, #2:Fresh)), nil] & :: nil :: [ nil | -((#0:Msg ; #1:Msg ; n(b, #2:Fresh)) ; #3:Msg), +(#0:Msg ; #1:Msg ; n(b, #2:Fresh)), nil] & :: #2:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #2:Fresh)) | -(e(#6:Sessionkey, n(b, #2:Fresh))), nil] ) || n(b, #2:Fresh) !inI, e(#6:Sessionkey, n(b, #2:Fresh)) !inI, (#0:Msg ; #1:Msg ; n(b, #2:Fresh)) !inI, (#1:Msg ; n(b, #2:Fresh)) !inI, ((#0:Msg ; #1:Msg ; n(b, #2:Fresh)) ; #3:Msg) inI || -((#0:Msg ; #1:Msg ; n(b, #2:Fresh)) ; #3:Msg), +(#0:Msg ; #1:Msg ; n(b, #2:Fresh)), -(#0:Msg ; #1:Msg ; n(b, #2:Fresh)), +(#1:Msg ; n(b, #2:Fresh)), -(#1:Msg ; n(b, #2:Fresh)), +(n(b, #2:Fresh)), -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), -(e(#6:Sessionkey, n(b, #2:Fresh))) || ghost( #6:Sessionkey, :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), nil] & :: #2:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #2:Fresh)) | -(e(#6:Sessionkey, n(b, #2:Fresh))), nil] , e(#6:Sessionkey, n(b, #2:Fresh)) !inI, n(b, #2:Fresh) inI, -(#6:Sessionkey), -(n(b, #2:Fresh)), +(e(#6:Sessionkey, n(b, #2:Fresh))), -(e(#6:Sessionkey, n(b, #2:Fresh))), nil ) || nil) (< 1 . 1 . 5 . 7 . 6 > ( :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #3:Fresh)), +(e(#6:Sessionkey, n(b, #3:Fresh))), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, #1:Msg ; #2:Msg ; n(b, #3:Fresh))), +(#1:Msg ; #2:Msg ; n(b, #3:Fresh)), nil] & :: nil :: [ nil | -(#1:Msg ; #2:Msg ; n(b, #3:Fresh)), +(#2:Msg ; n(b, #3:Fresh)), nil] & :: nil :: [ nil | -(#2:Msg ; n(b, #3:Fresh)), +(n(b, #3:Fresh)), nil] & :: #3:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #3:Fresh)) | -(e(#6:Sessionkey, n(b, #3:Fresh))), nil] ) || n(b, #3:Fresh) !inI, e(#6:Sessionkey, n(b, #3:Fresh)) !inI, (#1:Msg ; #2:Msg ; n(b, #3:Fresh)) !inI, (#2:Msg ; n(b, #3:Fresh)) !inI, e(#0:Key, #1:Msg ; #2:Msg ; n(b, #3:Fresh)) inI || -(#0:Key), -(e(#0:Key, #1:Msg ; #2:Msg ; n(b, #3:Fresh))), +(#1:Msg ; #2:Msg ; n(b, #3:Fresh)), -(#1:Msg ; #2:Msg ; n(b, #3:Fresh)), +(#2:Msg ; n(b, #3:Fresh)), -(#2:Msg ; n(b, #3:Fresh)), +(n(b, #3:Fresh)), -(#6:Sessionkey), -(n(b, #3:Fresh)), +(e(#6:Sessionkey, n(b, #3:Fresh))), -(e(#6:Sessionkey, n(b, #3:Fresh))) || ghost( #0:Key, :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #3:Fresh)), +(e(#6:Sessionkey, n(b, #3:Fresh))), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, #1:Msg ; #2:Msg ; n(b, #3:Fresh))), +(#1:Msg ; #2:Msg ; n(b, #3:Fresh)), nil] & :: nil :: [ nil | -(#1:Msg ; #2:Msg ; n(b, #3:Fresh)), +(#2:Msg ; n(b, #3:Fresh)), nil] & :: nil :: [ nil | -(#2:Msg ; n(b, #3:Fresh)), +(n(b, #3:Fresh)), nil] & :: #3:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #3:Fresh)) | -(e(#6:Sessionkey, n(b, #3:Fresh))), nil] , n(b, #3:Fresh) !inI, e(#6:Sessionkey, n(b, #3:Fresh)) !inI, (#1:Msg ; #2:Msg ; n(b, #3:Fresh)) !inI, (#2:Msg ; n(b, #3:Fresh)) !inI, e(#0:Key, #1:Msg ; #2:Msg ; n(b, #3:Fresh)) inI, -(#0:Key), -(e(#0:Key, #1:Msg ; #2:Msg ; n(b, #3:Fresh))), +(#1:Msg ; #2:Msg ; n(b, #3:Fresh)), -(#1:Msg ; #2:Msg ; n(b, #3:Fresh)), +(#2:Msg ; n(b, #3:Fresh)), -(#2:Msg ; n(b, #3:Fresh)), +(n(b, #3:Fresh)), -(#6:Sessionkey), -(n(b, #3:Fresh)), +(e(#6:Sessionkey, n(b, #3:Fresh))), -(e(#6:Sessionkey, n(b, #3:Fresh))), nil ), ghost( #6:Sessionkey, :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #3:Fresh)), +(e(#6:Sessionkey, n(b, #3:Fresh))), nil] & :: #3:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #3:Fresh)) | -(e(#6:Sessionkey, n(b, #3:Fresh))), nil] , e(#6:Sessionkey, n(b, #3:Fresh)) !inI, n(b, #3:Fresh) inI, -(#6:Sessionkey), -(n(b, #3:Fresh)), +(e(#6:Sessionkey, n(b, #3:Fresh))), -(e(#6:Sessionkey, n(b, #3:Fresh))), nil ) || nil) (< 1 . 1 . 5 . 7 . 8 > ( :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #3:Fresh)), +(e(#6:Sessionkey, n(b, #3:Fresh))), nil] & :: nil :: [ nil | -(#0:Msg ; #1:Msg ; #2:Msg ; n(b, #3:Fresh)), +(#1:Msg ; #2:Msg ; n(b, #3:Fresh)), nil] & :: nil :: [ nil | -(#1:Msg ; #2:Msg ; n(b, #3:Fresh)), +(#2:Msg ; n(b, #3:Fresh)), nil] & :: nil :: [ nil | -(#2:Msg ; n(b, #3:Fresh)), +(n(b, #3:Fresh)), nil] & :: #3:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #3:Fresh)) | -(e(#6:Sessionkey, n(b, #3:Fresh))), nil] ) || n(b, #3:Fresh) !inI, e(#6:Sessionkey, n(b, #3:Fresh)) !inI, (#1:Msg ; #2:Msg ; n(b, #3:Fresh)) !inI, (#2:Msg ; n(b, #3:Fresh)) !inI, (#0:Msg ; #1:Msg ; #2:Msg ; n(b, #3:Fresh)) inI || -(#0:Msg ; #1:Msg ; #2:Msg ; n(b, #3:Fresh)), +(#1:Msg ; #2:Msg ; n(b, #3:Fresh)), -(#1:Msg ; #2:Msg ; n(b, #3:Fresh)), +(#2:Msg ; n(b, #3:Fresh)), -(#2:Msg ; n(b, #3:Fresh)), +(n(b, #3:Fresh)), -(#6:Sessionkey), -(n(b, #3:Fresh)), +(e(#6:Sessionkey, n(b, #3:Fresh))), -(e(#6:Sessionkey, n(b, #3:Fresh))) || ghost( #6:Sessionkey, :: nil :: [ nil | -(#6:Sessionkey), -(n(b, #3:Fresh)), +(e(#6:Sessionkey, n(b, #3:Fresh))), nil] & :: #3:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), #6:Sessionkey ; n(b, #4:Fresh) ; a) ; #7:Msg), +(#7:Msg ; e(#6:Sessionkey, #5:Nonce) ; n(b, #3:Fresh)) | -(e(#6:Sessionkey, n(b, #3:Fresh))), nil] , e(#6:Sessionkey, n(b, #3:Fresh)) !inI, n(b, #3:Fresh) inI, -(#6:Sessionkey), -(n(b, #3:Fresh)), +(e(#6:Sessionkey, n(b, #3:Fresh))), -(e(#6:Sessionkey, n(b, #3:Fresh))), nil ) || nil) (< 1 . 5 . 6 . 1 . 2 > ( :: nil :: [ nil | -(#0:Msg), -(e(mkey(b, s), #1:Sessionkey ; n(b, #2:Fresh) ; a)), +(e(mkey(b, s), #1:Sessionkey ; n(b, #2:Fresh) ; a) ; #0:Msg), nil] & :: nil :: [ nil | -(#0:Msg ; e(#1:Sessionkey, n(b, #3:Fresh)) ; n(b, #3:Fresh)), +(e(#1:Sessionkey, n(b, #3:Fresh)) ; n(b, #3:Fresh)), nil] & :: nil :: [ nil | -(e(#1:Sessionkey, n(b, #3:Fresh)) ; n(b, #3:Fresh)), +(e(#1:Sessionkey, n(b, #3:Fresh))), nil] & :: #2:Fresh,#3:Fresh :: [ nil, -(a ; n(b, #3:Fresh)), +(a ; n(b, #3:Fresh) ; b ; n(b, #2:Fresh)) | -(e(mkey(b, s), #1:Sessionkey ; n(b, #2:Fresh) ; a) ; #0:Msg), +(#0:Msg ; e(#1:Sessionkey, n(b, #3:Fresh)) ; n(b, #3:Fresh)), -(e(#1:Sessionkey, n(b, #3:Fresh))), nil] ) || #0:Msg !inI, e(#1:Sessionkey, n(b, #3:Fresh)) !inI, (#0:Msg ; e(#1:Sessionkey, n(b, #3:Fresh)) ; n(b, #3:Fresh)) !inI, (e(#1:Sessionkey, n(b, #3:Fresh)) ; n(b, #3:Fresh)) !inI, (e(mkey(b, s), #1:Sessionkey ; n(b, #2:Fresh) ; a) ; #0:Msg) !inI, e(mkey(b, s), #1:Sessionkey ; n(b, #2:Fresh) ; a) inI || generatedByIntruder(#0:Msg), -(#0:Msg), -(e(mkey(b, s), #1:Sessionkey ; n(b, #2:Fresh) ; a)), +(e(mkey(b, s), #1:Sessionkey ; n(b, #2:Fresh) ; a) ; #0:Msg), -(e(mkey(b, s), #1:Sessionkey ; n(b, #2:Fresh) ; a) ; #0:Msg), +(#0:Msg ; e(#1:Sessionkey, n(b, #3:Fresh)) ; n(b, #3:Fresh)), -(#0:Msg ; e(#1:Sessionkey, n(b, #3:Fresh)) ; n(b, #3:Fresh)), +(e(#1:Sessionkey, n(b, #3:Fresh)) ; n(b, #3:Fresh)), -(e(#1:Sessionkey, n(b, #3:Fresh)) ; n(b, #3:Fresh)), +(e(#1:Sessionkey, n(b, #3:Fresh))), -(e(#1:Sessionkey, n(b, #3:Fresh))) || nil || nil) (< 1 . 5 . 6 . 1 . 7 > ( :: nil :: [ nil | -(e(#2:Sessionkey, n(b, #0:Fresh)) ; n(b, #0:Fresh)), +(e(#2:Sessionkey, n(b, #0:Fresh))), nil] & :: nil :: [ nil | -((e(#3:Sessionkey, #4:Nonce) ; n(#5:UName, #6:Fresh)) ; e(#2:Sessionkey, n(b, #0:Fresh)) ; n(b, #0:Fresh)), +(e(#2:Sessionkey, n(b, #0:Fresh)) ; n(b, #0:Fresh)), nil] & :: #0:Fresh,#1:Fresh :: [ nil, -(a ; n(b, #0:Fresh)), +(a ; n(b, #0:Fresh) ; b ; n(b, #1:Fresh)) | -(e(mkey(b, s), #2:Sessionkey ; n(b, #1:Fresh) ; a) ; e(#3:Sessionkey, #4:Nonce) ; n(#5:UName, #6:Fresh)), +((e(#3:Sessionkey, #4:Nonce) ; n(#5:UName, #6:Fresh)) ; e(#2:Sessionkey, n(b, #0:Fresh)) ; n(b, #0:Fresh)), -(e(#2:Sessionkey, n(b, #0:Fresh))), nil] & :: #6:Fresh,#7:Fresh :: [ nil, -(#8:UName ; #4:Nonce), +(#8:UName ; #4:Nonce ; #5:UName ; n(#5:UName, #7:Fresh)) | -(e(mkey(s, #5:UName), #3:Sessionkey ; n(#5:UName, #7:Fresh) ; #8:UName) ; e(mkey(b, s), #2:Sessionkey ; n(b, #1:Fresh) ; a)), +(e(mkey(b, s), #2:Sessionkey ; n(b, #1:Fresh) ; a) ; e(#3:Sessionkey, #4:Nonce) ; n(#5:UName, #6:Fresh)), nil] ) || e(#2:Sessionkey, n(b, #0:Fresh)) !inI, (e(#2:Sessionkey, n(b, #0:Fresh)) ; n(b, #0:Fresh)) !inI, (e(mkey(b, s), #2:Sessionkey ; n(b, #1:Fresh) ; a) ; e(#3:Sessionkey, #4:Nonce) ; n(#5:UName, #6:Fresh)) !inI, ((e(#3:Sessionkey, #4:Nonce) ; n(#5:UName, #6:Fresh)) ; e(#2:Sessionkey, n(b, #0:Fresh)) ; n(b, #0:Fresh)) !inI, (e(mkey(s, #5:UName), #3:Sessionkey ; n(#5:UName, #7:Fresh) ; #8:UName) ; e(mkey(b, s), #2:Sessionkey ; n(b, #1:Fresh) ; a)) inI || -(e(mkey(s, #5:UName), #3:Sessionkey ; n(#5:UName, #7:Fresh) ; #8:UName) ; e(mkey(b, s), #2:Sessionkey ; n(b, #1:Fresh) ; a)), +(e(mkey(b, s), #2:Sessionkey ; n(b, #1:Fresh) ; a) ; e(#3:Sessionkey, #4:Nonce) ; n(#5:UName, #6:Fresh)), -(e(mkey(b, s), #2:Sessionkey ; n(b, #1:Fresh) ; a) ; e(#3:Sessionkey, #4:Nonce) ; n(#5:UName, #6:Fresh)), +((e(#3:Sessionkey, #4:Nonce) ; n(#5:UName, #6:Fresh)) ; e(#2:Sessionkey, n(b, #0:Fresh)) ; n(b, #0:Fresh)), -((e(#3:Sessionkey, #4:Nonce) ; n(#5:UName, #6:Fresh)) ; e(#2:Sessionkey, n(b, #0:Fresh)) ; n(b, #0:Fresh)), +(e(#2:Sessionkey, n(b, #0:Fresh)) ; n(b, #0:Fresh)), -(e(#2:Sessionkey, n(b, #0:Fresh)) ; n(b, #0:Fresh)), +(e(#2:Sessionkey, n(b, #0:Fresh))), -(e(#2:Sessionkey, n(b, #0:Fresh))) || nil || nil) (< 1 . 5 . 6 . 1 . 8 > ( :: nil :: [ nil | -(e(mkey(a, s), #1:Nonce ; b ; seskey(a, b, n(#3:UName, #0:Fresh))) ; e(seskey(a, b, n(#3:UName, #0:Fresh)), n(b, #4:Fresh)) ; n(b, #4:Fresh)), +(e(seskey(a, b, n(#3:UName, #0:Fresh)), n(b, #4:Fresh)) ; n(b, #4:Fresh)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(#3:UName, #0:Fresh)), n(b, #4:Fresh)) ; n(b, #4:Fresh)), +(e(seskey(a, b, n(#3:UName, #0:Fresh)), n(b, #4:Fresh))), nil] & :: #0:Fresh :: [ nil | -(a ; #1:Nonce ; b ; n(b, #2:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#3:UName, #0:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), #1:Nonce ; b ; seskey(a, b, n(#3:UName, #0:Fresh)))), nil] & :: #2:Fresh,#4:Fresh :: [ nil, -(a ; n(b, #4:Fresh)), +(a ; n(b, #4:Fresh) ; b ; n(b, #2:Fresh)) | -(e(mkey(b, s), seskey(a, b, n(#3:UName, #0:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), #1:Nonce ; b ; seskey(a, b, n(#3:UName, #0:Fresh)))), +(e(mkey(a, s), #1:Nonce ; b ; seskey(a, b, n(#3:UName, #0:Fresh))) ; e(seskey(a, b, n(#3:UName, #0:Fresh)), n(b, #4:Fresh)) ; n(b, #4:Fresh)), -(e(seskey(a, b, n(#3:UName, #0:Fresh)), n(b, #4:Fresh))), nil] ) || e(seskey(a, b, n(#3:UName, #0:Fresh)), n(b, #4:Fresh)) !inI, (e(mkey(a, s), #1:Nonce ; b ; seskey(a, b, n(#3:UName, #0:Fresh))) ; e(seskey(a, b, n(#3:UName, #0:Fresh)), n(b, #4:Fresh)) ; n(b, #4:Fresh)) !inI, (e(mkey(b, s), seskey(a, b, n(#3:UName, #0:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), #1:Nonce ; b ; seskey(a, b, n(#3:UName, #0:Fresh)))) !inI, (e(seskey(a, b, n(#3:UName, #0:Fresh)), n(b, #4:Fresh)) ; n(b, #4:Fresh)) !inI, (a ; #1:Nonce ; b ; n(b, #2:Fresh)) inI || -(a ; #1:Nonce ; b ; n(b, #2:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#3:UName, #0:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), #1:Nonce ; b ; seskey(a, b, n(#3:UName, #0:Fresh)))), -(e(mkey(b, s), seskey(a, b, n(#3:UName, #0:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), #1:Nonce ; b ; seskey(a, b, n(#3:UName, #0:Fresh)))), +(e(mkey(a, s), #1:Nonce ; b ; seskey(a, b, n(#3:UName, #0:Fresh))) ; e(seskey(a, b, n(#3:UName, #0:Fresh)), n(b, #4:Fresh)) ; n(b, #4:Fresh)), -(e(mkey(a, s), #1:Nonce ; b ; seskey(a, b, n(#3:UName, #0:Fresh))) ; e(seskey(a, b, n(#3:UName, #0:Fresh)), n(b, #4:Fresh)) ; n(b, #4:Fresh)), +(e(seskey(a, b, n(#3:UName, #0:Fresh)), n(b, #4:Fresh)) ; n(b, #4:Fresh)), -(e(seskey(a, b, n(#3:UName, #0:Fresh)), n(b, #4:Fresh)) ; n(b, #4:Fresh)), +(e(seskey(a, b, n(#3:UName, #0:Fresh)), n(b, #4:Fresh))), -(e(seskey(a, b, n(#3:UName, #0:Fresh)), n(b, #4:Fresh))) || nil || nil) (< 1 . 5 . 6 . 8 . 4 > ( :: nil :: [ nil | -(#0:Msg), -(e(mkey(s, #1:UName), #2:Sessionkey ; n(#1:UName, #3:Fresh) ; #4:UName)), +(e(mkey(s, #1:UName), #2:Sessionkey ; n(#1:UName, #3:Fresh) ; #4:UName) ; #0:Msg), nil] & :: nil :: [ nil | -(#0:Msg ; e(#2:Sessionkey, n(b, #5:Fresh)) ; n(#1:UName, #9:Fresh)), +(e(#2:Sessionkey, n(b, #5:Fresh)) ; n(#1:UName, #9:Fresh)), nil] & :: nil :: [ nil | -(e(#2:Sessionkey, n(b, #5:Fresh)) ; n(#1:UName, #9:Fresh)), +(e(#2:Sessionkey, n(b, #5:Fresh))), nil] & :: #3:Fresh,#9:Fresh :: [ nil, -(#4:UName ; n(b, #5:Fresh)), +(#4:UName ; n(b, #5:Fresh) ; #1:UName ; n(#1:UName, #3:Fresh)) | -(e(mkey(s, #1:UName), #2:Sessionkey ; n(#1:UName, #3:Fresh) ; #4:UName) ; #0:Msg), +(#0:Msg ; e(#2:Sessionkey, n(b, #5:Fresh)) ; n(#1:UName, #9:Fresh)), nil] & :: #5:Fresh,#6:Fresh :: [ nil, -(a ; #7:Nonce), +(a ; #7:Nonce ; b ; n(b, #6:Fresh)), -(e(mkey(b, s), #2:Sessionkey ; n(b, #6:Fresh) ; a) ; #8:Msg), +(#8:Msg ; e(#2:Sessionkey, #7:Nonce) ; n(b, #5:Fresh)) | -(e(#2:Sessionkey, n(b, #5:Fresh))), nil] ) || #0:Msg !inI, e(#2:Sessionkey, n(b, #5:Fresh)) !inI, (#0:Msg ; e(#2:Sessionkey, n(b, #5:Fresh)) ; n(#1:UName, #9:Fresh)) !inI, (e(#2:Sessionkey, n(b, #5:Fresh)) ; n(#1:UName, #9:Fresh)) !inI, (e(mkey(s, #1:UName), #2:Sessionkey ; n(#1:UName, #3:Fresh) ; #4:UName) ; #0:Msg) !inI, e(mkey(s, #1:UName), #2:Sessionkey ; n(#1:UName, #3:Fresh) ; #4:UName) inI || generatedByIntruder(#0:Msg), -(#0:Msg), -(e(mkey(s, #1:UName), #2:Sessionkey ; n(#1:UName, #3:Fresh) ; #4:UName)), +(e(mkey(s, #1:UName), #2:Sessionkey ; n(#1:UName, #3:Fresh) ; #4:UName) ; #0:Msg), -(e(mkey(s, #1:UName), #2:Sessionkey ; n(#1:UName, #3:Fresh) ; #4:UName) ; #0:Msg), +(#0:Msg ; e(#2:Sessionkey, n(b, #5:Fresh)) ; n(#1:UName, #9:Fresh)), -(#0:Msg ; e(#2:Sessionkey, n(b, #5:Fresh)) ; n(#1:UName, #9:Fresh)), +(e(#2:Sessionkey, n(b, #5:Fresh)) ; n(#1:UName, #9:Fresh)), -(e(#2:Sessionkey, n(b, #5:Fresh)) ; n(#1:UName, #9:Fresh)), +(e(#2:Sessionkey, n(b, #5:Fresh))), -(e(#2:Sessionkey, n(b, #5:Fresh))) || nil || nil) (< 1 . 5 . 6 . 8 . 9 > ( :: nil :: [ nil | -(e(#3:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh))), nil] & :: nil :: [ nil | -((e(#9:Sessionkey, #10:Nonce) ; n(#11:UName, #12:Fresh)) ; e(#3:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), nil] & :: #0:Fresh,#1:Fresh :: [ nil, -(a ; #2:Nonce), +(a ; #2:Nonce ; b ; n(b, #1:Fresh)), -(e(mkey(b, s), #3:Sessionkey ; n(b, #1:Fresh) ; a) ; #4:Msg), +(#4:Msg ; e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)) | -(e(#3:Sessionkey, n(b, #0:Fresh))), nil] & :: #5:Fresh,#6:Fresh :: [ nil, -(#7:UName ; n(b, #0:Fresh)), +(#7:UName ; n(b, #0:Fresh) ; #8:UName ; n(#8:UName, #6:Fresh)) | -(e(mkey(s, #8:UName), #3:Sessionkey ; n(#8:UName, #6:Fresh) ; #7:UName) ; e(#9:Sessionkey, #10:Nonce) ; n(#11:UName, #12:Fresh)), +((e(#9:Sessionkey, #10:Nonce) ; n(#11:UName, #12:Fresh)) ; e(#3:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), nil] & :: #12:Fresh,#13:Fresh :: [ nil, -(#14:UName ; #10:Nonce), +(#14:UName ; #10:Nonce ; #11:UName ; n(#11:UName, #13:Fresh)) | -(e(mkey(s, #11:UName), #9:Sessionkey ; n(#11:UName, #13:Fresh) ; #14:UName) ; e(mkey(s, #8:UName), #3:Sessionkey ; n(#8:UName, #6:Fresh) ; #7:UName)), +(e(mkey(s, #8:UName), #3:Sessionkey ; n(#8:UName, #6:Fresh) ; #7:UName) ; e(#9:Sessionkey, #10:Nonce) ; n(#11:UName, #12:Fresh)), nil] ) || e(#3:Sessionkey, n(b, #0:Fresh)) !inI, (e(#3:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)) !inI, (e(mkey(s, #8:UName), #3:Sessionkey ; n(#8:UName, #6:Fresh) ; #7:UName) ; e(#9:Sessionkey, #10:Nonce) ; n(#11:UName, #12:Fresh)) !inI, ((e(#9:Sessionkey, #10:Nonce) ; n(#11:UName, #12:Fresh)) ; e(#3:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)) !inI, (e(mkey(s, #11:UName), #9:Sessionkey ; n(#11:UName, #13:Fresh) ; #14:UName) ; e(mkey(s, #8:UName), #3:Sessionkey ; n(#8:UName, #6:Fresh) ; #7:UName)) inI || -(e(mkey(s, #11:UName), #9:Sessionkey ; n(#11:UName, #13:Fresh) ; #14:UName) ; e(mkey(s, #8:UName), #3:Sessionkey ; n(#8:UName, #6:Fresh) ; #7:UName)), +(e(mkey(s, #8:UName), #3:Sessionkey ; n(#8:UName, #6:Fresh) ; #7:UName) ; e(#9:Sessionkey, #10:Nonce) ; n(#11:UName, #12:Fresh)), -(e(mkey(s, #8:UName), #3:Sessionkey ; n(#8:UName, #6:Fresh) ; #7:UName) ; e(#9:Sessionkey, #10:Nonce) ; n(#11:UName, #12:Fresh)), +((e(#9:Sessionkey, #10:Nonce) ; n(#11:UName, #12:Fresh)) ; e(#3:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), -((e(#9:Sessionkey, #10:Nonce) ; n(#11:UName, #12:Fresh)) ; e(#3:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), -(e(#3:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh))), -(e(#3:Sessionkey, n(b, #0:Fresh))) || nil || nil) (< 1 . 6 . 3 . 5 . 8 > ( :: nil :: [ nil | -(mkey(s, #0:UName)), -(n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey), +(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), nil] & :: nil :: [ nil | -(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), -(e(mkey(b, s), #3:Sessionkey ; n(b, #5:Fresh) ; a)), +(e(mkey(b, s), #3:Sessionkey ; n(b, #5:Fresh) ; a) ; e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), nil] & :: #1:Fresh :: [ nil, +(#0:UName ; n(#0:UName, #1:Fresh)) | -(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#0:UName, #1:Fresh)) ; n(b, #4:Fresh)), +(e(#3:Sessionkey, n(b, #4:Fresh))), nil] & :: #4:Fresh,#5:Fresh :: [ nil, -(a ; n(#0:UName, #1:Fresh)), +(a ; n(#0:UName, #1:Fresh) ; b ; n(b, #5:Fresh)) | -(e(mkey(b, s), #3:Sessionkey ; n(b, #5:Fresh) ; a) ; e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), +(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#0:UName, #1:Fresh)) ; n(b, #4:Fresh)), -(e(#3:Sessionkey, n(b, #4:Fresh))), nil] ) || e(#3:Sessionkey, n(b, #4:Fresh)) !inI, e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) !inI, (e(mkey(b, s), #3:Sessionkey ; n(b, #5:Fresh) ; a) ; e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)) !inI, (e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#0:UName, #1:Fresh)) ; n(b, #4:Fresh)) !inI, mkey(s, #0:UName) inI, e(mkey(b, s), #3:Sessionkey ; n(b, #5:Fresh) ; a) inI, (n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) inI, inst(#0:UName), inst(#2:UName), inst(#3:Sessionkey) || -(mkey(s, #0:UName)), -(n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey), +(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), -(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), -(e(mkey(b, s), #3:Sessionkey ; n(b, #5:Fresh) ; a)), +(e(mkey(b, s), #3:Sessionkey ; n(b, #5:Fresh) ; a) ; e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), -(e(mkey(b, s), #3:Sessionkey ; n(b, #5:Fresh) ; a) ; e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), +(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#0:UName, #1:Fresh)) ; n(b, #4:Fresh)), -(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#0:UName, #1:Fresh)) ; n(b, #4:Fresh)), +(e(#3:Sessionkey, n(b, #4:Fresh))), -(e(#3:Sessionkey, n(b, #4:Fresh))) || nil || nil) (< 1 . 6 . 3 . 5 . 9 > ( :: nil :: [ nil | -(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), -(e(mkey(b, s), #3:Sessionkey ; n(b, #6:Fresh) ; a)), +(e(mkey(b, s), #3:Sessionkey ; n(b, #6:Fresh) ; a) ; e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), nil] & :: nil :: [ nil | -(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) ; #4:Msg), +(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), nil] & :: #1:Fresh :: [ nil, +(#0:UName ; n(#0:UName, #1:Fresh)) | -(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#0:UName, #1:Fresh)) ; n(b, #5:Fresh)), +(e(#3:Sessionkey, n(b, #5:Fresh))), nil] & :: #5:Fresh,#6:Fresh :: [ nil, -(a ; n(#0:UName, #1:Fresh)), +(a ; n(#0:UName, #1:Fresh) ; b ; n(b, #6:Fresh)) | -(e(mkey(b, s), #3:Sessionkey ; n(b, #6:Fresh) ; a) ; e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), +(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#0:UName, #1:Fresh)) ; n(b, #5:Fresh)), -(e(#3:Sessionkey, n(b, #5:Fresh))), nil] ) || e(#3:Sessionkey, n(b, #5:Fresh)) !inI, e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) !inI, (e(mkey(b, s), #3:Sessionkey ; n(b, #6:Fresh) ; a) ; e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)) !inI, (e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#0:UName, #1:Fresh)) ; n(b, #5:Fresh)) !inI, e(mkey(b, s), #3:Sessionkey ; n(b, #6:Fresh) ; a) inI, (e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) ; #4:Msg) inI, inst(#0:UName), inst(#2:UName), inst(#3:Sessionkey) || -(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) ; #4:Msg), +(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), -(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), -(e(mkey(b, s), #3:Sessionkey ; n(b, #6:Fresh) ; a)), +(e(mkey(b, s), #3:Sessionkey ; n(b, #6:Fresh) ; a) ; e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), -(e(mkey(b, s), #3:Sessionkey ; n(b, #6:Fresh) ; a) ; e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey)), +(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#0:UName, #1:Fresh)) ; n(b, #5:Fresh)), -(e(mkey(s, #0:UName), n(#0:UName, #1:Fresh) ; #2:UName ; #3:Sessionkey) ; e(#3:Sessionkey, n(#0:UName, #1:Fresh)) ; n(b, #5:Fresh)), +(e(#3:Sessionkey, n(b, #5:Fresh))), -(e(#3:Sessionkey, n(b, #5:Fresh))) || nil || nil) (< 1 . 6 . 3 . 5 . 10 > ( :: nil :: [ nil | -(e(mkey(s, #1:UName), n(#1:UName, #2:Fresh) ; #3:UName ; #4:Sessionkey)), -(e(mkey(b, s), #4:Sessionkey ; n(b, #6:Fresh) ; a)), +(e(mkey(b, s), #4:Sessionkey ; n(b, #6:Fresh) ; a) ; e(mkey(s, #1:UName), n(#1:UName, #2:Fresh) ; #3:UName ; #4:Sessionkey)), nil] & :: nil :: [ nil | -(#0:Msg ; e(mkey(s, #1:UName), n(#1:UName, #2:Fresh) ; #3:UName ; #4:Sessionkey)), +(e(mkey(s, #1:UName), n(#1:UName, #2:Fresh) ; #3:UName ; #4:Sessionkey)), nil] & :: #2:Fresh :: [ nil, +(#1:UName ; n(#1:UName, #2:Fresh)) | -(e(mkey(s, #1:UName), n(#1:UName, #2:Fresh) ; #3:UName ; #4:Sessionkey) ; e(#4:Sessionkey, n(#1:UName, #2:Fresh)) ; n(b, #5:Fresh)), +(e(#4:Sessionkey, n(b, #5:Fresh))), nil] & :: #5:Fresh,#6:Fresh :: [ nil, -(a ; n(#1:UName, #2:Fresh)), +(a ; n(#1:UName, #2:Fresh) ; b ; n(b, #6:Fresh)) | -(e(mkey(b, s), #4:Sessionkey ; n(b, #6:Fresh) ; a) ; e(mkey(s, #1:UName), n(#1:UName, #2:Fresh) ; #3:UName ; #4:Sessionkey)), +(e(mkey(s, #1:UName), n(#1:UName, #2:Fresh) ; #3:UName ; #4:Sessionkey) ; e(#4:Sessionkey, n(#1:UName, #2:Fresh)) ; n(b, #5:Fresh)), -(e(#4:Sessionkey, n(b, #5:Fresh))), nil] ) || e(#4:Sessionkey, n(b, #5:Fresh)) !inI, e(mkey(s, #1:UName), n(#1:UName, #2:Fresh) ; #3:UName ; #4:Sessionkey) !inI, (e(mkey(b, s), #4:Sessionkey ; n(b, #6:Fresh) ; a) ; e(mkey(s, #1:UName), n(#1:UName, #2:Fresh) ; #3:UName ; #4:Sessionkey)) !inI, (e(mkey(s, #1:UName), n(#1:UName, #2:Fresh) ; #3:UName ; #4:Sessionkey) ; e(#4:Sessionkey, n(#1:UName, #2:Fresh)) ; n(b, #5:Fresh)) !inI, e(mkey(b, s), #4:Sessionkey ; n(b, #6:Fresh) ; a) inI, (#0:Msg ; e(mkey(s, #1:UName), n(#1:UName, #2:Fresh) ; #3:UName ; #4:Sessionkey)) inI, inst(#1:UName), inst(#3:UName), inst(#4:Sessionkey) || -(#0:Msg ; e(mkey(s, #1:UName), n(#1:UName, #2:Fresh) ; #3:UName ; #4:Sessionkey)), +(e(mkey(s, #1:UName), n(#1:UName, #2:Fresh) ; #3:UName ; #4:Sessionkey)), -(e(mkey(s, #1:UName), n(#1:UName, #2:Fresh) ; #3:UName ; #4:Sessionkey)), -(e(mkey(b, s), #4:Sessionkey ; n(b, #6:Fresh) ; a)), +(e(mkey(b, s), #4:Sessionkey ; n(b, #6:Fresh) ; a) ; e(mkey(s, #1:UName), n(#1:UName, #2:Fresh) ; #3:UName ; #4:Sessionkey)), -(e(mkey(b, s), #4:Sessionkey ; n(b, #6:Fresh) ; a) ; e(mkey(s, #1:UName), n(#1:UName, #2:Fresh) ; #3:UName ; #4:Sessionkey)), +(e(mkey(s, #1:UName), n(#1:UName, #2:Fresh) ; #3:UName ; #4:Sessionkey) ; e(#4:Sessionkey, n(#1:UName, #2:Fresh)) ; n(b, #5:Fresh)), -(e(mkey(s, #1:UName), n(#1:UName, #2:Fresh) ; #3:UName ; #4:Sessionkey) ; e(#4:Sessionkey, n(#1:UName, #2:Fresh)) ; n(b, #5:Fresh)), +(e(#4:Sessionkey, n(b, #5:Fresh))), -(e(#4:Sessionkey, n(b, #5:Fresh))) || nil || nil) (< 1 . 6 . 3 . 5 . 11 > ( :: nil :: [ nil | -(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a)), +(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), nil] & :: nil :: [ nil | -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; #2:Msg), +(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a)), nil] & :: #3:Fresh :: [ nil, +(#4:UName ; n(#4:UName, #3:Fresh)) | -(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; e(#0:Sessionkey, n(#4:UName, #3:Fresh)) ; n(b, #6:Fresh)), +(e(#0:Sessionkey, n(b, #6:Fresh))), nil] & :: #1:Fresh,#6:Fresh :: [ nil, -(a ; n(#4:UName, #3:Fresh)), +(a ; n(#4:UName, #3:Fresh) ; b ; n(b, #1:Fresh)) | -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), +(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; e(#0:Sessionkey, n(#4:UName, #3:Fresh)) ; n(b, #6:Fresh)), -(e(#0:Sessionkey, n(b, #6:Fresh))), nil] ) || e(#0:Sessionkey, n(b, #6:Fresh)) !inI, e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) !inI, (e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)) !inI, (e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; e(#0:Sessionkey, n(#4:UName, #3:Fresh)) ; n(b, #6:Fresh)) !inI, e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) inI, (e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; #2:Msg) inI, inst(#4:UName), inst(#5:UName), inst(#0:Sessionkey) || -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; #2:Msg), +(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a)), -(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a)), +(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), +(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; e(#0:Sessionkey, n(#4:UName, #3:Fresh)) ; n(b, #6:Fresh)), -(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; e(#0:Sessionkey, n(#4:UName, #3:Fresh)) ; n(b, #6:Fresh)), +(e(#0:Sessionkey, n(b, #6:Fresh))), -(e(#0:Sessionkey, n(b, #6:Fresh))) || nil || nil) (< 1 . 6 . 3 . 8 . 2 > ( :: #0:Fresh :: [ nil, +(a ; n(a, #0:Fresh)) | -(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)), +(e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh))), nil] & :: #2:Fresh :: [ nil | -(a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))), nil] & :: #3:Fresh,#4:Fresh :: [ nil | -(a ; n(a, #0:Fresh)), +(a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))), +(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)), -(e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh))), nil] ) || e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh)) !inI, (a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)) !inI, (e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)) !inI, (e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))) !inI, (a ; n(a, #0:Fresh)) inI, inst(#1:UName) || -(a ; n(a, #0:Fresh)), +(a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)), -(a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))), -(e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))), +(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)), -(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)), +(e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh))), -(e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh))) || nil || nil) < 1 . 6 . 3 . 8 . 7 > ( :: nil :: [ nil | -(n(a, #0:Fresh) ; b ; n(b, #1:Fresh)), -(a), +(a ; n(a, #0:Fresh) ; b ; n(b, #1:Fresh)), nil] & :: #0:Fresh :: [ nil, +(a ; n(a, #0:Fresh)) | -(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#2:UName, #3:Fresh))) ; e(seskey(a, b, n(#2:UName, #3:Fresh)), n(a, #0:Fresh)) ; n(b, #4:Fresh)), +(e(seskey(a, b, n(#2:UName, #3:Fresh)), n(b, #4:Fresh))), nil] & :: #3:Fresh :: [ nil | -(a ; n(a, #0:Fresh) ; b ; n(b, #1:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#2:UName, #3:Fresh)) ; n(b, #1:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#2:UName, #3:Fresh)))), nil] & :: #1:Fresh,#4:Fresh :: [ nil, -(a ; n(a, #0:Fresh)), +(a ; n(a, #0:Fresh) ; b ; n(b, #1:Fresh)) | -(e(mkey(b, s), seskey(a, b, n(#2:UName, #3:Fresh)) ; n(b, #1:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#2:UName, #3:Fresh)))), +(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#2:UName, #3:Fresh))) ; e(seskey(a, b, n(#2:UName, #3:Fresh)), n(a, #0:Fresh)) ; n(b, #4:Fresh)), -(e(seskey(a, b, n(#2:UName, #3:Fresh)), n(b, #4:Fresh))), nil] ) || e(seskey(a, b, n(#2:UName, #3:Fresh)), n(b, #4:Fresh)) !inI, (a ; n(a, #0:Fresh) ; b ; n(b, #1:Fresh)) !inI, (e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#2:UName, #3:Fresh))) ; e(seskey(a, b, n(#2:UName, #3:Fresh)), n(a, #0:Fresh)) ; n(b, #4:Fresh)) !inI, (e(mkey(b, s), seskey(a, b, n(#2:UName, #3:Fresh)) ; n(b, #1:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#2:UName, #3:Fresh)))) !inI, (n(a, #0:Fresh) ; b ; n(b, #1:Fresh)) inI, inst(#2:UName) || -(n(a, #0:Fresh) ; b ; n(b, #1:Fresh)), -(a), +(a ; n(a, #0:Fresh) ; b ; n(b, #1:Fresh)), -(a ; n(a, #0:Fresh) ; b ; n(b, #1:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#2:UName, #3:Fresh)) ; n(b, #1:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#2:UName, #3:Fresh)))), -(e(mkey(b, s), seskey(a, b, n(#2:UName, #3:Fresh)) ; n(b, #1:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#2:UName, #3:Fresh)))), +(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#2:UName, #3:Fresh))) ; e(seskey(a, b, n(#2:UName, #3:Fresh)), n(a, #0:Fresh)) ; n(b, #4:Fresh)), -(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#2:UName, #3:Fresh))) ; e(seskey(a, b, n(#2:UName, #3:Fresh)), n(a, #0:Fresh)) ; n(b, #4:Fresh)), +(e(seskey(a, b, n(#2:UName, #3:Fresh)), n(b, #4:Fresh))), -(e(seskey(a, b, n(#2:UName, #3:Fresh)), n(b, #4:Fresh))) || nil || nil ========================================== reduce in MAUDE-NPA : run(5) . rewrites: 18 in 0ms cpu (0ms real) (162162 rewrites/second) result IdSystemSet: (< 1 . 1 . 2 . 8 . 5 . 3 > ( :: nil :: [ nil | -(#7:Sessionkey), -(n(b, #2:Fresh)), +(e(#7:Sessionkey, n(b, #2:Fresh))), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, #1:Msg ; n(b, #2:Fresh) ; #3:Msg)), +(#1:Msg ; n(b, #2:Fresh) ; #3:Msg), nil] & :: nil :: [ nil | -(#1:Msg ; n(b, #2:Fresh) ; #3:Msg), +(n(b, #2:Fresh) ; #3:Msg), nil] & :: nil :: [ nil | -(n(b, #2:Fresh) ; #3:Msg), +(n(b, #2:Fresh)), nil] & :: nil :: [ nil | -(e(#0:Key, #1:Msg ; n(b, #2:Fresh) ; #3:Msg) ; #4:Msg), +(e(#0:Key, #1:Msg ; n(b, #2:Fresh) ; #3:Msg)), nil] & :: #2:Fresh,#5:Fresh :: [ nil, -(a ; #6:Nonce), +(a ; #6:Nonce ; b ; n(b, #5:Fresh)), -(e(mkey(b, s), #7:Sessionkey ; n(b, #5:Fresh) ; a) ; #8:Msg), +(#8:Msg ; e(#7:Sessionkey, #6:Nonce) ; n(b, #2:Fresh)) | -(e(#7:Sessionkey, n(b, #2:Fresh))), nil] ) || n(b, #2:Fresh) !inI, e(#7:Sessionkey, n(b, #2:Fresh)) !inI, e(#0:Key, #1:Msg ; n(b, #2:Fresh) ; #3:Msg) !inI, (#1:Msg ; n(b, #2:Fresh) ; #3:Msg) !inI, (n(b, #2:Fresh) ; #3:Msg) !inI, (e(#0:Key, #1:Msg ; n(b, #2:Fresh) ; #3:Msg) ; #4:Msg) inI || -(e(#0:Key, #1:Msg ; n(b, #2:Fresh) ; #3:Msg) ; #4:Msg), +(e(#0:Key, #1:Msg ; n(b, #2:Fresh) ; #3:Msg)), -(#0:Key), -(e(#0:Key, #1:Msg ; n(b, #2:Fresh) ; #3:Msg)), +(#1:Msg ; n(b, #2:Fresh) ; #3:Msg), -(#1:Msg ; n(b, #2:Fresh) ; #3:Msg), +(n(b, #2:Fresh) ; #3:Msg), -(n(b, #2:Fresh) ; #3:Msg), +(n(b, #2:Fresh)), -(#7:Sessionkey), -(n(b, #2:Fresh)), +(e(#7:Sessionkey, n(b, #2:Fresh))), -(e(#7:Sessionkey, n(b, #2:Fresh))) || ghost( #0:Key, :: nil :: [ nil | -(#7:Sessionkey), -(n(b, #2:Fresh)), +(e(#7:Sessionkey, n(b, #2:Fresh))), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, #1:Msg ; n(b, #2:Fresh) ; #3:Msg)), +(#1:Msg ; n(b, #2:Fresh) ; #3:Msg), nil] & :: nil :: [ nil | -(#1:Msg ; n(b, #2:Fresh) ; #3:Msg), +(n(b, #2:Fresh) ; #3:Msg), nil] & :: nil :: [ nil | -(n(b, #2:Fresh) ; #3:Msg), +(n(b, #2:Fresh)), nil] & :: #2:Fresh,#5:Fresh :: [ nil, -(a ; #6:Nonce), +(a ; #6:Nonce ; b ; n(b, #5:Fresh)), -(e(mkey(b, s), #7:Sessionkey ; n(b, #5:Fresh) ; a) ; #8:Msg), +(#8:Msg ; e(#7:Sessionkey, #6:Nonce) ; n(b, #2:Fresh)) | -(e(#7:Sessionkey, n(b, #2:Fresh))), nil] , n(b, #2:Fresh) !inI, e(#7:Sessionkey, n(b, #2:Fresh)) !inI, (#1:Msg ; n(b, #2:Fresh) ; #3:Msg) !inI, (n(b, #2:Fresh) ; #3:Msg) !inI, e(#0:Key, #1:Msg ; n(b, #2:Fresh) ; #3:Msg) inI, -(#0:Key), -(e(#0:Key, #1:Msg ; n(b, #2:Fresh) ; #3:Msg)), +(#1:Msg ; n(b, #2:Fresh) ; #3:Msg), -(#1:Msg ; n(b, #2:Fresh) ; #3:Msg), +(n(b, #2:Fresh) ; #3:Msg), -(n(b, #2:Fresh) ; #3:Msg), +(n(b, #2:Fresh)), -(#7:Sessionkey), -(n(b, #2:Fresh)), +(e(#7:Sessionkey, n(b, #2:Fresh))), -(e(#7:Sessionkey, n(b, #2:Fresh))), nil ), ghost( #7:Sessionkey, :: nil :: [ nil | -(#7:Sessionkey), -(n(b, #2:Fresh)), +(e(#7:Sessionkey, n(b, #2:Fresh))), nil] & :: #2:Fresh,#5:Fresh :: [ nil, -(a ; #6:Nonce), +(a ; #6:Nonce ; b ; n(b, #5:Fresh)), -(e(mkey(b, s), #7:Sessionkey ; n(b, #5:Fresh) ; a) ; #8:Msg), +(#8:Msg ; e(#7:Sessionkey, #6:Nonce) ; n(b, #2:Fresh)) | -(e(#7:Sessionkey, n(b, #2:Fresh))), nil] , e(#7:Sessionkey, n(b, #2:Fresh)) !inI, n(b, #2:Fresh) inI, -(#7:Sessionkey), -(n(b, #2:Fresh)), +(e(#7:Sessionkey, n(b, #2:Fresh))), -(e(#7:Sessionkey, n(b, #2:Fresh))), nil ) || nil) (< 1 . 1 . 3 . 4 . 8 . 3 > ( :: nil :: [ nil | -(#3:Sessionkey), -(n(b, #0:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh))), nil] & :: nil :: [ nil | -(#9:Sessionkey), -(e(#9:Sessionkey, n(b, #0:Fresh))), +(n(b, #0:Fresh)), nil] & :: nil :: [ nil | -(#10:Msg ; e(#9:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), +(e(#9:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), nil] & :: nil :: [ nil | -(e(#9:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), +(e(#9:Sessionkey, n(b, #0:Fresh))), nil] & :: #0:Fresh,#1:Fresh :: [ nil, -(a ; #2:Nonce), +(a ; #2:Nonce ; b ; n(b, #1:Fresh)), -(e(mkey(b, s), #3:Sessionkey ; n(b, #1:Fresh) ; a) ; #4:Msg), +(#4:Msg ; e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)) | -(e(#3:Sessionkey, n(b, #0:Fresh))), nil] & :: #5:Fresh,#6:Fresh :: [ nil, -(#7:UName ; n(b, #0:Fresh)), +(#7:UName ; n(b, #0:Fresh) ; #8:UName ; n(#8:UName, #6:Fresh)) | -(e(mkey(s, #8:UName), #9:Sessionkey ; n(#8:UName, #6:Fresh) ; #7:UName) ; #10:Msg), +(#10:Msg ; e(#9:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), nil] ) || n(b, #0:Fresh) !inI, e(#3:Sessionkey, n(b, #0:Fresh)) !inI, e(#9:Sessionkey, n(b, #0:Fresh)) !inI, (#10:Msg ; e(#9:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)) !inI, (e(#9:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)) !inI, (e(mkey(s, #8:UName), #9:Sessionkey ; n(#8:UName, #6:Fresh) ; #7:UName) ; #10:Msg) inI, inst(#9:Sessionkey) || -(e(mkey(s, #8:UName), #9:Sessionkey ; n(#8:UName, #6:Fresh) ; #7:UName) ; #10:Msg), +(#10:Msg ; e(#9:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), -(#10:Msg ; e(#9:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), +(e(#9:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), -(e(#9:Sessionkey, n(b, #0:Fresh)) ; n(#8:UName, #5:Fresh)), +(e(#9:Sessionkey, n(b, #0:Fresh))), -(#9:Sessionkey), -(e(#9:Sessionkey, n(b, #0:Fresh))), +(n(b, #0:Fresh)), -(#3:Sessionkey), -(n(b, #0:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh))), -(e(#3:Sessionkey, n(b, #0:Fresh))) || ghost( #9:Sessionkey, :: nil :: [ nil | -(#3:Sessionkey), -(n(b, #0:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh))), nil] & :: nil :: [ nil | -(#9:Sessionkey), -(e(#9:Sessionkey, n(b, #0:Fresh))), +(n(b, #0:Fresh)), nil] & :: #0:Fresh,#1:Fresh :: [ nil, -(a ; #2:Nonce), +(a ; #2:Nonce ; b ; n(b, #1:Fresh)), -(e(mkey(b, s), #3:Sessionkey ; n(b, #1:Fresh) ; a) ; #4:Msg), +(#4:Msg ; e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)) | -(e(#3:Sessionkey, n(b, #0:Fresh))), nil] , n(b, #0:Fresh) !inI, e(#3:Sessionkey, n(b, #0:Fresh)) !inI, e(#9:Sessionkey, n(b, #0:Fresh)) inI, -(#9:Sessionkey), -(e(#9:Sessionkey, n(b, #0:Fresh))), +(n(b, #0:Fresh)), -(#3:Sessionkey), -(n(b, #0:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh))), -(e(#3:Sessionkey, n(b, #0:Fresh))), nil ), ghost( #3:Sessionkey, :: nil :: [ nil | -(#3:Sessionkey), -(n(b, #0:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh))), nil] & :: #0:Fresh,#1:Fresh :: [ nil, -(a ; #2:Nonce), +(a ; #2:Nonce ; b ; n(b, #1:Fresh)), -(e(mkey(b, s), #3:Sessionkey ; n(b, #1:Fresh) ; a) ; #4:Msg), +(#4:Msg ; e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)) | -(e(#3:Sessionkey, n(b, #0:Fresh))), nil] , e(#3:Sessionkey, n(b, #0:Fresh)) !inI, n(b, #0:Fresh) inI, -(#3:Sessionkey), -(n(b, #0:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh))), -(e(#3:Sessionkey, n(b, #0:Fresh))), nil ) || nil) (< 1 . 1 . 5 . 7 . 1 . 2 > ( :: nil :: [ nil | -(#0:Msg), -(e(mkey(b, s), #1:Sessionkey ; n(b, #2:Fresh) ; a)), +(e(mkey(b, s), #1:Sessionkey ; n(b, #2:Fresh) ; a) ; #0:Msg), nil] & :: nil :: [ nil | -(#1:Sessionkey), -(n(b, #3:Fresh)), +(e(#1:Sessionkey, n(b, #3:Fresh))), nil] & :: nil :: [ nil | -(#0:Msg ; e(#1:Sessionkey, #4:Nonce) ; n(b, #3:Fresh)), +(e(#1:Sessionkey, #4:Nonce) ; n(b, #3:Fresh)), nil] & :: nil :: [ nil | -(e(#1:Sessionkey, #4:Nonce) ; n(b, #3:Fresh)), +(n(b, #3:Fresh)), nil] & :: #2:Fresh,#3:Fresh :: [ nil, -(a ; #4:Nonce), +(a ; #4:Nonce ; b ; n(b, #2:Fresh)) | -(e(mkey(b, s), #1:Sessionkey ; n(b, #2:Fresh) ; a) ; #0:Msg), +(#0:Msg ; e(#1:Sessionkey, #4:Nonce) ; n(b, #3:Fresh)), -(e(#1:Sessionkey, n(b, #3:Fresh))), nil] ) || #0:Msg !inI, n(b, #3:Fresh) !inI, e(#1:Sessionkey, n(b, #3:Fresh)) !inI, (#0:Msg ; e(#1:Sessionkey, #4:Nonce) ; n(b, #3:Fresh)) !inI, (e(#1:Sessionkey, #4:Nonce) ; n(b, #3:Fresh)) !inI, (e(mkey(b, s), #1:Sessionkey ; n(b, #2:Fresh) ; a) ; #0:Msg) !inI, e(mkey(b, s), #1:Sessionkey ; n(b, #2:Fresh) ; a) inI || generatedByIntruder(#0:Msg), -(#0:Msg), -(e(mkey(b, s), #1:Sessionkey ; n(b, #2:Fresh) ; a)), +(e(mkey(b, s), #1:Sessionkey ; n(b, #2:Fresh) ; a) ; #0:Msg), -(e(mkey(b, s), #1:Sessionkey ; n(b, #2:Fresh) ; a) ; #0:Msg), +(#0:Msg ; e(#1:Sessionkey, #4:Nonce) ; n(b, #3:Fresh)), -(#0:Msg ; e(#1:Sessionkey, #4:Nonce) ; n(b, #3:Fresh)), +(e(#1:Sessionkey, #4:Nonce) ; n(b, #3:Fresh)), -(e(#1:Sessionkey, #4:Nonce) ; n(b, #3:Fresh)), +(n(b, #3:Fresh)), -(#1:Sessionkey), -(n(b, #3:Fresh)), +(e(#1:Sessionkey, n(b, #3:Fresh))), -(e(#1:Sessionkey, n(b, #3:Fresh))) || ghost( #1:Sessionkey, :: nil :: [ nil | -(#1:Sessionkey), -(n(b, #3:Fresh)), +(e(#1:Sessionkey, n(b, #3:Fresh))), nil] & :: #2:Fresh,#3:Fresh :: [ nil, -(a ; #4:Nonce), +(a ; #4:Nonce ; b ; n(b, #2:Fresh)), -(e(mkey(b, s), #1:Sessionkey ; n(b, #2:Fresh) ; a) ; #0:Msg), +(#0:Msg ; e(#1:Sessionkey, #4:Nonce) ; n(b, #3:Fresh)) | -(e(#1:Sessionkey, n(b, #3:Fresh))), nil] , e(#1:Sessionkey, n(b, #3:Fresh)) !inI, n(b, #3:Fresh) inI, -(#1:Sessionkey), -(n(b, #3:Fresh)), +(e(#1:Sessionkey, n(b, #3:Fresh))), -(e(#1:Sessionkey, n(b, #3:Fresh))), nil ) || nil) (< 1 . 1 . 5 . 7 . 1 . 7 > ( :: nil :: [ nil | -(#3:Sessionkey), -(n(b, #0:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh))), nil] & :: nil :: [ nil | -(e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)), +(n(b, #0:Fresh)), nil] & :: nil :: [ nil | -((e(#4:Sessionkey, #5:Nonce) ; n(#6:UName, #7:Fresh)) ; e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)), +(e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)), nil] & :: #0:Fresh,#1:Fresh :: [ nil, -(a ; #2:Nonce), +(a ; #2:Nonce ; b ; n(b, #1:Fresh)) | -(e(mkey(b, s), #3:Sessionkey ; n(b, #1:Fresh) ; a) ; e(#4:Sessionkey, #5:Nonce) ; n(#6:UName, #7:Fresh)), +((e(#4:Sessionkey, #5:Nonce) ; n(#6:UName, #7:Fresh)) ; e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)), -(e(#3:Sessionkey, n(b, #0:Fresh))), nil] & :: #7:Fresh,#8:Fresh :: [ nil, -(#9:UName ; #5:Nonce), +(#9:UName ; #5:Nonce ; #6:UName ; n(#6:UName, #8:Fresh)) | -(e(mkey(s, #6:UName), #4:Sessionkey ; n(#6:UName, #8:Fresh) ; #9:UName) ; e(mkey(b, s), #3:Sessionkey ; n(b, #1:Fresh) ; a)), +(e(mkey(b, s), #3:Sessionkey ; n(b, #1:Fresh) ; a) ; e(#4:Sessionkey, #5:Nonce) ; n(#6:UName, #7:Fresh)), nil] ) || n(b, #0:Fresh) !inI, e(#3:Sessionkey, n(b, #0:Fresh)) !inI, (e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)) !inI, (e(mkey(b, s), #3:Sessionkey ; n(b, #1:Fresh) ; a) ; e(#4:Sessionkey, #5:Nonce) ; n(#6:UName, #7:Fresh)) !inI, ((e(#4:Sessionkey, #5:Nonce) ; n(#6:UName, #7:Fresh)) ; e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)) !inI, (e(mkey(s, #6:UName), #4:Sessionkey ; n(#6:UName, #8:Fresh) ; #9:UName) ; e(mkey(b, s), #3:Sessionkey ; n(b, #1:Fresh) ; a)) inI || -(e(mkey(s, #6:UName), #4:Sessionkey ; n(#6:UName, #8:Fresh) ; #9:UName) ; e(mkey(b, s), #3:Sessionkey ; n(b, #1:Fresh) ; a)), +(e(mkey(b, s), #3:Sessionkey ; n(b, #1:Fresh) ; a) ; e(#4:Sessionkey, #5:Nonce) ; n(#6:UName, #7:Fresh)), -(e(mkey(b, s), #3:Sessionkey ; n(b, #1:Fresh) ; a) ; e(#4:Sessionkey, #5:Nonce) ; n(#6:UName, #7:Fresh)), +((e(#4:Sessionkey, #5:Nonce) ; n(#6:UName, #7:Fresh)) ; e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)), -((e(#4:Sessionkey, #5:Nonce) ; n(#6:UName, #7:Fresh)) ; e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)), +(e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)), -(e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)), +(n(b, #0:Fresh)), -(#3:Sessionkey), -(n(b, #0:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh))), -(e(#3:Sessionkey, n(b, #0:Fresh))) || ghost( #3:Sessionkey, :: nil :: [ nil | -(#3:Sessionkey), -(n(b, #0:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh))), nil] & :: #0:Fresh,#1:Fresh :: [ nil, -(a ; #2:Nonce), +(a ; #2:Nonce ; b ; n(b, #1:Fresh)), -(e(mkey(b, s), #3:Sessionkey ; n(b, #1:Fresh) ; a) ; e(#4:Sessionkey, #5:Nonce) ; n(#6:UName, #7:Fresh)), +((e(#4:Sessionkey, #5:Nonce) ; n(#6:UName, #7:Fresh)) ; e(#3:Sessionkey, #2:Nonce) ; n(b, #0:Fresh)) | -(e(#3:Sessionkey, n(b, #0:Fresh))), nil] , e(#3:Sessionkey, n(b, #0:Fresh)) !inI, n(b, #0:Fresh) inI, -(#3:Sessionkey), -(n(b, #0:Fresh)), +(e(#3:Sessionkey, n(b, #0:Fresh))), -(e(#3:Sessionkey, n(b, #0:Fresh))), nil ) || nil) (< 1 . 5 . 6 . 1 . 2 . 3 > ( :: nil :: [ nil | -(#4:Msg), -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a)), +(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; #4:Msg), nil] & :: nil :: [ nil | -(#4:Msg ; e(#0:Sessionkey, n(b, #3:Fresh)) ; n(b, #3:Fresh)), +(e(#0:Sessionkey, n(b, #3:Fresh)) ; n(b, #3:Fresh)), nil] & :: nil :: [ nil | -(e(#0:Sessionkey, n(b, #3:Fresh)) ; n(b, #3:Fresh)), +(e(#0:Sessionkey, n(b, #3:Fresh))), nil] & :: nil :: [ nil | -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; #2:Msg), +(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a)), nil] & :: #1:Fresh,#3:Fresh :: [ nil, -(a ; n(b, #3:Fresh)), +(a ; n(b, #3:Fresh) ; b ; n(b, #1:Fresh)) | -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; #4:Msg), +(#4:Msg ; e(#0:Sessionkey, n(b, #3:Fresh)) ; n(b, #3:Fresh)), -(e(#0:Sessionkey, n(b, #3:Fresh))), nil] ) || #4:Msg !inI, e(#0:Sessionkey, n(b, #3:Fresh)) !inI, e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) !inI, (#4:Msg ; e(#0:Sessionkey, n(b, #3:Fresh)) ; n(b, #3:Fresh)) !inI, (e(#0:Sessionkey, n(b, #3:Fresh)) ; n(b, #3:Fresh)) !inI, (e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; #4:Msg) !inI, (e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; #2:Msg) inI || -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; #2:Msg), +(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a)), generatedByIntruder(#4:Msg), -(#4:Msg), -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a)), +(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; #4:Msg), -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; #4:Msg), +(#4:Msg ; e(#0:Sessionkey, n(b, #3:Fresh)) ; n(b, #3:Fresh)), -(#4:Msg ; e(#0:Sessionkey, n(b, #3:Fresh)) ; n(b, #3:Fresh)), +(e(#0:Sessionkey, n(b, #3:Fresh)) ; n(b, #3:Fresh)), -(e(#0:Sessionkey, n(b, #3:Fresh)) ; n(b, #3:Fresh)), +(e(#0:Sessionkey, n(b, #3:Fresh))), -(e(#0:Sessionkey, n(b, #3:Fresh))) || nil || nil) (< 1 . 5 . 6 . 1 . 8 . 6 > ( :: nil :: [ nil | -(#0:Nonce ; b ; n(b, #1:Fresh)), -(a), +(a ; #0:Nonce ; b ; n(b, #1:Fresh)), nil] & :: nil :: [ nil | -(e(mkey(a, s), #0:Nonce ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #2:Fresh)) ; n(b, #2:Fresh)), +(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #2:Fresh)) ; n(b, #2:Fresh)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #2:Fresh)) ; n(b, #2:Fresh)), +(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #2:Fresh))), nil] & :: #4:Fresh :: [ nil | -(a ; #0:Nonce ; b ; n(b, #1:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #1:Fresh) ; a) ; e(mkey(a, s), #0:Nonce ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))), nil] & :: #1:Fresh,#2:Fresh :: [ nil, -(a ; n(b, #2:Fresh)), +(a ; n(b, #2:Fresh) ; b ; n(b, #1:Fresh)) | -(e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #1:Fresh) ; a) ; e(mkey(a, s), #0:Nonce ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))), +(e(mkey(a, s), #0:Nonce ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #2:Fresh)) ; n(b, #2:Fresh)), -(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #2:Fresh))), nil] ) || e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #2:Fresh)) !inI, (a ; #0:Nonce ; b ; n(b, #1:Fresh)) !inI, (e(mkey(a, s), #0:Nonce ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #2:Fresh)) ; n(b, #2:Fresh)) !inI, (e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #1:Fresh) ; a) ; e(mkey(a, s), #0:Nonce ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))) !inI, (e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #2:Fresh)) ; n(b, #2:Fresh)) !inI, (#0:Nonce ; b ; n(b, #1:Fresh)) inI || -(#0:Nonce ; b ; n(b, #1:Fresh)), -(a), +(a ; #0:Nonce ; b ; n(b, #1:Fresh)), -(a ; #0:Nonce ; b ; n(b, #1:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #1:Fresh) ; a) ; e(mkey(a, s), #0:Nonce ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))), -(e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #1:Fresh) ; a) ; e(mkey(a, s), #0:Nonce ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))), +(e(mkey(a, s), #0:Nonce ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #2:Fresh)) ; n(b, #2:Fresh)), -(e(mkey(a, s), #0:Nonce ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #2:Fresh)) ; n(b, #2:Fresh)), +(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #2:Fresh)) ; n(b, #2:Fresh)), -(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #2:Fresh)) ; n(b, #2:Fresh)), +(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #2:Fresh))), -(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #2:Fresh))) || nil || nil) (< 1 . 5 . 6 . 8 . 4 . 3 > ( :: nil :: [ nil | -(#6:Msg), -(e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName)), +(e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName) ; #6:Msg), nil] & :: nil :: [ nil | -(mkey(s, #0:UName)), -(#1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName), +(e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName)), nil] & :: nil :: [ nil | -(#6:Msg ; e(#1:Sessionkey, n(b, #5:Fresh)) ; n(#0:UName, #4:Fresh)), +(e(#1:Sessionkey, n(b, #5:Fresh)) ; n(#0:UName, #4:Fresh)), nil] & :: nil :: [ nil | -(e(#1:Sessionkey, n(b, #5:Fresh)) ; n(#0:UName, #4:Fresh)), +(e(#1:Sessionkey, n(b, #5:Fresh))), nil] & :: #2:Fresh,#4:Fresh :: [ nil, -(#3:UName ; n(b, #5:Fresh)), +(#3:UName ; n(b, #5:Fresh) ; #0:UName ; n(#0:UName, #2:Fresh)) | -(e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName) ; #6:Msg), +(#6:Msg ; e(#1:Sessionkey, n(b, #5:Fresh)) ; n(#0:UName, #4:Fresh)), nil] & :: #5:Fresh,#7:Fresh :: [ nil, -(a ; #8:Nonce), +(a ; #8:Nonce ; b ; n(b, #7:Fresh)), -(e(mkey(b, s), #1:Sessionkey ; n(b, #7:Fresh) ; a) ; #9:Msg), +(#9:Msg ; e(#1:Sessionkey, #8:Nonce) ; n(b, #5:Fresh)) | -(e(#1:Sessionkey, n(b, #5:Fresh))), nil] ) || #6:Msg !inI, e(#1:Sessionkey, n(b, #5:Fresh)) !inI, e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName) !inI, (#6:Msg ; e(#1:Sessionkey, n(b, #5:Fresh)) ; n(#0:UName, #4:Fresh)) !inI, (e(#1:Sessionkey, n(b, #5:Fresh)) ; n(#0:UName, #4:Fresh)) !inI, (e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName) ; #6:Msg) !inI, mkey(s, #0:UName) inI, (#1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName) inI || -(mkey(s, #0:UName)), -(#1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName), +(e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName)), generatedByIntruder(#6:Msg), -(#6:Msg), -(e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName)), +(e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName) ; #6:Msg), -(e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName) ; #6:Msg), +(#6:Msg ; e(#1:Sessionkey, n(b, #5:Fresh)) ; n(#0:UName, #4:Fresh)), -(#6:Msg ; e(#1:Sessionkey, n(b, #5:Fresh)) ; n(#0:UName, #4:Fresh)), +(e(#1:Sessionkey, n(b, #5:Fresh)) ; n(#0:UName, #4:Fresh)), -(e(#1:Sessionkey, n(b, #5:Fresh)) ; n(#0:UName, #4:Fresh)), +(e(#1:Sessionkey, n(b, #5:Fresh))), -(e(#1:Sessionkey, n(b, #5:Fresh))) || nil || nil) (< 1 . 5 . 6 . 8 . 4 . 4 > ( :: nil :: [ nil | -(#7:Msg), -(e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName)), +(e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName) ; #7:Msg), nil] & :: nil :: [ nil | -(#7:Msg ; e(#1:Sessionkey, n(b, #6:Fresh)) ; n(#0:UName, #5:Fresh)), +(e(#1:Sessionkey, n(b, #6:Fresh)) ; n(#0:UName, #5:Fresh)), nil] & :: nil :: [ nil | -(e(#1:Sessionkey, n(b, #6:Fresh)) ; n(#0:UName, #5:Fresh)), +(e(#1:Sessionkey, n(b, #6:Fresh))), nil] & :: nil :: [ nil | -(e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName) ; #4:Msg), +(e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName)), nil] & :: #2:Fresh,#5:Fresh :: [ nil, -(#3:UName ; n(b, #6:Fresh)), +(#3:UName ; n(b, #6:Fresh) ; #0:UName ; n(#0:UName, #2:Fresh)) | -(e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName) ; #7:Msg), +(#7:Msg ; e(#1:Sessionkey, n(b, #6:Fresh)) ; n(#0:UName, #5:Fresh)), nil] & :: #6:Fresh,#8:Fresh :: [ nil, -(a ; #9:Nonce), +(a ; #9:Nonce ; b ; n(b, #8:Fresh)), -(e(mkey(b, s), #1:Sessionkey ; n(b, #8:Fresh) ; a) ; #10:Msg), +(#10:Msg ; e(#1:Sessionkey, #9:Nonce) ; n(b, #6:Fresh)) | -(e(#1:Sessionkey, n(b, #6:Fresh))), nil] ) || #7:Msg !inI, e(#1:Sessionkey, n(b, #6:Fresh)) !inI, e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName) !inI, (#7:Msg ; e(#1:Sessionkey, n(b, #6:Fresh)) ; n(#0:UName, #5:Fresh)) !inI, (e(#1:Sessionkey, n(b, #6:Fresh)) ; n(#0:UName, #5:Fresh)) !inI, (e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName) ; #7:Msg) !inI, (e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName) ; #4:Msg) inI || -(e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName) ; #4:Msg), +(e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName)), generatedByIntruder(#7:Msg), -(#7:Msg), -(e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName)), +(e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName) ; #7:Msg), -(e(mkey(s, #0:UName), #1:Sessionkey ; n(#0:UName, #2:Fresh) ; #3:UName) ; #7:Msg), +(#7:Msg ; e(#1:Sessionkey, n(b, #6:Fresh)) ; n(#0:UName, #5:Fresh)), -(#7:Msg ; e(#1:Sessionkey, n(b, #6:Fresh)) ; n(#0:UName, #5:Fresh)), +(e(#1:Sessionkey, n(b, #6:Fresh)) ; n(#0:UName, #5:Fresh)), -(e(#1:Sessionkey, n(b, #6:Fresh)) ; n(#0:UName, #5:Fresh)), +(e(#1:Sessionkey, n(b, #6:Fresh))), -(e(#1:Sessionkey, n(b, #6:Fresh))) || nil || nil) (< 1 . 6 . 3 . 5 . 8 . 16 > ( :: nil :: [ nil | -(mkey(s, #4:UName)), -(n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey), +(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), nil] & :: nil :: [ nil | -(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a)), +(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), nil] & :: nil :: [ nil | -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; #2:Msg), +(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a)), nil] & :: #3:Fresh :: [ nil, +(#4:UName ; n(#4:UName, #3:Fresh)) | -(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; e(#0:Sessionkey, n(#4:UName, #3:Fresh)) ; n(b, #6:Fresh)), +(e(#0:Sessionkey, n(b, #6:Fresh))), nil] & :: #1:Fresh,#6:Fresh :: [ nil, -(a ; n(#4:UName, #3:Fresh)), +(a ; n(#4:UName, #3:Fresh) ; b ; n(b, #1:Fresh)) | -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), +(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; e(#0:Sessionkey, n(#4:UName, #3:Fresh)) ; n(b, #6:Fresh)), -(e(#0:Sessionkey, n(b, #6:Fresh))), nil] ) || e(#0:Sessionkey, n(b, #6:Fresh)) !inI, e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) !inI, e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) !inI, (e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)) !inI, (e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; e(#0:Sessionkey, n(#4:UName, #3:Fresh)) ; n(b, #6:Fresh)) !inI, mkey(s, #4:UName) inI, (n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) inI, (e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; #2:Msg) inI, inst(#4:UName), inst(#5:UName), inst(#0:Sessionkey) || -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; #2:Msg), +(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a)), -(mkey(s, #4:UName)), -(n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey), +(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), -(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a)), +(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), +(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; e(#0:Sessionkey, n(#4:UName, #3:Fresh)) ; n(b, #6:Fresh)), -(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; e(#0:Sessionkey, n(#4:UName, #3:Fresh)) ; n(b, #6:Fresh)), +(e(#0:Sessionkey, n(b, #6:Fresh))), -(e(#0:Sessionkey, n(b, #6:Fresh))) || nil || nil) (< 1 . 6 . 3 . 5 . 9 . 12 > ( :: nil :: [ nil | -(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a)), +(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), nil] & :: nil :: [ nil | -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; #2:Msg), +(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a)), nil] & :: nil :: [ nil | -(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; #7:Msg), +(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), nil] & :: #3:Fresh :: [ nil, +(#4:UName ; n(#4:UName, #3:Fresh)) | -(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; e(#0:Sessionkey, n(#4:UName, #3:Fresh)) ; n(b, #6:Fresh)), +(e(#0:Sessionkey, n(b, #6:Fresh))), nil] & :: #1:Fresh,#6:Fresh :: [ nil, -(a ; n(#4:UName, #3:Fresh)), +(a ; n(#4:UName, #3:Fresh) ; b ; n(b, #1:Fresh)) | -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), +(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; e(#0:Sessionkey, n(#4:UName, #3:Fresh)) ; n(b, #6:Fresh)), -(e(#0:Sessionkey, n(b, #6:Fresh))), nil] ) || e(#0:Sessionkey, n(b, #6:Fresh)) !inI, e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) !inI, e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) !inI, (e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)) !inI, (e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; e(#0:Sessionkey, n(#4:UName, #3:Fresh)) ; n(b, #6:Fresh)) !inI, (e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; #2:Msg) inI, (e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; #7:Msg) inI, inst(#4:UName), inst(#5:UName), inst(#0:Sessionkey) || -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; #2:Msg), +(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a)), -(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; #7:Msg), +(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), -(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a)), +(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), +(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; e(#0:Sessionkey, n(#4:UName, #3:Fresh)) ; n(b, #6:Fresh)), -(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; e(#0:Sessionkey, n(#4:UName, #3:Fresh)) ; n(b, #6:Fresh)), +(e(#0:Sessionkey, n(b, #6:Fresh))), -(e(#0:Sessionkey, n(b, #6:Fresh))) || nil || nil) (< 1 . 6 . 3 . 5 . 10 . 12 > ( :: nil :: [ nil | -(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a)), +(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), nil] & :: nil :: [ nil | -(#7:Msg ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), +(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), nil] & :: nil :: [ nil | -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; #2:Msg), +(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a)), nil] & :: #3:Fresh :: [ nil, +(#4:UName ; n(#4:UName, #3:Fresh)) | -(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; e(#0:Sessionkey, n(#4:UName, #3:Fresh)) ; n(b, #6:Fresh)), +(e(#0:Sessionkey, n(b, #6:Fresh))), nil] & :: #1:Fresh,#6:Fresh :: [ nil, -(a ; n(#4:UName, #3:Fresh)), +(a ; n(#4:UName, #3:Fresh) ; b ; n(b, #1:Fresh)) | -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), +(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; e(#0:Sessionkey, n(#4:UName, #3:Fresh)) ; n(b, #6:Fresh)), -(e(#0:Sessionkey, n(b, #6:Fresh))), nil] ) || e(#0:Sessionkey, n(b, #6:Fresh)) !inI, e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) !inI, e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) !inI, (e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)) !inI, (e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; e(#0:Sessionkey, n(#4:UName, #3:Fresh)) ; n(b, #6:Fresh)) !inI, (#7:Msg ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)) inI, (e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; #2:Msg) inI, inst(#4:UName), inst(#5:UName), inst(#0:Sessionkey) || -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; #2:Msg), +(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a)), -(#7:Msg ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), +(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), -(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a)), +(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), -(e(mkey(b, s), #0:Sessionkey ; n(b, #1:Fresh) ; a) ; e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey)), +(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; e(#0:Sessionkey, n(#4:UName, #3:Fresh)) ; n(b, #6:Fresh)), -(e(mkey(s, #4:UName), n(#4:UName, #3:Fresh) ; #5:UName ; #0:Sessionkey) ; e(#0:Sessionkey, n(#4:UName, #3:Fresh)) ; n(b, #6:Fresh)), +(e(#0:Sessionkey, n(b, #6:Fresh))), -(e(#0:Sessionkey, n(b, #6:Fresh))) || nil || nil) (< 1 . 6 . 3 . 8 . 2 . 1 > ( :: #0:Fresh :: [ nil | +(a ; n(a, #0:Fresh)), -(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)), +(e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh))), nil] & :: #2:Fresh :: [ nil | -(a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))), nil] & :: #3:Fresh,#4:Fresh :: [ nil | -(a ; n(a, #0:Fresh)), +(a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))), +(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)), -(e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh))), nil] ) || e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh)) !inI, (a ; n(a, #0:Fresh)) !inI, (a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)) !inI, (e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)) !inI, (e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))) !inI, inst(#1:UName) || +(a ; n(a, #0:Fresh)), -(a ; n(a, #0:Fresh)), +(a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)), -(a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))), -(e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))), +(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)), -(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)), +(e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh))), -(e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh))) || nil || nil) (< 1 . 6 . 3 . 8 . 2 . 5 > ( :: nil :: [ nil | -(n(a, #0:Fresh)), -(a), +(a ; n(a, #0:Fresh)), nil] & :: #0:Fresh :: [ nil, +(a ; n(a, #0:Fresh)) | -(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)), +(e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh))), nil] & :: #2:Fresh :: [ nil | -(a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))), nil] & :: #3:Fresh,#4:Fresh :: [ nil | -(a ; n(a, #0:Fresh)), +(a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))), +(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)), -(e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh))), nil] ) || e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh)) !inI, (a ; n(a, #0:Fresh)) !inI, (a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)) !inI, (e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)) !inI, (e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))) !inI, n(a, #0:Fresh) inI, inst(#1:UName) || -(n(a, #0:Fresh)), -(a), +(a ; n(a, #0:Fresh)), -(a ; n(a, #0:Fresh)), +(a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)), -(a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))), -(e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))), +(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)), -(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)), +(e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh))), -(e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh))) || nil || nil) (< 1 . 6 . 3 . 8 . 2 . 6 > ( :: nil :: [ nil | -(#0:Msg ; a ; n(a, #1:Fresh)), +(a ; n(a, #1:Fresh)), nil] & :: #1:Fresh :: [ nil, +(a ; n(a, #1:Fresh)) | -(e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#2:UName, #3:Fresh))) ; e(seskey(a, b, n(#2:UName, #3:Fresh)), n(a, #1:Fresh)) ; n(b, #4:Fresh)), +(e(seskey(a, b, n(#2:UName, #3:Fresh)), n(b, #4:Fresh))), nil] & :: #3:Fresh :: [ nil | -(a ; n(a, #1:Fresh) ; b ; n(b, #5:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#2:UName, #3:Fresh)) ; n(b, #5:Fresh) ; a) ; e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#2:UName, #3:Fresh)))), nil] & :: #4:Fresh,#5:Fresh :: [ nil | -(a ; n(a, #1:Fresh)), +(a ; n(a, #1:Fresh) ; b ; n(b, #5:Fresh)), -(e(mkey(b, s), seskey(a, b, n(#2:UName, #3:Fresh)) ; n(b, #5:Fresh) ; a) ; e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#2:UName, #3:Fresh)))), +(e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#2:UName, #3:Fresh))) ; e(seskey(a, b, n(#2:UName, #3:Fresh)), n(a, #1:Fresh)) ; n(b, #4:Fresh)), -(e(seskey(a, b, n(#2:UName, #3:Fresh)), n(b, #4:Fresh))), nil] ) || e(seskey(a, b, n(#2:UName, #3:Fresh)), n(b, #4:Fresh)) !inI, (a ; n(a, #1:Fresh)) !inI, (a ; n(a, #1:Fresh) ; b ; n(b, #5:Fresh)) !inI, (e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#2:UName, #3:Fresh))) ; e(seskey(a, b, n(#2:UName, #3:Fresh)), n(a, #1:Fresh)) ; n(b, #4:Fresh)) !inI, (e(mkey(b, s), seskey(a, b, n(#2:UName, #3:Fresh)) ; n(b, #5:Fresh) ; a) ; e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#2:UName, #3:Fresh)))) !inI, (#0:Msg ; a ; n(a, #1:Fresh)) inI, inst(#2:UName) || -(#0:Msg ; a ; n(a, #1:Fresh)), +(a ; n(a, #1:Fresh)), -(a ; n(a, #1:Fresh)), +(a ; n(a, #1:Fresh) ; b ; n(b, #5:Fresh)), -(a ; n(a, #1:Fresh) ; b ; n(b, #5:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#2:UName, #3:Fresh)) ; n(b, #5:Fresh) ; a) ; e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#2:UName, #3:Fresh)))), -(e(mkey(b, s), seskey(a, b, n(#2:UName, #3:Fresh)) ; n(b, #5:Fresh) ; a) ; e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#2:UName, #3:Fresh)))), +(e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#2:UName, #3:Fresh))) ; e(seskey(a, b, n(#2:UName, #3:Fresh)), n(a, #1:Fresh)) ; n(b, #4:Fresh)), -(e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#2:UName, #3:Fresh))) ; e(seskey(a, b, n(#2:UName, #3:Fresh)), n(a, #1:Fresh)) ; n(b, #4:Fresh)), +(e(seskey(a, b, n(#2:UName, #3:Fresh)), n(b, #4:Fresh))), -(e(seskey(a, b, n(#2:UName, #3:Fresh)), n(b, #4:Fresh))) || nil || nil) (< 1 . 6 . 3 . 8 . 7 . 3 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, n(a, #1:Fresh) ; b ; n(b, #2:Fresh))), +(n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), nil] & :: nil :: [ nil | -(n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), -(a), +(a ; n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), nil] & :: #1:Fresh :: [ nil, +(a ; n(a, #1:Fresh)) | -(e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(a, #1:Fresh)) ; n(b, #5:Fresh)), +(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #5:Fresh))), nil] & :: #4:Fresh :: [ nil | -(a ; n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))), nil] & :: #2:Fresh,#5:Fresh :: [ nil, -(a ; n(a, #1:Fresh)), +(a ; n(a, #1:Fresh) ; b ; n(b, #2:Fresh)) | -(e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))), +(e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(a, #1:Fresh)) ; n(b, #5:Fresh)), -(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #5:Fresh))), nil] ) || e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #5:Fresh)) !inI, (a ; n(a, #1:Fresh) ; b ; n(b, #2:Fresh)) !inI, (n(a, #1:Fresh) ; b ; n(b, #2:Fresh)) !inI, (e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(a, #1:Fresh)) ; n(b, #5:Fresh)) !inI, (e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))) !inI, e(#0:Key, n(a, #1:Fresh) ; b ; n(b, #2:Fresh)) inI, inst(#3:UName) || -(#0:Key), -(e(#0:Key, n(a, #1:Fresh) ; b ; n(b, #2:Fresh))), +(n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), -(n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), -(a), +(a ; n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), -(a ; n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))), -(e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))), +(e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(a, #1:Fresh)) ; n(b, #5:Fresh)), -(e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(a, #1:Fresh)) ; n(b, #5:Fresh)), +(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #5:Fresh))), -(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #5:Fresh))) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, n(a, #1:Fresh) ; b ; n(b, #2:Fresh))), +(n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), nil] & :: nil :: [ nil | -(n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), -(a), +(a ; n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), nil] & :: #1:Fresh :: [ nil, +(a ; n(a, #1:Fresh)) | -(e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(a, #1:Fresh)) ; n(b, #5:Fresh)), +(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #5:Fresh))), nil] & :: #4:Fresh :: [ nil | -(a ; n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))), nil] & :: #2:Fresh,#5:Fresh :: [ nil, -(a ; n(a, #1:Fresh)), +(a ; n(a, #1:Fresh) ; b ; n(b, #2:Fresh)) | -(e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))), +(e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(a, #1:Fresh)) ; n(b, #5:Fresh)), -(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #5:Fresh))), nil] , e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #5:Fresh)) !inI, (a ; n(a, #1:Fresh) ; b ; n(b, #2:Fresh)) !inI, (n(a, #1:Fresh) ; b ; n(b, #2:Fresh)) !inI, (e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(a, #1:Fresh)) ; n(b, #5:Fresh)) !inI, (e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))) !inI, e(#0:Key, n(a, #1:Fresh) ; b ; n(b, #2:Fresh)) inI, inst(#3:UName), -(#0:Key), -(e(#0:Key, n(a, #1:Fresh) ; b ; n(b, #2:Fresh))), +(n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), -(n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), -(a), +(a ; n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), -(a ; n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))), -(e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))), +(e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(a, #1:Fresh)) ; n(b, #5:Fresh)), -(e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(a, #1:Fresh)) ; n(b, #5:Fresh)), +(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #5:Fresh))), -(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #5:Fresh))), nil ) || nil) (< 1 . 6 . 3 . 8 . 7 . 6 > ( :: nil :: [ nil | -(#0:Msg ; n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), +(n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), nil] & :: nil :: [ nil | -(n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), -(a), +(a ; n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), nil] & :: #1:Fresh :: [ nil, +(a ; n(a, #1:Fresh)) | -(e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(a, #1:Fresh)) ; n(b, #5:Fresh)), +(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #5:Fresh))), nil] & :: #4:Fresh :: [ nil | -(a ; n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))), nil] & :: #2:Fresh,#5:Fresh :: [ nil, -(a ; n(a, #1:Fresh)), +(a ; n(a, #1:Fresh) ; b ; n(b, #2:Fresh)) | -(e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))), +(e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(a, #1:Fresh)) ; n(b, #5:Fresh)), -(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #5:Fresh))), nil] ) || e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #5:Fresh)) !inI, (a ; n(a, #1:Fresh) ; b ; n(b, #2:Fresh)) !inI, (n(a, #1:Fresh) ; b ; n(b, #2:Fresh)) !inI, (e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(a, #1:Fresh)) ; n(b, #5:Fresh)) !inI, (e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))) !inI, (#0:Msg ; n(a, #1:Fresh) ; b ; n(b, #2:Fresh)) inI, inst(#3:UName) || -(#0:Msg ; n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), +(n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), -(n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), -(a), +(a ; n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), -(a ; n(a, #1:Fresh) ; b ; n(b, #2:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))), -(e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))), +(e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(a, #1:Fresh)) ; n(b, #5:Fresh)), -(e(mkey(a, s), n(a, #1:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(a, #1:Fresh)) ; n(b, #5:Fresh)), +(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #5:Fresh))), -(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #5:Fresh))) || nil || nil) (< 1 . 6 . 3 . 8 . 7 . 7 > ( :: nil :: [ nil | -(n(a, #0:Fresh) ; b ; n(b, #1:Fresh)), -(a), +(a ; n(a, #0:Fresh) ; b ; n(b, #1:Fresh)), nil] & :: nil :: [ nil | -((n(a, #0:Fresh) ; b ; n(b, #1:Fresh)) ; #2:Msg), +(n(a, #0:Fresh) ; b ; n(b, #1:Fresh)), nil] & :: #0:Fresh :: [ nil, +(a ; n(a, #0:Fresh)) | -(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(a, #0:Fresh)) ; n(b, #5:Fresh)), +(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #5:Fresh))), nil] & :: #4:Fresh :: [ nil | -(a ; n(a, #0:Fresh) ; b ; n(b, #1:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #1:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))), nil] & :: #1:Fresh,#5:Fresh :: [ nil, -(a ; n(a, #0:Fresh)), +(a ; n(a, #0:Fresh) ; b ; n(b, #1:Fresh)) | -(e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #1:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))), +(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(a, #0:Fresh)) ; n(b, #5:Fresh)), -(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #5:Fresh))), nil] ) || e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #5:Fresh)) !inI, (a ; n(a, #0:Fresh) ; b ; n(b, #1:Fresh)) !inI, (n(a, #0:Fresh) ; b ; n(b, #1:Fresh)) !inI, (e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(a, #0:Fresh)) ; n(b, #5:Fresh)) !inI, (e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #1:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))) !inI, ((n(a, #0:Fresh) ; b ; n(b, #1:Fresh)) ; #2:Msg) inI, inst(#3:UName) || -((n(a, #0:Fresh) ; b ; n(b, #1:Fresh)) ; #2:Msg), +(n(a, #0:Fresh) ; b ; n(b, #1:Fresh)), -(n(a, #0:Fresh) ; b ; n(b, #1:Fresh)), -(a), +(a ; n(a, #0:Fresh) ; b ; n(b, #1:Fresh)), -(a ; n(a, #0:Fresh) ; b ; n(b, #1:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #1:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))), -(e(mkey(b, s), seskey(a, b, n(#3:UName, #4:Fresh)) ; n(b, #1:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh)))), +(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(a, #0:Fresh)) ; n(b, #5:Fresh)), -(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#3:UName, #4:Fresh))) ; e(seskey(a, b, n(#3:UName, #4:Fresh)), n(a, #0:Fresh)) ; n(b, #5:Fresh)), +(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #5:Fresh))), -(e(seskey(a, b, n(#3:UName, #4:Fresh)), n(b, #5:Fresh))) || nil || nil) (< 1 . 1 . 2 . 6 . 6 . 7 . 0 > ( :: nil :: [ nil | -(#8:Sessionkey), -(n(b, #2:Fresh)), +(e(#8:Sessionkey, n(b, #2:Fresh))), nil] & :: nil :: [ nil | -(mkey(s, #1:UName)), -(e(mkey(s, #1:UName), n(b, #2:Fresh) ; #3:UName ; seskey(#1:UName, #3:UName, n(#5:UName, #0:Fresh)))), +(n(b, #2:Fresh) ; #3:UName ; seskey(#1:UName, #3:UName, n(#5:UName, #0:Fresh))), nil] & :: nil :: [ nil | -(n(b, #2:Fresh) ; #3:UName ; seskey(#1:UName, #3:UName, n(#5:UName, #0:Fresh))), +(n(b, #2:Fresh)), nil] & :: #0:Fresh :: [ nil, -(#1:UName ; n(b, #2:Fresh) ; #3:UName ; #4:Nonce), +(e(mkey(s, #3:UName), seskey(#1:UName, #3:UName, n(#5:UName, #0:Fresh)) ; #4:Nonce ; #1:UName) ; e(mkey(s, #1:UName), n(b, #2:Fresh) ; #3:UName ; seskey(#1:UName, #3:UName, n(#5:UName, #0:Fresh)))) | nil] & :: #2:Fresh,#6:Fresh :: [ nil, -(a ; #7:Nonce), +(a ; #7:Nonce ; b ; n(b, #6:Fresh)), -(e(mkey(b, s), #8:Sessionkey ; n(b, #6:Fresh) ; a) ; #9:Msg), +(#9:Msg ; e(#8:Sessionkey, #7:Nonce) ; n(b, #2:Fresh)) | -(e(#8:Sessionkey, n(b, #2:Fresh))), nil] ) || n(b, #2:Fresh) !inI, e(#8:Sessionkey, n(b, #2:Fresh)) !inI, (n(b, #2:Fresh) ; #3:UName ; seskey(#1:UName, #3:UName, n(#5:UName, #0:Fresh))) !inI, mkey(s, #1:UName) inI, e(mkey(s, #1:UName), n(b, #2:Fresh) ; #3:UName ; seskey(#1:UName, #3:UName, n(#5:UName, #0:Fresh))) inI || resuscitated(mkey(s, #1:UName)), -(mkey(s, #1:UName)), -(e(mkey(s, #1:UName), n(b, #2:Fresh) ; #3:UName ; seskey(#1:UName, #3:UName, n(#5:UName, #0:Fresh)))), +(n(b, #2:Fresh) ; #3:UName ; seskey(#1:UName, #3:UName, n(#5:UName, #0:Fresh))), -(n(b, #2:Fresh) ; #3:UName ; seskey(#1:UName, #3:UName, n(#5:UName, #0:Fresh))), +(n(b, #2:Fresh)), -(#8:Sessionkey), -(n(b, #2:Fresh)), +(e(#8:Sessionkey, n(b, #2:Fresh))), -(e(#8:Sessionkey, n(b, #2:Fresh))) || ghost( #8:Sessionkey, :: nil :: [ nil | -(#8:Sessionkey), -(n(b, #2:Fresh)), +(e(#8:Sessionkey, n(b, #2:Fresh))), nil] & :: #2:Fresh,#6:Fresh :: [ nil, -(a ; #7:Nonce), +(a ; #7:Nonce ; b ; n(b, #6:Fresh)), -(e(mkey(b, s), #8:Sessionkey ; n(b, #6:Fresh) ; a) ; #9:Msg), +(#9:Msg ; e(#8:Sessionkey, #7:Nonce) ; n(b, #2:Fresh)) | -(e(#8:Sessionkey, n(b, #2:Fresh))), nil] , e(#8:Sessionkey, n(b, #2:Fresh)) !inI, n(b, #2:Fresh) inI, -(#8:Sessionkey), -(n(b, #2:Fresh)), +(e(#8:Sessionkey, n(b, #2:Fresh))), -(e(#8:Sessionkey, n(b, #2:Fresh))), nil ) || nil) < 1 . 1 . 5 . 7 . 1 . 8 . 0 > ( :: nil :: [ nil | -(seskey(a, b, n(#3:UName, #0:Fresh))), -(n(b, #4:Fresh)), +(e(seskey(a, b, n(#3:UName, #0:Fresh)), n(b, #4:Fresh))), nil] & :: #0:Fresh :: [ nil, -(a ; #1:Nonce ; b ; n(b, #2:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#3:UName, #0:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), #1:Nonce ; b ; seskey(a, b, n(#3:UName, #0:Fresh)))) | nil] & :: #2:Fresh,#4:Fresh :: [ nil, -(a ; #5:Nonce), +(a ; #5:Nonce ; b ; n(b, #2:Fresh)), -(e(mkey(b, s), seskey(a, b, n(#3:UName, #0:Fresh)) ; n(b, #2:Fresh) ; a) ; e(mkey(a, s), #1:Nonce ; b ; seskey(a, b, n(#3:UName, #0:Fresh)))), +(e(mkey(a, s), #1:Nonce ; b ; seskey(a, b, n(#3:UName, #0:Fresh))) ; e(seskey(a, b, n(#3:UName, #0:Fresh)), #5:Nonce) ; n(b, #4:Fresh)) | -(e(seskey(a, b, n(#3:UName, #0:Fresh)), n(b, #4:Fresh))), nil] ) || e(seskey(a, b, n(#3:UName, #0:Fresh)), n(b, #4:Fresh)) !inI, n(b, #4:Fresh) inI, seskey(a, b, n(#3:UName, #0:Fresh)) inI || resuscitated(seskey(a, b, n(#3:UName, #0:Fresh))), -(seskey(a, b, n(#3:UName, #0:Fresh))), -(n(b, #4:Fresh)), +(e(seskey(a, b, n(#3:UName, #0:Fresh)), n(b, #4:Fresh))), -(e(seskey(a, b, n(#3:UName, #0:Fresh)), n(b, #4:Fresh))) || nil || nil ========================================== reduce in MAUDE-NPA : initials(5) . rewrites: 218 in 0ms cpu (0ms real) (~ rewrites/second) result IdSystem: < 1 . 6 . 3 . 8 . 2 . 1 > ( :: #0:Fresh :: [ nil | +(a ; n(a, #0:Fresh)), -(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)), +(e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh))), nil] & :: #2:Fresh :: [ nil | -(a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))), nil] & :: #3:Fresh,#4:Fresh :: [ nil | -(a ; n(a, #0:Fresh)), +(a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)), -(e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))), +(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)), -(e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh))), nil] ) || e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh)) !inI, (a ; n(a, #0:Fresh)) !inI, (a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)) !inI, (e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)) !inI, (e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))) !inI, inst(#1:UName) || +(a ; n(a, #0:Fresh)), -(a ; n(a, #0:Fresh)), +(a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)), -(a ; n(a, #0:Fresh) ; b ; n(b, #4:Fresh)), +(e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))), -(e(mkey(b, s), seskey(a, b, n(#1:UName, #2:Fresh)) ; n(b, #4:Fresh) ; a) ; e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh)))), +(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)), -(e(mkey(a, s), n(a, #0:Fresh) ; b ; seskey(a, b, n(#1:UName, #2:Fresh))) ; e(seskey(a, b, n(#1:UName, #2:Fresh)), n(a, #0:Fresh)) ; n(b, #3:Fresh)), +(e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh))), -(e(seskey(a, b, n(#1:UName, #2:Fresh)), n(b, #3:Fresh))) || nil || nil Maude> Bye. Wed Dec 5 10:23:40 CET 2012 Santiagos-MacBook-Pro:prototype-20121204 sescobar$