Santiagos-MacBook-Pro:prototype-20121204 sescobar$ examples/Wide_Mouthed_Frog-command Wed Dec 5 11:28:34 CET 2012 \||||||||||||||||||/ --- Welcome to Maude --- /||||||||||||||||||\ Maude alpha96b built: Nov 9 2012 18:20:01 Copyright 1997-2011 SRI International Wed Dec 5 11:28:34 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: 8298054 in 12078ms cpu (12203ms real) (686996 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 ; #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, (#0:Msg notLeq e(mkey(#1:UName, s), #2:UName ; seskey(#1:UName, #2:UName, n(#1:UName, #3:Fresh)))), (#0:Msg notLeq e(seskey(#4:UName, #5:UName, n(#4:UName, #6:Fresh)), #7:Nonce)), #0:Msg notLeq seskey(#8:UName, #9:UName, n(#8:UName, #10:Fresh)) => (#11: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:Key notInI, (#0:Key notLeq mkey(#1:UName, s)), #0:Key notLeq seskey(#2:UName, #3:UName, n(#2:UName, #4:Fresh)) => e(#0:Key, #5:Msg) inL .) | (errorNoHeuristicApplied { grl #0:Msg inL => (#1:Msg ; #0:Msg) inL ., '#0:Msg <- 'e['seskey['#2:UName,'#3:UName,'n['#2:UName,'#4:Fresh]],'#5:Nonce] ; '#1:Msg <- '#2:UName, grl e(seskey(#2:UName, #3:UName, n(#2:UName, #4:Fresh)), #5:Nonce) inL => emptyMsgSet inL .,none, grl #5:Nonce notInI, #5:Nonce notLeq #8:UName ; #9:Sessionkey => emptyMsgSet inL .} usingGrammar 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:UName ; #2:Sessionkey => e(#3:Key, #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) notLeq mkey(#3:UName, i) => mkey(#0:Name, #1:Name) inL .) | (errorInconsistentExceptionsInGrammarRule grl n(#0:Name, #1:Fresh) notLeq #5: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 #5: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 .) | ( grl empty => p(#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 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(#3:UName, #5:Fresh)) => seskey(#0:Name, #1:Name, #2:Nonce) inL . ========================================== reduce in MAUDE-NPA : run(0) . rewrites: 3177 in 29ms cpu (31ms real) (106948 rewrites/second) result IdSystem: < 1 > ( :: nil :: [ nil, -(e(mkey(b, s), a ; seskey(a, b, n(a, r:Fresh)))), -(a ; e(seskey(a, b, n(a, r:Fresh)), NMA:Nonce)) | nil] & :: r:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, r:Fresh)))), +(a ; e(seskey(a, b, n(a, r:Fresh)), NMA:Nonce)) | nil] ) || empty || nil || nil || nil ========================================== reduce in MAUDE-NPA : summary(1) . rewrites: 1413888 in 2795ms cpu (2812ms real) (505783 rewrites/second) result Summary: States>> 5 Solutions>> 0 ========================================== reduce in MAUDE-NPA : summary(2) . rewrites: 4886973 in 7442ms cpu (7482ms real) (656642 rewrites/second) result Summary: States>> 13 Solutions>> 0 ========================================== reduce in MAUDE-NPA : summary(3) . rewrites: 24106443 in 24428ms cpu (24522ms real) (986813 rewrites/second) result Summary: States>> 27 Solutions>> 1 ========================================== reduce in MAUDE-NPA : run(1) . rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second) result IdSystemSet: (< 1 . 1 > ( :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))) | +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] ) || (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) inI || +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) || nil || nil) (< 1 . 3 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, e(#0:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))) inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI || -(#0:Key), -(e(#0:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] , e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, e(#0:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))) inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI, -(#0:Key), -(e(#0:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil ) || nil) (< 1 . 4 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] ) || (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, e(#0:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) inI || -(#0:Key), -(e(#0:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] , (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, e(#0:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) inI, -(#0:Key), -(e(#0:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil ) || nil) (< 1 . 5 > ( :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) | nil] ) || (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) inI, e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce) inI || -(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) || nil || nil) < 1 . 6 > ( :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) | nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))) inI, (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) inI || -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) || nil || nil ========================================== reduce in MAUDE-NPA : run(2) . rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second) result IdSystemSet: (< 1 . 1 . 2 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) | +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, e(#0:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))) inI || -(#0:Key), -(e(#0:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) | +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] , e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, e(#0:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))) inI, -(#0:Key), -(e(#0:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil ) || nil) (< 1 . 1 . 3 > ( :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))) | +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) !inI, (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))) inI || -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) || nil || nil) (< 1 . 3 . 3 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))))), +(e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: #2:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) | nil] ) || e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))) !inI, e(#0:Key, e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))) inI, (a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) inI || -(#0:Key), -(e(#0:Key, e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))))), +(e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), -(#1:Key), -(e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))))), +(e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: #2:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) | nil] , e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))) !inI, e(#0:Key, e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))) inI, (a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) inI, -(#0:Key), -(e(#0:Key, e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))))), +(e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), -(#1:Key), -(e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil ), ghost( #1:Key, :: nil :: [ nil | -(#1:Key), -(e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: #2:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) | nil] , e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))) !inI, e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))) inI, (a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) inI, -(#1:Key), -(e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil ) || nil) (< 1 . 3 . 5 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, e(#0:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI, e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))) inI || -(#0:Key), -(e(#0:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] , e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, e(#0:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI, e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))) inI, -(#0:Key), -(e(#0:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil ), ghost( #3:Key, :: nil :: [ nil | -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] , e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))) inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI, -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil ) || nil) (< 1 . 3 . 9 > ( :: nil :: [ nil | -(#2:Key), -(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) | nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) !inI, (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))) inI, e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce) inI || -(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(#2:Key), -(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) || ghost( #2:Key, :: nil :: [ nil | -(#2:Key), -(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) | nil] , e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) !inI, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))) inI, (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) inI, -(#2:Key), -(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil ) || nil) (< 1 . 4 . 2 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)))), +(e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: #2:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) | nil] ) || e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, (a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, e(#0:Key, e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))) inI || -(#0:Key), -(e(#0:Key, e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)))), +(e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), -(#1:Key), -(e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)))), +(e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: #2:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) | nil] , e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, (a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, e(#0:Key, e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))) inI, -(#0:Key), -(e(#0:Key, e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)))), +(e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), -(#1:Key), -(e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil ), ghost( #1:Key, :: nil :: [ nil | -(#1:Key), -(e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: #2:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) | nil] , (a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))) inI, -(#1:Key), -(e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil ) || nil) (< 1 . 4 . 7 > ( :: nil :: [ nil | -(#2:Key), -(e(#2:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) | nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) !inI, (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI, e(#2:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))) inI || -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(#2:Key), -(e(#2:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) || ghost( #2:Key, :: nil :: [ nil | -(#2:Key), -(e(#2:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) | nil] , (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI, e(#2:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) inI, -(#2:Key), -(e(#2:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil ) || nil) (< 1 . 5 . 2 > ( :: nil :: [ nil | -(#0:Nonce), -(seskey(a, b, n(a, #1:Fresh))), +(e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)) | nil] ) || #0:Nonce !inI, e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) inI, seskey(a, b, n(a, #1:Fresh)) inI || generatedByIntruder(#0:Nonce), -(#0:Nonce), -(seskey(a, b, n(a, #1:Fresh))), +(e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)), -(e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)) || nil || nil) (< 1 . 5 . 4 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] ) || e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, e(#0:Key, e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) inI || -(#0:Key), -(e(#0:Key, e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] , e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, e(#0:Key, e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) inI, -(#0:Key), -(e(#0:Key, e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil ) || nil) (< 1 . 5 . 5 > ( :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) | nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) !inI, (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI, e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce) inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))) inI || -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) || nil || nil) (< 1 . 5 . 12 > ( :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(#0:Msg ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), +(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] ) || e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) inI, (#0:Msg ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI || -(#0:Msg ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), +(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) || nil || nil) (< 1 . 6 . 3 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) !inI, e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI || -(#0:Key), -(e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] , e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) !inI, e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI, -(#0:Key), -(e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil ) || nil) < 1 . 6 . 5 > ( :: nil :: [ nil | -(e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), -(a), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) | nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))) !inI, e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh))) inI, (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) inI || -(e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), -(a), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) || nil || nil ========================================== reduce in MAUDE-NPA : run(3) . rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second) result IdSystemSet: (< 1 . 1 . 2 . 2 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))))), +(e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: #2:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))) | +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] ) || e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))) !inI, (a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, e(#0:Key, e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))) inI || -(#0:Key), -(e(#0:Key, e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))))), +(e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), -(#1:Key), -(e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))))), +(e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: #2:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))) | +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] , e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))) !inI, (a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, e(#0:Key, e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))) inI, -(#0:Key), -(e(#0:Key, e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))))), +(e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), -(#1:Key), -(e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil ), ghost( #1:Key, :: nil :: [ nil | -(#1:Key), -(e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: #2:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))) | +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] , e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))) !inI, (a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))) inI, -(#1:Key), -(e(#1:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil ) || nil) (< 1 . 1 . 3 . 1 > ( :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: #0:Fresh :: [ nil | +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))) !inI, (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI || +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) || nil || nil) (< 1 . 1 . 3 . 3 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) | +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) inI || -(#0:Key), -(e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) | +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] , e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) inI, -(#0:Key), -(e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil ) || nil) (< 1 . 1 . 3 . 4 > ( :: nil :: [ nil | -(e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), -(a), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))) | +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))) !inI, (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI, e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh))) inI || -(e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), -(a), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) || nil || nil) (< 1 . 3 . 3 . 3 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(#1:Key, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))))))), +(e(#1:Key, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))))), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))))), +(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))))), nil] & :: nil :: [ nil | -(#2:Key), -(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), -(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), nil] & :: #3:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #3:Fresh)))), +(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) | nil] ) || e(#1:Key, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))))) !inI, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))) !inI, e(#0:Key, e(#1:Key, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))))) inI, (a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) inI || -(#0:Key), -(e(#0:Key, e(#1:Key, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))))))), +(e(#1:Key, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))))), -(#1:Key), -(e(#1:Key, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))))), +(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))))), -(#2:Key), -(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), -(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(#1:Key, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))))))), +(e(#1:Key, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))))), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))))), +(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))))), nil] & :: nil :: [ nil | -(#2:Key), -(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), -(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), nil] & :: #3:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #3:Fresh)))), +(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) | nil] , e(#1:Key, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))))) !inI, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))) !inI, e(#0:Key, e(#1:Key, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))))) inI, (a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) inI, -(#0:Key), -(e(#0:Key, e(#1:Key, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))))))), +(e(#1:Key, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))))), -(#1:Key), -(e(#1:Key, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))))), +(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))))), -(#2:Key), -(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), -(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), nil ), ghost( #1:Key, :: nil :: [ nil | -(#1:Key), -(e(#1:Key, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))))), +(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))))), nil] & :: nil :: [ nil | -(#2:Key), -(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), -(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), nil] & :: #3:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #3:Fresh)))), +(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) | nil] , e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))) !inI, e(#1:Key, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))))) inI, (a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) inI, -(#1:Key), -(e(#1:Key, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))))), +(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))))), -(#2:Key), -(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), -(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), nil ), ghost( #2:Key, :: nil :: [ nil | -(#2:Key), -(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), -(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), nil] & :: #3:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #3:Fresh)))), +(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) | nil] , e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))) !inI, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))) inI, (a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) inI, -(#2:Key), -(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), -(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), nil ) || nil) (< 1 . 3 . 3 . 6 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(#3:Key), -(e(#3:Key, e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))))), +(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), nil] & :: nil :: [ nil | -(#4:Key), -(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] ) || e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, e(#0:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI, e(#3:Key, e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))) inI || -(#0:Key), -(e(#0:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(#3:Key), -(e(#3:Key, e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))))), +(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), -(#4:Key), -(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(#3:Key), -(e(#3:Key, e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))))), +(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), nil] & :: nil :: [ nil | -(#4:Key), -(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] , e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, e(#0:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI, e(#3:Key, e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))) inI, -(#0:Key), -(e(#0:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(#3:Key), -(e(#3:Key, e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))))), +(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), -(#4:Key), -(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil ), ghost( #3:Key, :: nil :: [ nil | -(#3:Key), -(e(#3:Key, e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))))), +(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), nil] & :: nil :: [ nil | -(#4:Key), -(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] , e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, e(#3:Key, e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))) inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI, -(#3:Key), -(e(#3:Key, e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))))), +(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), -(#4:Key), -(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil ), ghost( #4:Key, :: nil :: [ nil | -(#4:Key), -(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] , e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))) inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI, -(#4:Key), -(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil ) || nil) (< 1 . 3 . 3 . 9 > ( :: nil :: [ nil | -(#2:Key), -(e(#2:Key, e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))))), +(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))))), nil] & :: nil :: [ nil | -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) | nil] ) || e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) !inI, (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI, e(#2:Key, e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))))) inI, e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce) inI || -(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(#2:Key), -(e(#2:Key, e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))))), +(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))))), -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) || ghost( #2:Key, :: nil :: [ nil | -(#2:Key), -(e(#2:Key, e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))))), +(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))))), nil] & :: nil :: [ nil | -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) | nil] , e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) !inI, e(#2:Key, e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))))) inI, (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) inI, -(#2:Key), -(e(#2:Key, e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))))), +(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))))), -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil ), ghost( #3:Key, :: nil :: [ nil | -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) | nil] , e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) !inI, e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))) inI, (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) inI, -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil ) || nil) (< 1 . 3 . 5 . 3 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)))), +(e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: nil :: [ nil | -(#4:Key), -(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: #2:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) | nil] ) || e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))) !inI, (a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, e(#0:Key, e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))) inI, e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))) inI || -(#0:Key), -(e(#0:Key, e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)))), +(e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), -(#1:Key), -(e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(#4:Key), -(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)))), +(e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: nil :: [ nil | -(#4:Key), -(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: #2:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) | nil] , e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))) !inI, (a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, e(#0:Key, e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))) inI, e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))) inI, -(#0:Key), -(e(#0:Key, e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)))), +(e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), -(#1:Key), -(e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(#4:Key), -(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil ), ghost( #1:Key, :: nil :: [ nil | -(#1:Key), -(e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: nil :: [ nil | -(#4:Key), -(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: #2:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) | nil] , e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))) !inI, (a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) inI, e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))) inI, -(#1:Key), -(e(#1:Key, a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(#4:Key), -(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil ), ghost( #4:Key, :: nil :: [ nil | -(#4:Key), -(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: #2:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) | nil] , e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))) !inI, e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))) inI, (a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) inI, -(#4:Key), -(e(#4:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil ) || nil) (< 1 . 3 . 9 . 2 > ( :: nil :: [ nil | -(#0:Nonce), -(seskey(a, b, n(a, #1:Fresh))), +(e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)), nil] & :: nil :: [ nil | -(#2:Key), -(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)) | nil] ) || #0:Nonce !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)) !inI, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))) inI, seskey(a, b, n(a, #1:Fresh)) inI || generatedByIntruder(#0:Nonce), -(#0:Nonce), -(seskey(a, b, n(a, #1:Fresh))), +(e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)), -(e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)), -(#2:Key), -(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)) || ghost( #2:Key, :: nil :: [ nil | -(#2:Key), -(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)) | nil] , e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))) inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)) inI, -(#2:Key), -(e(#2:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #0:Nonce)), nil ) || nil) (< 1 . 3 . 9 . 5 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, e(#0:Key, e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI, e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))) inI || -(#0:Key), -(e(#0:Key, e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] , e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, e(#0:Key, e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI, e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))) inI, -(#0:Key), -(e(#0:Key, e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil ), ghost( #3:Key, :: nil :: [ nil | -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] , e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))) inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI, -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil ) || nil) (< 1 . 3 . 9 . 11 > ( :: nil :: [ nil | -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(#0:Msg ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), +(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))) inI, (#0:Msg ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI || -(#0:Msg ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), +(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) || ghost( #3:Key, :: nil :: [ nil | -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] , e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))) inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI, -(#3:Key), -(e(#3:Key, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil ) || nil) (< 1 . 4 . 2 . 2 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(#1:Key, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce))))), +(e(#1:Key, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)))), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)))), +(e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce))), nil] & :: nil :: [ nil | -(#2:Key), -(e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce))), +(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), -(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), nil] & :: #3:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #3:Fresh)))), +(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) | nil] ) || e(#1:Key, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce))) !inI, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) !inI, (a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) !inI, e(#0:Key, e(#1:Key, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)))) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))) inI || -(#0:Key), -(e(#0:Key, e(#1:Key, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce))))), +(e(#1:Key, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)))), -(#1:Key), -(e(#1:Key, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)))), +(e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce))), -(#2:Key), -(e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce))), +(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), -(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(#1:Key, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce))))), +(e(#1:Key, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)))), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)))), +(e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce))), nil] & :: nil :: [ nil | -(#2:Key), -(e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce))), +(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), -(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), nil] & :: #3:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #3:Fresh)))), +(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) | nil] , e(#1:Key, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce))) !inI, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) !inI, (a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) !inI, e(#0:Key, e(#1:Key, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)))) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))) inI, -(#0:Key), -(e(#0:Key, e(#1:Key, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce))))), +(e(#1:Key, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)))), -(#1:Key), -(e(#1:Key, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)))), +(e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce))), -(#2:Key), -(e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce))), +(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), -(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), nil ), ghost( #1:Key, :: nil :: [ nil | -(#1:Key), -(e(#1:Key, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)))), +(e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce))), nil] & :: nil :: [ nil | -(#2:Key), -(e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce))), +(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), -(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), nil] & :: #3:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #3:Fresh)))), +(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) | nil] , e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) !inI, (a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) !inI, e(#1:Key, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce))) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))) inI, -(#1:Key), -(e(#1:Key, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)))), +(e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce))), -(#2:Key), -(e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce))), +(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), -(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), nil ), ghost( #2:Key, :: nil :: [ nil | -(#2:Key), -(e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce))), +(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), -(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), nil] & :: #3:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #3:Fresh)))), +(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) | nil] , (a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) !inI, e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh))) inI, -(#2:Key), -(e(#2:Key, a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce))), +(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #3:Fresh)))), -(a ; e(seskey(a, b, n(a, #3:Fresh)), #4:Nonce)), nil ) || nil) (< 1 . 4 . 2 . 8 > ( :: nil :: [ nil | -(#2:Key), -(e(#2:Key, e(#3:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)))), +(e(#3:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), nil] & :: nil :: [ nil | -(#3:Key), -(e(#3:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) | nil] ) || e(#3:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) !inI, (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI, e(#2:Key, e(#3:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))) inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))) inI || -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(#2:Key), -(e(#2:Key, e(#3:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)))), +(e(#3:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), -(#3:Key), -(e(#3:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) || ghost( #2:Key, :: nil :: [ nil | -(#2:Key), -(e(#2:Key, e(#3:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)))), +(e(#3:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), nil] & :: nil :: [ nil | -(#3:Key), -(e(#3:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) | nil] , e(#3:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI, (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI, e(#2:Key, e(#3:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) inI, -(#2:Key), -(e(#2:Key, e(#3:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)))), +(e(#3:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), -(#3:Key), -(e(#3:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil ), ghost( #3:Key, :: nil :: [ nil | -(#3:Key), -(e(#3:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) | nil] , (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI, e(#3:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) inI, -(#3:Key), -(e(#3:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil ) || nil) (< 1 . 4 . 7 . 3 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(#3:Key), -(e(#3:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) inI, e(#3:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI || -(#0:Key), -(e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(#3:Key), -(e(#3:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(#3:Key), -(e(#3:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] , e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) inI, e(#3:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI, -(#0:Key), -(e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(#3:Key), -(e(#3:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil ), ghost( #3:Key, :: nil :: [ nil | -(#3:Key), -(e(#3:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] , (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, e(#3:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) inI, -(#3:Key), -(e(#3:Key, a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil ) || nil) (< 1 . 4 . 7 . 7 > ( :: nil :: [ nil | -(#2:Key), -(e(#2:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), -(a), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) | nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))) !inI, (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI, e(#2:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) inI, e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh))) inI || -(e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), -(a), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(#2:Key), -(e(#2:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) || ghost( #2:Key, :: nil :: [ nil | -(#2:Key), -(e(#2:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) | nil] , (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI, e(#2:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) inI, -(#2:Key), -(e(#2:Key, a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil ) || nil) (< 1 . 5 . 2 . 2 > ( :: nil :: [ nil | -(#1:Nonce), -(seskey(a, b, n(a, #0:Fresh))), +(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) | nil] ) || #1:Nonce !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) !inI, e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce) !inI, (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))) inI, seskey(a, b, n(a, #0:Fresh)) inI || -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), generatedByIntruder(#1:Nonce), -(#1:Nonce), -(seskey(a, b, n(a, #0:Fresh))), +(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) || nil || nil) (< 1 . 5 . 2 . 7 > ( :: nil :: [ nil | -(#2:Nonce), -(seskey(a, b, n(a, #1:Fresh))), +(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, seskey(a, b, n(a, #1:Fresh)))), +(seskey(a, b, n(a, #1:Fresh))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] ) || #2:Nonce !inI, e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, seskey(a, b, n(a, #1:Fresh)) !inI, e(#0:Key, seskey(a, b, n(a, #1:Fresh))) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) inI || -(#0:Key), -(e(#0:Key, seskey(a, b, n(a, #1:Fresh)))), +(seskey(a, b, n(a, #1:Fresh))), generatedByIntruder(#2:Nonce), -(#2:Nonce), -(seskey(a, b, n(a, #1:Fresh))), +(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#2:Nonce), -(seskey(a, b, n(a, #1:Fresh))), +(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(#0:Key), -(e(#0:Key, seskey(a, b, n(a, #1:Fresh)))), +(seskey(a, b, n(a, #1:Fresh))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] , #2:Nonce !inI, e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, seskey(a, b, n(a, #1:Fresh)) !inI, e(#0:Key, seskey(a, b, n(a, #1:Fresh))) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) inI, -(#0:Key), -(e(#0:Key, seskey(a, b, n(a, #1:Fresh)))), +(seskey(a, b, n(a, #1:Fresh))), generatedByIntruder(#2:Nonce), -(#2:Nonce), -(seskey(a, b, n(a, #1:Fresh))), +(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil ) || nil) (< 1 . 5 . 2 . 11 > ( :: nil :: [ nil | -(#2:Nonce), -(seskey(a, b, n(a, #1:Fresh))), +(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(#0:Msg ; seskey(a, b, n(a, #1:Fresh))), +(seskey(a, b, n(a, #1:Fresh))), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] ) || #2:Nonce !inI, e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, seskey(a, b, n(a, #1:Fresh)) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) inI, (#0:Msg ; seskey(a, b, n(a, #1:Fresh))) inI || -(#0:Msg ; seskey(a, b, n(a, #1:Fresh))), +(seskey(a, b, n(a, #1:Fresh))), generatedByIntruder(#2:Nonce), -(#2:Nonce), -(seskey(a, b, n(a, #1:Fresh))), +(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) || nil || nil) (< 1 . 5 . 4 . 2 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(#1:Key, e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)))), +(e(#1:Key, e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: #2:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) | nil] ) || e(#1:Key, e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce) !inI, (a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, e(#0:Key, e(#1:Key, e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))) inI || -(#0:Key), -(e(#0:Key, e(#1:Key, e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)))), +(e(#1:Key, e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), -(#1:Key), -(e(#1:Key, e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(#1:Key, e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)))), +(e(#1:Key, e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: #2:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) | nil] , e(#1:Key, e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce) !inI, (a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, e(#0:Key, e(#1:Key, e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))) inI, -(#0:Key), -(e(#0:Key, e(#1:Key, e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)))), +(e(#1:Key, e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), -(#1:Key), -(e(#1:Key, e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil ), ghost( #1:Key, :: nil :: [ nil | -(#1:Key), -(e(#1:Key, e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: #2:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) | nil] , e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce) !inI, (a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, e(#1:Key, e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))) inI, -(#1:Key), -(e(#1:Key, e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil ) || nil) (< 1 . 5 . 4 . 8 > ( :: nil :: [ nil | -(#2:Key), -(e(#2:Key, e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), +(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) | nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) !inI, e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce) !inI, (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI, e(#2:Key, e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))) inI || -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(#2:Key), -(e(#2:Key, e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), +(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) || ghost( #2:Key, :: nil :: [ nil | -(#2:Key), -(e(#2:Key, e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), +(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) | nil] , e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce) !inI, (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI, e(#2:Key, e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) inI, -(#2:Key), -(e(#2:Key, e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce))), +(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil ) || nil) (< 1 . 5 . 5 . 4 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) inI, e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce) inI || -(#0:Key), -(e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] , e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) inI, e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce) inI, -(#0:Key), -(e(#0:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil ) || nil) (< 1 . 5 . 5 . 5 > ( :: nil :: [ nil | -(e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), -(a), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: #0:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) | nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))) !inI, (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI, e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh))) inI, e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce) inI || -(e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), -(a), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) || nil || nil) (< 1 . 5 . 5 . 11 > ( :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(#0:Msg ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), +(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) inI, (#0:Msg ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI || -(#0:Msg ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), +(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) || nil || nil) (< 1 . 5 . 12 . 4 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, #1:Msg ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(#1:Msg ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: nil :: [ nil | -(#1:Msg ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), +(e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: #2:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) | nil] ) || e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce) !inI, (a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, (#1:Msg ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, e(#0:Key, #1:Msg ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))) inI || -(#0:Key), -(e(#0:Key, #1:Msg ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(#1:Msg ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(#1:Msg ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), +(e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, #1:Msg ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(#1:Msg ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: nil :: [ nil | -(e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: nil :: [ nil | -(#1:Msg ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), +(e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: #2:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) | nil] , e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce) !inI, (a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, (#1:Msg ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) !inI, e(#0:Key, #1:Msg ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) inI, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))) inI, -(#0:Key), -(e(#0:Key, #1:Msg ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce))), +(#1:Msg ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(#1:Msg ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), +(e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(a), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil ) || nil) (< 1 . 6 . 3 . 3 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(#1:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))))), +(e(#1:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh))))), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), nil] & :: #2:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) | nil] ) || e(#1:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))) !inI, e(#0:Key, e(#1:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh))))) inI, (a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) inI || -(#0:Key), -(e(#0:Key, e(#1:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))))), +(e(#1:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh))))), -(#1:Key), -(e(#1:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(#1:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))))), +(e(#1:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh))))), nil] & :: nil :: [ nil | -(#1:Key), -(e(#1:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), nil] & :: #2:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) | nil] , e(#1:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))) !inI, e(#0:Key, e(#1:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh))))) inI, (a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) inI, -(#0:Key), -(e(#0:Key, e(#1:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))))), +(e(#1:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh))))), -(#1:Key), -(e(#1:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil ), ghost( #1:Key, :: nil :: [ nil | -(#1:Key), -(e(#1:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), nil] & :: #2:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) | nil] , e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh))) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))) !inI, e(#1:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))) inI, (a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)) inI, -(#1:Key), -(e(#1:Key, a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh))))), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #2:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #2:Fresh)))), -(a ; e(seskey(a, b, n(a, #2:Fresh)), #3:Nonce)), nil ) || nil) (< 1 . 6 . 5 . 3 > ( :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), -(a), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] ) || e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) !inI, e(#0:Key, e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI || -(#0:Key), -(e(#0:Key, e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), -(a), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) || ghost( #0:Key, :: nil :: [ nil | -(#0:Key), -(e(#0:Key, e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), -(a), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] , e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) !inI, e(#0:Key, e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI, -(#0:Key), -(e(#0:Key, e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))))), +(e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), -(a), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil ) || nil) < 1 . 6 . 5 . 13 > ( :: nil :: [ nil | -(e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), -(a), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: nil :: [ nil | -(#0:Msg ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), nil] & :: #1:Fresh :: [ nil, +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) | nil] ) || e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh))) !inI, e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh))) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) !inI, (a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) inI, (#0:Msg ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))) inI || -(#0:Msg ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), -(a), +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #1:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(e(mkey(b, s), a ; seskey(a, b, n(a, #1:Fresh)))), -(a ; e(seskey(a, b, n(a, #1:Fresh)), #2:Nonce)) || nil || nil ========================================== reduce in MAUDE-NPA : initials(3) . rewrites: 315 in 0ms cpu (0ms real) (~ rewrites/second) result IdSystem: < 1 . 1 . 3 . 1 > ( :: nil :: [ nil | -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] & :: nil :: [ nil | -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), nil] & :: #0:Fresh :: [ nil | +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), nil] ) || e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh))) !inI, (a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))) !inI, (a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) !inI || +(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(mkey(a, s), b ; seskey(a, b, n(a, #0:Fresh)))), +(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), +(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)), -(e(mkey(b, s), a ; seskey(a, b, n(a, #0:Fresh)))), -(a ; e(seskey(a, b, n(a, #0:Fresh)), #1:Nonce)) || nil || nil Maude> Bye. Wed Dec 5 11:29:22 CET 2012 Santiagos-MacBook-Pro:prototype-20121204 sescobar$