Santiagos-MacBook-Pro:prototype-20121204 sescobar$ examples/homo-hpc-command Wed Dec 5 10:46:32 CET 2012 \||||||||||||||||||/ --- Welcome to Maude --- /||||||||||||||||||\ Maude alpha96b built: Nov 9 2012 18:20:01 Copyright 1997-2011 SRI International Wed Dec 5 10:46:32 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: 37710292 in 57354ms cpu (57604ms real) (657494 rewrites/second) result GrammarList: ( grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; grl #0:Msg inL => pke(#0:Msg, i) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(i, #1:Name)) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(#1:Name, i)) inL . ; grl #0:Msg inL => sign(#0:Msg, #1:Name) inL . ; grl #0:Msg notInI, (#0:Msg notLeq n(#1:Name, #2:Fresh)), #0:Msg notLeq pke(hpke(data(#3:Name, #4:Fresh), pkey(#3:Name, #5:Name)), s) => (#0:Msg ; #6:Msg) inL .) | ( grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; grl #0:Msg inL => pke(#0:Msg, i) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(i, #1:Name)) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(#1:Name, i)) inL . ; grl #0:Msg inL => sign(#0:Msg, #1:Name) inL . ; grl #0:Msg notInI, (#0:Msg notLeq #1:Name ; #2:Nonce ; #3:Nonce ; f(#4:HEnc, #5:HEnc)), (#0:Msg notLeq #6:Name ; n(#7:Name, #8:Fresh) ; #9:Nonce ; pke(hpke(data(#7:Name, #10:Fresh), pkey(#7:Name, #6:Name)), s) ; #11:Enc), (#0:Msg notLeq #12:Nonce ; #13:Nonce ; f(#14:HEnc, #15:HEnc)), (#0:Msg notLeq #16:Nonce ; pke(hpke(data(#17:Name, #18:Fresh), pkey(#17:Name, #19:Name)), s) ; #20:Enc), (#0:Msg notLeq #21:Nonce ; f(#22:HEnc, #23:HEnc)), (#0:Msg notLeq n( #24:Name, #25:Fresh) ; pke(hpke(data(#24:Name, #26:Fresh), pkey(#24:Name, #27:Name)), s)), (#0:Msg notLeq n(#28:Name, #29:Fresh) ; #30:Nonce ; pke(hpke(data(#28:Name, #31:Fresh), pkey(#28:Name, #32:Name)), s) ; #33:Enc), (#0:Msg notLeq n(#34:Name, #35:Fresh) ; pke(hpke(data(#34:Name, #36:Fresh), pkey(#37:Name, #34:Name)), s)), (#0:Msg notLeq pke(hpke(data(#38:Name, #39:Fresh), pkey(#38:Name, #40:Name)), s) ; #41:Enc), (#0:Msg notLeq f(#42:HEnc, #43:HEnc)), (#0:Msg notLeq pke(hpke(data(#44:Name, #45:Fresh), pkey(#46:Name, #44:Name)), s)), #0:Msg notLeq pke(hpke(data(#47:Name, #48:Fresh), pkey(#47:Name, #49:Name)), s) => (#50: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 empty => data(#0:Name, #1:Fresh) inL . ; grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; grl #0:Msg inL => pke(#0:Msg, i) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(i, #1:Name)) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(#1:Name, i)) inL . ; grl #0:Msg inL => sign(#0:Msg, #1:Name) inL .) | ( grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; grl #0:Msg inL => pke(#0:Msg, i) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(i, #1:Name)) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(#1:Name, i)) inL . ; grl #0:Msg inL => sign(#0:Msg, #1:Name) inL . ; grl #0:Msg notInI, (#0:Msg notLeq hpke(data(#1:Name, #2:Fresh), pkey(#1:Name, #3:Name))), #0:Msg notLeq hpke(data(#4:Name, #5:Fresh), pkey(#6:Name, #4:Name)) => f(#0:Msg, #7:Msg) inL . ; grl #0:Msg notInI, (#0:Msg notLeq hpke(data(#1:Name, #2:Fresh), pkey(#1:Name, #3:Name))), #0:Msg notLeq hpke(data(#4:Name, #5:Fresh), pkey(#6:Name, #4:Name)) => pke(#0:Msg, s) inL .) | ( grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; grl #0:Msg inL => pke(#0:Msg, i) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(i, #1:Name)) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(#1:Name, i)) inL . ; grl #0:Msg inL => sign(#0:Msg, #1:Name) inL . ; grl #0:Msg notInI, (#0:Msg notLeq hpke(data(#1:Name, #2:Fresh), pkey(#1:Name, #3:Name))), #0:Msg notLeq hpke(data(#4:Name, #5:Fresh), pkey(#6:Name, #4:Name)) => f(#7:Msg, #0:Msg) inL . ; grl #0:Msg notInI, (#0:Msg notLeq hpke(data(#1:Name, #2:Fresh), pkey(#1:Name, #3:Name))), #0:Msg notLeq hpke(data(#4:Name, #5:Fresh), pkey(#6:Name, #4:Name)) => pke(#0:Msg, s) inL .) | ( grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; grl #0:Msg inL => pke(#0:Msg, i) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(i, #1:Name)) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(#1:Name, i)) inL . ; grl #0:Msg inL => sign(#0:Msg, #1:Name) inL . ; grl f(#0:Msg, #1:Msg) notLeq f(#2:HEnc, #3:HEnc) => f(#0:Msg, #1:Msg) inL .) | ( grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; grl #0:Msg inL => pke(#0:Msg, i) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(i, #1:Name)) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(#1:Name, i)) inL . ; grl #0:Msg inL => sign(#0:Msg, #1:Name) inL . ; grl #0:Msg notInI => hpke(#0:Msg, #1:Pkey) inL .) | ( grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; grl #0:Msg inL => pke(#0:Msg, i) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(i, #1:Name)) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(#1:Name, i)) inL . ; grl #0:Msg inL => sign(#0:Msg, #1:Name) inL . ; grl #0:Pkey notInI, #0:Pkey notLeq pkey(#1:Name, #2:Name) => hpke(#3:Msg, #0:Pkey) inL .) | ( grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; grl #0:Msg inL => pke(#0:Msg, i) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(i, #1:Name)) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(#1:Name, i)) inL . ; grl #0:Msg inL => sign(#0:Msg, #1:Name) inL . ; grl hpke(#0:Msg, #1:Pkey) notLeq hpke(#2:Msg, pkey(#3:Name, #4:Name)) => hpke(#0:Msg, #1:Pkey) inL .) | (errorInconsistentExceptionsInGrammarRule grl n(#0:Name, #1:Fresh) notLeq #5:Nonce => n(#0:Name, #1:Fresh) inL . inGrammar grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; grl #0:Msg inL => pke(#0:Msg, i) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(i, #1:Name)) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(#1:Name, i)) inL . ; grl #0:Msg inL => sign(#0:Msg, #1:Name) inL . ; grl n(#0:Name, #1:Fresh) notLeq #5:Nonce => n(#0:Name, #1:Fresh) inL .) | ( grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; grl #0:Msg inL => pke(#0:Msg, i) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(i, #1:Name)) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(#1:Name, i)) inL . ; grl #0:Msg inL => sign(#0:Msg, #1:Name) inL . ; grl #0:Msg notInI, (#0:Msg notLeq hpke(data(#1:Name, #2:Fresh), pkey(#1:Name, #3:Name))), #0:Msg notLeq hpke(data(#4:Name, #5:Fresh), pkey(#6:Name, #4:Name)) => pke(#0:Msg, #7:Name) inL .) | (errorNoHeuristicApplied { grl empty => pke(#1:Msg, #2:Name) inL .,none, grl empty => (#1:Msg,#2:Name) inL .,none, grl empty => (#1:Msg,#2:Name) inL .} usingGrammar grl empty => pke(#1:Msg, #2:Name) inL .) | ( grl empty => pkey(#0:Name, #1:Name) inL . ; grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; grl #0:Msg inL => pke(#0:Msg, i) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(i, #1:Name)) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(#1:Name, i)) inL . ; grl #0:Msg inL => sign(#0:Msg, #1:Name) inL .) | ( grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; grl #0:Msg inL => pke(#0:Msg, i) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(i, #1:Name)) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(#1:Name, i)) inL . ; grl #0:Msg inL => sign(#0:Msg, #1:Name) inL . ; grl #0:Msg notInI, (#0:Msg notLeq #1:Name ; #2:Name ; #3:Nonce ; #4:Nonce ; f(#5:HEnc, #6:HEnc)), (#0:Msg notLeq #7:Name ; #8:Name ; n(#7:Name, #9:Fresh) ; #10:Nonce ; pke(hpke(data(#7:Name, #11:Fresh), pkey(#7:Name, #8:Name)), s) ; #12:Enc), (#0:Msg notLeq #13:Name ; n(#14:Name, #15:Fresh) ; pke(hpke(data(#14:Name, #16:Fresh), pkey(#14:Name, #13:Name)), s)), #0:Msg notLeq #17:Nonce ; n(#18:Name, #19:Fresh) ; pke(hpke(data(#18:Name, #20:Fresh), pkey( #21:Name, #18:Name)), s) => sign(#0:Msg, #22:Name) inL .) | grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ; grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ; grl #0:Msg inL => pke(#0:Msg, i) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(i, #1:Name)) inL . ; grl #0:Msg inL => hpke(#0:Msg, pkey(#1:Name, i)) inL . ; grl #0:Msg inL => sign(#0:Msg, #1:Name) inL . ; grl (sign(#0:Msg, #1:Name) notLeq sign(#2:Msg, i)), (sign(#0:Msg, #1:Name) notLeq sign(#3:Name ; #4:Name ; #5:Nonce ; #6:Nonce ; f(#7:HEnc, #8:HEnc), s)), (sign(#0:Msg, #1:Name) notLeq sign(#9:Name ; #10:Name ; n(#9:Name, #11:Fresh) ; #12:Nonce ; pke(hpke(data(#9:Name, #13:Fresh), pkey(#9:Name, #10:Name)), s) ; #14:Enc, #9:Name)), (sign(#0:Msg, #1:Name) notLeq sign(#15:Name ; n(#16:Name, #17:Fresh) ; pke(hpke(data(#16:Name, #18:Fresh), pkey(#16:Name, #15:Name)), s), #16:Name)), sign(#0:Msg, #1:Name) notLeq sign(#19:Nonce ; n(#20:Name, #21:Fresh) ; pke(hpke(data(#20:Name, #22:Fresh), pkey(#23:Name, #20:Name)), s), #20:Name) => sign(#0:Msg, #1:Name) inL . ========================================== reduce in MAUDE-NPA : run(0) . rewrites: 3978 in 39ms cpu (41ms real) (100910 rewrites/second) result IdSystem: < 1 > :: r:Fresh,r':Fresh :: [ nil, +(sign(b ; n(a, r:Fresh) ; pke(hpke(data(a, r':Fresh), pkey(a, b)), s), a)), -(sign(n(a, r:Fresh) ; N:Nonce ; Y1:Enc, b)), +(sign(a ; b ; n(a, r:Fresh) ; N:Nonce ; pke(hpke(data(a, r':Fresh), pkey(a, b)), s) ; Y1:Enc, a)), -(sign(a ; b ; n(a, r:Fresh) ; N:Nonce ; X1:HEnc, s)) | nil] || empty || nil || nil || never((S:StrandSet & :: r1:Fresh,r2:Fresh :: [ nil | -(sign(b ; n(a, r:Fresh) ; pke(hpke(data(a, r':Fresh), pkey(a, b)), s), a)), +(sign(n(a, r:Fresh) ; n(b, r1:Fresh) ; pke(hpke(data(b, r2:Fresh), pkey(a, b)), s), b)), nil] ) || IK:IntruderKnowledge) ========================================== reduce in MAUDE-NPA : summary(1) . rewrites: 8054899 in 20759ms cpu (20789ms real) (388010 rewrites/second) result Summary: States>> 2 Solutions>> 0 ========================================== reduce in MAUDE-NPA : summary(2) . rewrites: 8804174 in 32429ms cpu (32474ms real) (271490 rewrites/second) result Summary: States>> 2 Solutions>> 0 ========================================== reduce in MAUDE-NPA : summary(3) . rewrites: 7144452 in 37074ms cpu (37129ms real) (192705 rewrites/second) result Summary: States>> 1 Solutions>> 0 ========================================== reduce in MAUDE-NPA : summary(4) . rewrites: 3376920 in 19732ms cpu (19746ms real) (171135 rewrites/second) result Summary: States>> 1 Solutions>> 0 ========================================== reduce in MAUDE-NPA : summary(5) . rewrites: 2712140 in 20551ms cpu (20565ms real) (131966 rewrites/second) result Summary: States>> 1 Solutions>> 0 ========================================== reduce in MAUDE-NPA : summary(6) . rewrites: 3045368 in 29559ms cpu (29583ms real) (103025 rewrites/second) result Summary: States>> 2 Solutions>> 0 ========================================== reduce in MAUDE-NPA : summary(7) . rewrites: 6111024 in 54075ms cpu (54121ms real) (113008 rewrites/second) result Summary: States>> 2 Solutions>> 0 ========================================== reduce in MAUDE-NPA : summary(8) . rewrites: 7255205 in 58009ms cpu (58050ms real) (125069 rewrites/second) result Summary: States>> 2 Solutions>> 0 ========================================== reduce in MAUDE-NPA : summary(9) . rewrites: 8903048 in 74881ms cpu (74924ms real) (118895 rewrites/second) result Summary: States>> 2 Solutions>> 0 ========================================== reduce in MAUDE-NPA : summary(10) . rewrites: 10268734 in 91741ms cpu (91834ms real) (111931 rewrites/second) result Summary: States>> 3 Solutions>> 1 ========================================== reduce in MAUDE-NPA : summary(11) . rewrites: 12959045 in 97533ms cpu (97592ms real) (132867 rewrites/second) result Summary: States>> 2 Solutions>> 1 ========================================== reduce in MAUDE-NPA : summary(12) . rewrites: 8468602 in 67428ms cpu (67471ms real) (125593 rewrites/second) result Summary: States>> 1 Solutions>> 1 ========================================== reduce in MAUDE-NPA : run(1) . rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second) result IdSystemSet: (< 1 . 6 > ( :: nil :: [ nil | -(sign(a ; b ; n(a, #0:Fresh) ; #1:Nonce ; pke(#2:HEnc, s) ; pke(#3:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; #1:Nonce ; f(#2:HEnc, #3:HEnc), s)), nil] & :: #0:Fresh,#4:Fresh :: [ nil, +(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s), a)), -(sign(n(a, #0:Fresh) ; #1:Nonce ; #5:Enc, b)), +(sign(a ; b ; n(a, #0:Fresh) ; #1:Nonce ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s) ; #5:Enc, a)) | -(sign(a ; b ; n(a, #0:Fresh) ; #1:Nonce ; f(#2:HEnc, #3:HEnc), s)), nil] ) || sign(a ; b ; n(a, #0:Fresh) ; #1:Nonce ; f(#2:HEnc, #3:HEnc), s) !inI, sign(a ; b ; n(a, #0:Fresh) ; #1:Nonce ; pke(#2:HEnc, s) ; pke(#3:HEnc, s), a) inI || -(sign(a ; b ; n(a, #0:Fresh) ; #1:Nonce ; pke(#2:HEnc, s) ; pke(#3:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; #1:Nonce ; f(#2:HEnc, #3:HEnc), s)), -(sign(a ; b ; n(a, #0:Fresh) ; #1:Nonce ; #6:HEnc, s)) || nil || never((#7:StrandSet & :: #8:Fresh,#9:Fresh :: [ nil | -(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s), a)), +(sign(n(a, #0:Fresh) ; n(b, #8:Fresh) ; pke(hpke(data(b, #9:Fresh), pkey(a, b)), s), b)), nil] ) || #10:IntruderKnowledge)) < 1 . 8 > :: #1:Fresh,#0:Fresh :: [ nil, +(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a)) | -(sign(n(a, #0:Fresh) ; #2:Nonce ; #3:Enc, b)), +(sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; #3:Enc, a)), -(sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; #4:HEnc, s)), nil] || sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; #4:HEnc, s) inI, sign(n(a, #0:Fresh) ; #2:Nonce ; #3:Enc, b) inI || -(sign(n(a, #0:Fresh) ; #2:Nonce ; #3:Enc, b)), +(sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; #3:Enc, a)), -(sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; #4:HEnc, s)) || nil || never((#5:StrandSet & :: #6:Fresh,#7:Fresh :: [ nil | -(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a)), +(sign(n(a, #0:Fresh) ; n(b, #6:Fresh) ; pke(hpke(data(b, #7:Fresh), pkey(a, b)), s), b)), nil] ) || #8:IntruderKnowledge) ========================================== reduce in MAUDE-NPA : run(2) . rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second) result IdSystemSet: (< 1 . 6 . 1 > ( :: nil :: [ nil | -(sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; pke(#4:HEnc, s) ; pke(#5:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; f(#4:HEnc, #5:HEnc), s)), nil] & :: #1:Fresh,#0:Fresh :: [ nil, +(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a)) | -(sign(n(a, #0:Fresh) ; #2:Nonce ; #3:Enc, b)), +(sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; #3:Enc, a)), -(sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; f(#4:HEnc, #5:HEnc), s)), nil] ) || sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; f(#4:HEnc, #5:HEnc), s) !inI, sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; pke(#4:HEnc, s) ; pke(#5:HEnc, s), a) inI, sign(n(a, #0:Fresh) ; #2:Nonce ; #3:Enc, b) inI || -(sign(n(a, #0:Fresh) ; #2:Nonce ; #3:Enc, b)), +(sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; #3:Enc, a)), -(sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; pke(#4:HEnc, s) ; pke(#5:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; f(#4:HEnc, #5:HEnc), s)), -(sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; #6:HEnc, s)) || nil || never((#7:StrandSet & :: #8:Fresh,#9:Fresh :: [ nil | -(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a)), +(sign(n(a, #0:Fresh) ; n(b, #8:Fresh) ; pke(hpke(data(b, #9:Fresh), pkey(a, b)), s), b)), nil] ) || #10:IntruderKnowledge)) < 1 . 6 . 2 > ( :: nil :: [ nil | -(sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; pke(#3:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; f(hpke(data(a, #1:Fresh), pkey(a, b)), #3:HEnc), s)), nil] & :: #1:Fresh,#0:Fresh :: [ nil, +(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a)) | -(sign(n(a, #0:Fresh) ; #2:Nonce ; pke(#3:HEnc, s), b)), +(sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; pke(#3:HEnc, s), a)), -(sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; f(hpke(data(a, #1:Fresh), pkey(a, b)), #3:HEnc), s)), nil] ) || sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; pke(#3:HEnc, s), a) !inI, sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; f(hpke(data(a, #1:Fresh), pkey(a, b)), #3:HEnc), s) !inI, sign(n(a, #0:Fresh) ; #2:Nonce ; pke(#3:HEnc, s), b) inI, inst(#3:HEnc) || -(sign(n(a, #0:Fresh) ; #2:Nonce ; pke(#3:HEnc, s), b)), +(sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; pke(#3:HEnc, s), a)), -(sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; pke(#3:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; f(hpke(data(a, #1:Fresh), pkey(a, b)), #3:HEnc), s)), -(sign(a ; b ; n(a, #0:Fresh) ; #2:Nonce ; #4:HEnc, s)) || nil || never((#5:StrandSet & :: #6:Fresh,#7:Fresh :: [ nil | -(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a)), +(sign(n(a, #0:Fresh) ; n(b, #6:Fresh) ; pke(hpke(data(b, #7:Fresh), pkey(a, b)), s), b)), nil] ) || #8:IntruderKnowledge) ========================================== reduce in MAUDE-NPA : run(3) . rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second) result IdSystem: < 1 . 6 . 2 . 7 > ( :: nil :: [ nil | -(sign(a ; b ; n(a, #1:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(a, #0:Fresh), pkey(a, b)), s) ; pke(#6:HEnc, s), a)), +(sign(a ; b ; n(a, #1:Fresh) ; n(b, #2:Fresh) ; f(hpke(data(a, #0:Fresh), pkey(a, b)), #6:HEnc), s)), nil] & :: #1:Fresh,#0:Fresh :: [ nil, +(sign(b ; n(a, #1:Fresh) ; pke(hpke(data(a, #0:Fresh), pkey(a, b)), s), a)) | -(sign(n(a, #1:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(b, #3:Fresh), pkey(#4:Name, b)), s), b)), +(sign(a ; b ; n(a, #1:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(a, #0:Fresh), pkey(a, b)), s) ; pke(hpke(data(b, #3:Fresh), pkey(#4:Name, b)), s), a)), -(sign(a ; b ; n(a, #1:Fresh) ; n(b, #2:Fresh) ; f(hpke(data(a, #0:Fresh), pkey(a, b)), hpke(data(b, #3:Fresh), pkey(#4:Name, b))), s)), nil] & :: #2:Fresh,#3:Fresh :: [ nil | -(sign(b ; n(a, #1:Fresh) ; #5:Enc, #4:Name)), +(sign(n(a, #1:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(b, #3:Fresh), pkey(#4:Name, b)), s), b)), nil] ) || sign(a ; b ; n(a, #1:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(a, #0:Fresh), pkey(a, b)), s) ; pke(#6:HEnc, s), a) !inI, sign(a ; b ; n(a, #1:Fresh) ; n(b, #2:Fresh) ; f(hpke(data(a, #0:Fresh), pkey(a, b)), #6:HEnc), s) !inI, sign(n(a, #1:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(b, #3:Fresh), pkey(#4:Name, b)), s), b) !inI, sign(b ; n(a, #1:Fresh) ; #5:Enc, #4:Name) inI, inst(#6:HEnc) || -(sign(b ; n(a, #1:Fresh) ; #5:Enc, #4:Name)), +(sign(n(a, #1:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(b, #3:Fresh), pkey(#4:Name, b)), s), b)), -(sign(n(a, #1:Fresh) ; n(b, #2:Fresh) ; pke(#6:HEnc, s), b)), +(sign(a ; b ; n(a, #1:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(a, #0:Fresh), pkey(a, b)), s) ; pke(#6:HEnc, s), a)), -(sign(a ; b ; n(a, #1:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(a, #0:Fresh), pkey(a, b)), s) ; pke(#6:HEnc, s), a)), +(sign(a ; b ; n(a, #1:Fresh) ; n(b, #2:Fresh) ; f(hpke(data(a, #0:Fresh), pkey(a, b)), #6:HEnc), s)), -(sign(a ; b ; n(a, #1:Fresh) ; n(b, #2:Fresh) ; #7:HEnc, s)) || nil || never((#8:StrandSet & :: #9:Fresh,#10:Fresh :: [ nil | -(sign(b ; n(a, #1:Fresh) ; pke(hpke(data(a, #0:Fresh), pkey(a, b)), s), a)), +(sign(n(a, #1:Fresh) ; n(b, #9:Fresh) ; pke(hpke(data(b, #10:Fresh), pkey(a, b)), s), b)), nil] ) || #11:IntruderKnowledge) ========================================== reduce in MAUDE-NPA : run(4) . rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second) result IdSystem: < 1 . 6 . 2 . 7 . 3 > ( :: nil :: [ nil | -(b ; n(a, #0:Fresh) ; #1:Enc), +(sign(b ; n(a, #0:Fresh) ; #1:Enc, i)), nil] & :: nil :: [ nil | -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; f(hpke(data(a, #2:Fresh), pkey(a, b)), #5:HEnc), s)), nil] & :: #2:Fresh,#0:Fresh :: [ nil, +(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s), a)) | -(sign(n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(b, #4:Fresh), pkey(i, b)), s), b)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s) ; pke(hpke(data(b, #4:Fresh), pkey(i, b)), s), a)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; f(hpke(data(a, #2:Fresh), pkey(a, b)), hpke(data(b, #4:Fresh), pkey(i, b))), s)), nil] & :: #3:Fresh,#4:Fresh :: [ nil | -(sign(b ; n(a, #0:Fresh) ; #1:Enc, i)), +(sign(n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(b, #4:Fresh), pkey(i, b)), s), b)), nil] ) || sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a) !inI, sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; f(hpke(data(a, #2:Fresh), pkey(a, b)), #5:HEnc), s) !inI, sign(b ; n(a, #0:Fresh) ; #1:Enc, i) !inI, sign(n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(b, #4:Fresh), pkey(i, b)), s), b) !inI, (b ; n(a, #0:Fresh) ; #1:Enc) inI, inst(#5:HEnc) || -(b ; n(a, #0:Fresh) ; #1:Enc), +(sign(b ; n(a, #0:Fresh) ; #1:Enc, i)), -(sign(b ; n(a, #0:Fresh) ; #1:Enc, i)), +(sign(n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(b, #4:Fresh), pkey(i, b)), s), b)), -(sign(n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(#5:HEnc, s), b)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; f(hpke(data(a, #2:Fresh), pkey(a, b)), #5:HEnc), s)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; #6:HEnc, s)) || nil || never((#7:StrandSet & :: #8:Fresh,#9:Fresh :: [ nil | -(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s), a)), +(sign(n(a, #0:Fresh) ; n(b, #8:Fresh) ; pke(hpke(data(b, #9:Fresh), pkey(a, b)), s), b)), nil] ) || #10:IntruderKnowledge) ========================================== reduce in MAUDE-NPA : run(5) . rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second) result IdSystem: < 1 . 6 . 2 . 7 . 3 . 2 > ( :: nil :: [ nil | -(b), -(n(a, #0:Fresh) ; #1:Enc), +(b ; n(a, #0:Fresh) ; #1:Enc), nil] & :: nil :: [ nil | -(b ; n(a, #0:Fresh) ; #1:Enc), +(sign(b ; n(a, #0:Fresh) ; #1:Enc, i)), nil] & :: nil :: [ nil | -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; f(hpke(data(a, #2:Fresh), pkey(a, b)), #5:HEnc), s)), nil] & :: #2:Fresh,#0:Fresh :: [ nil, +(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s), a)) | -(sign(n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(b, #4:Fresh), pkey(i, b)), s), b)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s) ; pke(hpke(data(b, #4:Fresh), pkey(i, b)), s), a)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; f(hpke(data(a, #2:Fresh), pkey(a, b)), hpke(data(b, #4:Fresh), pkey(i, b))), s)), nil] & :: #3:Fresh,#4:Fresh :: [ nil | -(sign(b ; n(a, #0:Fresh) ; #1:Enc, i)), +(sign(n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(b, #4:Fresh), pkey(i, b)), s), b)), nil] ) || (b ; n(a, #0:Fresh) ; #1:Enc) !inI, sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a) !inI, sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; f(hpke(data(a, #2:Fresh), pkey(a, b)), #5:HEnc), s) !inI, sign(b ; n(a, #0:Fresh) ; #1:Enc, i) !inI, sign(n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(b, #4:Fresh), pkey(i, b)), s), b) !inI, (n(a, #0:Fresh) ; #1:Enc) inI, inst(#5:HEnc) || -(b), -(n(a, #0:Fresh) ; #1:Enc), +(b ; n(a, #0:Fresh) ; #1:Enc), -(b ; n(a, #0:Fresh) ; #1:Enc), +(sign(b ; n(a, #0:Fresh) ; #1:Enc, i)), -(sign(b ; n(a, #0:Fresh) ; #1:Enc, i)), +(sign(n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(b, #4:Fresh), pkey(i, b)), s), b)), -(sign(n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(#5:HEnc, s), b)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; f(hpke(data(a, #2:Fresh), pkey(a, b)), #5:HEnc), s)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; #6:HEnc, s)) || nil || never((#7:StrandSet & :: #8:Fresh,#9:Fresh :: [ nil | -(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s), a)), +(sign(n(a, #0:Fresh) ; n(b, #8:Fresh) ; pke(hpke(data(b, #9:Fresh), pkey(a, b)), s), b)), nil] ) || #10:IntruderKnowledge) ========================================== reduce in MAUDE-NPA : run(6) . rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second) result IdSystemSet: (< 1 . 6 . 2 . 7 . 3 . 2 . 2 > ( :: nil :: [ nil | -(b), -(n(a, #1:Fresh) ; #2:Enc), +(b ; n(a, #1:Fresh) ; #2:Enc), nil] & :: nil :: [ nil | -(b ; n(a, #1:Fresh) ; #2:Enc), +(sign(b ; n(a, #1:Fresh) ; #2:Enc, i)), nil] & :: nil :: [ nil | -(#0:Msg ; n(a, #1:Fresh) ; #2:Enc), +(n(a, #1:Fresh) ; #2:Enc), nil] & :: nil :: [ nil | -(sign(a ; b ; n(a, #1:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(a, #3:Fresh), pkey(a, b)), s) ; pke(#6:HEnc, s), a)), +(sign(a ; b ; n(a, #1:Fresh) ; n(b, #4:Fresh) ; f(hpke(data(a, #3:Fresh), pkey(a, b)), #6:HEnc), s)), nil] & :: #1:Fresh,#3:Fresh :: [ nil, +(sign(b ; n(a, #1:Fresh) ; pke(hpke(data(a, #3:Fresh), pkey(a, b)), s), a)) | -(sign(n(a, #1:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(b, #5:Fresh), pkey(i, b)), s), b)), +(sign(a ; b ; n(a, #1:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(a, #3:Fresh), pkey(a, b)), s) ; pke(hpke(data(b, #5:Fresh), pkey(i, b)), s), a)), -(sign(a ; b ; n(a, #1:Fresh) ; n(b, #4:Fresh) ; f(hpke(data(a, #3:Fresh), pkey(a, b)), hpke(data(b, #5:Fresh), pkey(i, b))), s)), nil] & :: #4:Fresh,#5:Fresh :: [ nil | -(sign(b ; n(a, #1:Fresh) ; #2:Enc, i)), +(sign(n(a, #1:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(b, #5:Fresh), pkey(i, b)), s), b)), nil] ) || (b ; n(a, #1:Fresh) ; #2:Enc) !inI, (n(a, #1:Fresh) ; #2:Enc) !inI, sign(a ; b ; n(a, #1:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(a, #3:Fresh), pkey(a, b)), s) ; pke(#6:HEnc, s), a) !inI, sign(a ; b ; n(a, #1:Fresh) ; n(b, #4:Fresh) ; f(hpke(data(a, #3:Fresh), pkey(a, b)), #6:HEnc), s) !inI, sign(b ; n(a, #1:Fresh) ; #2:Enc, i) !inI, sign(n(a, #1:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(b, #5:Fresh), pkey(i, b)), s), b) !inI, (#0:Msg ; n(a, #1:Fresh) ; #2:Enc) inI, inst(#6:HEnc) || -(#0:Msg ; n(a, #1:Fresh) ; #2:Enc), +(n(a, #1:Fresh) ; #2:Enc), -(b), -(n(a, #1:Fresh) ; #2:Enc), +(b ; n(a, #1:Fresh) ; #2:Enc), -(b ; n(a, #1:Fresh) ; #2:Enc), +(sign(b ; n(a, #1:Fresh) ; #2:Enc, i)), -(sign(b ; n(a, #1:Fresh) ; #2:Enc, i)), +(sign(n(a, #1:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(b, #5:Fresh), pkey(i, b)), s), b)), -(sign(n(a, #1:Fresh) ; n(b, #4:Fresh) ; pke(#6:HEnc, s), b)), +(sign(a ; b ; n(a, #1:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(a, #3:Fresh), pkey(a, b)), s) ; pke(#6:HEnc, s), a)), -(sign(a ; b ; n(a, #1:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(a, #3:Fresh), pkey(a, b)), s) ; pke(#6:HEnc, s), a)), +(sign(a ; b ; n(a, #1:Fresh) ; n(b, #4:Fresh) ; f(hpke(data(a, #3:Fresh), pkey(a, b)), #6:HEnc), s)), -(sign(a ; b ; n(a, #1:Fresh) ; n(b, #4:Fresh) ; #7:HEnc, s)) || nil || never((#8:StrandSet & :: #9:Fresh,#10:Fresh :: [ nil | -(sign(b ; n(a, #1:Fresh) ; pke(hpke(data(a, #3:Fresh), pkey(a, b)), s), a)), +(sign(n(a, #1:Fresh) ; n(b, #9:Fresh) ; pke(hpke(data(b, #10:Fresh), pkey(a, b)), s), b)), nil] ) || #11:IntruderKnowledge)) < 1 . 6 . 2 . 7 . 3 . 2 . 3 > ( :: nil :: [ nil | -(b), -(n(a, #0:Fresh) ; #1:Enc), +(b ; n(a, #0:Fresh) ; #1:Enc), nil] & :: nil :: [ nil | -(n(a, #0:Fresh)), -(#1:Enc), +(n(a, #0:Fresh) ; #1:Enc), nil] & :: nil :: [ nil | -(b ; n(a, #0:Fresh) ; #1:Enc), +(sign(b ; n(a, #0:Fresh) ; #1:Enc, i)), nil] & :: nil :: [ nil | -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; f(hpke(data(a, #2:Fresh), pkey(a, b)), #5:HEnc), s)), nil] & :: #2:Fresh,#0:Fresh :: [ nil, +(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s), a)) | -(sign(n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(b, #4:Fresh), pkey(i, b)), s), b)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s) ; pke(hpke(data(b, #4:Fresh), pkey(i, b)), s), a)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; f(hpke(data(a, #2:Fresh), pkey(a, b)), hpke(data(b, #4:Fresh), pkey(i, b))), s)), nil] & :: #3:Fresh,#4:Fresh :: [ nil | -(sign(b ; n(a, #0:Fresh) ; #1:Enc, i)), +(sign(n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(b, #4:Fresh), pkey(i, b)), s), b)), nil] ) || #1:Enc !inI, (b ; n(a, #0:Fresh) ; #1:Enc) !inI, (n(a, #0:Fresh) ; #1:Enc) !inI, sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a) !inI, sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; f(hpke(data(a, #2:Fresh), pkey(a, b)), #5:HEnc), s) !inI, sign(b ; n(a, #0:Fresh) ; #1:Enc, i) !inI, sign(n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(b, #4:Fresh), pkey(i, b)), s), b) !inI, n(a, #0:Fresh) inI, inst(#5:HEnc) || generatedByIntruder(#1:Enc), -(n(a, #0:Fresh)), -(#1:Enc), +(n(a, #0:Fresh) ; #1:Enc), -(b), -(n(a, #0:Fresh) ; #1:Enc), +(b ; n(a, #0:Fresh) ; #1:Enc), -(b ; n(a, #0:Fresh) ; #1:Enc), +(sign(b ; n(a, #0:Fresh) ; #1:Enc, i)), -(sign(b ; n(a, #0:Fresh) ; #1:Enc, i)), +(sign(n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(b, #4:Fresh), pkey(i, b)), s), b)), -(sign(n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(#5:HEnc, s), b)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; f(hpke(data(a, #2:Fresh), pkey(a, b)), #5:HEnc), s)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; #6:HEnc, s)) || nil || never((#7:StrandSet & :: #8:Fresh,#9:Fresh :: [ nil | -(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s), a)), +(sign(n(a, #0:Fresh) ; n(b, #8:Fresh) ; pke(hpke(data(b, #9:Fresh), pkey(a, b)), s), b)), nil] ) || #10:IntruderKnowledge) ========================================== reduce in MAUDE-NPA : run(7) . rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second) result IdSystemSet: (< 1 . 6 . 2 . 7 . 3 . 2 . 2 . 7 > ( :: nil :: [ nil | -(b), -(n(a, #1:Fresh) ; #2:Enc), +(b ; n(a, #1:Fresh) ; #2:Enc), nil] & :: nil :: [ nil | -(b ; n(a, #1:Fresh) ; #2:Enc), +(sign(b ; n(a, #1:Fresh) ; #2:Enc, i)), nil] & :: nil :: [ nil | -(#0:Msg ; n(a, #1:Fresh) ; #2:Enc), +(n(a, #1:Fresh) ; #2:Enc), nil] & :: nil :: [ nil | -(sign(a ; b ; n(a, #1:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s) ; pke(#7:HEnc, s), a)), +(sign(a ; b ; n(a, #1:Fresh) ; n(b, #5:Fresh) ; f(hpke(data(a, #4:Fresh), pkey(a, b)), #7:HEnc), s)), nil] & :: nil :: [ nil | -(sign(#0:Msg ; n(a, #1:Fresh) ; #2:Enc, #3:Name)), +(#0:Msg ; n(a, #1:Fresh) ; #2:Enc), nil] & :: #1:Fresh,#4:Fresh :: [ nil, +(sign(b ; n(a, #1:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s), a)) | -(sign(n(a, #1:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(b, #6:Fresh), pkey(i, b)), s), b)), +(sign(a ; b ; n(a, #1:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s) ; pke(hpke(data(b, #6:Fresh), pkey(i, b)), s), a)), -(sign(a ; b ; n(a, #1:Fresh) ; n(b, #5:Fresh) ; f(hpke(data(a, #4:Fresh), pkey(a, b)), hpke(data(b, #6:Fresh), pkey(i, b))), s)), nil] & :: #5:Fresh,#6:Fresh :: [ nil | -(sign(b ; n(a, #1:Fresh) ; #2:Enc, i)), +(sign(n(a, #1:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(b, #6:Fresh), pkey(i, b)), s), b)), nil] ) || (b ; n(a, #1:Fresh) ; #2:Enc) !inI, (#0:Msg ; n(a, #1:Fresh) ; #2:Enc) !inI, (n(a, #1:Fresh) ; #2:Enc) !inI, sign(a ; b ; n(a, #1:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s) ; pke(#7:HEnc, s), a) !inI, sign(a ; b ; n(a, #1:Fresh) ; n(b, #5:Fresh) ; f(hpke(data(a, #4:Fresh), pkey(a, b)), #7:HEnc), s) !inI, sign(b ; n(a, #1:Fresh) ; #2:Enc, i) !inI, sign(n(a, #1:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(b, #6:Fresh), pkey(i, b)), s), b) !inI, sign(#0:Msg ; n(a, #1:Fresh) ; #2:Enc, #3:Name) inI, inst(#7:HEnc) || -(sign(#0:Msg ; n(a, #1:Fresh) ; #2:Enc, #3:Name)), +(#0:Msg ; n(a, #1:Fresh) ; #2:Enc), -(#0:Msg ; n(a, #1:Fresh) ; #2:Enc), +(n(a, #1:Fresh) ; #2:Enc), -(b), -(n(a, #1:Fresh) ; #2:Enc), +(b ; n(a, #1:Fresh) ; #2:Enc), -(b ; n(a, #1:Fresh) ; #2:Enc), +(sign(b ; n(a, #1:Fresh) ; #2:Enc, i)), -(sign(b ; n(a, #1:Fresh) ; #2:Enc, i)), +(sign(n(a, #1:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(b, #6:Fresh), pkey(i, b)), s), b)), -(sign(n(a, #1:Fresh) ; n(b, #5:Fresh) ; pke(#7:HEnc, s), b)), +(sign(a ; b ; n(a, #1:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s) ; pke(#7:HEnc, s), a)), -(sign(a ; b ; n(a, #1:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s) ; pke(#7:HEnc, s), a)), +(sign(a ; b ; n(a, #1:Fresh) ; n(b, #5:Fresh) ; f(hpke(data(a, #4:Fresh), pkey(a, b)), #7:HEnc), s)), -(sign(a ; b ; n(a, #1:Fresh) ; n(b, #5:Fresh) ; #8:HEnc, s)) || nil || never((#9:StrandSet & :: #10:Fresh,#11:Fresh :: [ nil | -(sign(b ; n(a, #1:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s), a)), +(sign(n(a, #1:Fresh) ; n(b, #10:Fresh) ; pke(hpke(data(b, #11:Fresh), pkey(a, b)), s), b)), nil] ) || #12:IntruderKnowledge)) < 1 . 6 . 2 . 7 . 3 . 2 . 3 . 4 > ( :: nil :: [ nil | -(b), -(n(a, #0:Fresh) ; #5:Enc), +(b ; n(a, #0:Fresh) ; #5:Enc), nil] & :: nil :: [ nil | -(n(a, #0:Fresh)), -(#5:Enc), +(n(a, #0:Fresh) ; #5:Enc), nil] & :: nil :: [ nil | -(b ; n(a, #0:Fresh) ; #5:Enc), +(sign(b ; n(a, #0:Fresh) ; #5:Enc, i)), nil] & :: nil :: [ nil | -(n(a, #0:Fresh) ; #1:Msg), +(n(a, #0:Fresh)), nil] & :: nil :: [ nil | -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s) ; pke(#6:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; f(hpke(data(a, #2:Fresh), pkey(a, b)), #6:HEnc), s)), nil] & :: #2:Fresh,#0:Fresh :: [ nil, +(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s), a)) | -(sign(n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(b, #4:Fresh), pkey(i, b)), s), b)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s) ; pke(hpke(data(b, #4:Fresh), pkey(i, b)), s), a)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; f(hpke(data(a, #2:Fresh), pkey(a, b)), hpke(data(b, #4:Fresh), pkey(i, b))), s)), nil] & :: #3:Fresh,#4:Fresh :: [ nil | -(sign(b ; n(a, #0:Fresh) ; #5:Enc, i)), +(sign(n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(b, #4:Fresh), pkey(i, b)), s), b)), nil] ) || #5:Enc !inI, n(a, #0:Fresh) !inI, (b ; n(a, #0:Fresh) ; #5:Enc) !inI, (n(a, #0:Fresh) ; #5:Enc) !inI, sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s) ; pke(#6:HEnc, s), a) !inI, sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; f(hpke(data(a, #2:Fresh), pkey(a, b)), #6:HEnc), s) !inI, sign(b ; n(a, #0:Fresh) ; #5:Enc, i) !inI, sign(n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(b, #4:Fresh), pkey(i, b)), s), b) !inI, (n(a, #0:Fresh) ; #1:Msg) inI, inst(#6:HEnc) || -(n(a, #0:Fresh) ; #1:Msg), +(n(a, #0:Fresh)), generatedByIntruder(#5:Enc), -(n(a, #0:Fresh)), -(#5:Enc), +(n(a, #0:Fresh) ; #5:Enc), -(b), -(n(a, #0:Fresh) ; #5:Enc), +(b ; n(a, #0:Fresh) ; #5:Enc), -(b ; n(a, #0:Fresh) ; #5:Enc), +(sign(b ; n(a, #0:Fresh) ; #5:Enc, i)), -(sign(b ; n(a, #0:Fresh) ; #5:Enc, i)), +(sign(n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(b, #4:Fresh), pkey(i, b)), s), b)), -(sign(n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(#6:HEnc, s), b)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s) ; pke(#6:HEnc, s), a)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s) ; pke(#6:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; f(hpke(data(a, #2:Fresh), pkey(a, b)), #6:HEnc), s)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #3:Fresh) ; #7:HEnc, s)) || nil || never((#8:StrandSet & :: #9:Fresh,#10:Fresh :: [ nil | -(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #2:Fresh), pkey(a, b)), s), a)), +(sign(n(a, #0:Fresh) ; n(b, #9:Fresh) ; pke(hpke(data(b, #10:Fresh), pkey(a, b)), s), b)), nil] ) || #11:IntruderKnowledge) ========================================== reduce in MAUDE-NPA : run(8) . rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second) result IdSystemSet: (< 1 . 6 . 2 . 7 . 3 . 2 . 3 . 4 . 2 > ( :: nil :: [ nil | -(b), -(n(a, #1:Fresh) ; #6:Enc), +(b ; n(a, #1:Fresh) ; #6:Enc), nil] & :: nil :: [ nil | -(n(a, #1:Fresh)), -(#6:Enc), +(n(a, #1:Fresh) ; #6:Enc), nil] & :: nil :: [ nil | -(b ; n(a, #1:Fresh) ; #6:Enc), +(sign(b ; n(a, #1:Fresh) ; #6:Enc, i)), nil] & :: nil :: [ nil | -(#0:Msg ; n(a, #1:Fresh) ; #2:Msg), +(n(a, #1:Fresh) ; #2:Msg), nil] & :: nil :: [ nil | -(n(a, #1:Fresh) ; #2:Msg), +(n(a, #1:Fresh)), nil] & :: nil :: [ nil | -(sign(a ; b ; n(a, #1:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(a, #3:Fresh), pkey(a, b)), s) ; pke(#7:HEnc, s), a)), +(sign(a ; b ; n(a, #1:Fresh) ; n(b, #4:Fresh) ; f(hpke(data(a, #3:Fresh), pkey(a, b)), #7:HEnc), s)), nil] & :: #1:Fresh,#3:Fresh :: [ nil, +(sign(b ; n(a, #1:Fresh) ; pke(hpke(data(a, #3:Fresh), pkey(a, b)), s), a)) | -(sign(n(a, #1:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(b, #5:Fresh), pkey(i, b)), s), b)), +(sign(a ; b ; n(a, #1:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(a, #3:Fresh), pkey(a, b)), s) ; pke(hpke(data(b, #5:Fresh), pkey(i, b)), s), a)), -(sign(a ; b ; n(a, #1:Fresh) ; n(b, #4:Fresh) ; f(hpke(data(a, #3:Fresh), pkey(a, b)), hpke(data(b, #5:Fresh), pkey(i, b))), s)), nil] & :: #4:Fresh,#5:Fresh :: [ nil | -(sign(b ; n(a, #1:Fresh) ; #6:Enc, i)), +(sign(n(a, #1:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(b, #5:Fresh), pkey(i, b)), s), b)), nil] ) || #6:Enc !inI, n(a, #1:Fresh) !inI, (b ; n(a, #1:Fresh) ; #6:Enc) !inI, (n(a, #1:Fresh) ; #2:Msg) !inI, (n(a, #1:Fresh) ; #6:Enc) !inI, sign(a ; b ; n(a, #1:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(a, #3:Fresh), pkey(a, b)), s) ; pke(#7:HEnc, s), a) !inI, sign(a ; b ; n(a, #1:Fresh) ; n(b, #4:Fresh) ; f(hpke(data(a, #3:Fresh), pkey(a, b)), #7:HEnc), s) !inI, sign(b ; n(a, #1:Fresh) ; #6:Enc, i) !inI, sign(n(a, #1:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(b, #5:Fresh), pkey(i, b)), s), b) !inI, (#0:Msg ; n(a, #1:Fresh) ; #2:Msg) inI, inst(#7:HEnc) || -(#0:Msg ; n(a, #1:Fresh) ; #2:Msg), +(n(a, #1:Fresh) ; #2:Msg), -(n(a, #1:Fresh) ; #2:Msg), +(n(a, #1:Fresh)), generatedByIntruder(#6:Enc), -(n(a, #1:Fresh)), -(#6:Enc), +(n(a, #1:Fresh) ; #6:Enc), -(b), -(n(a, #1:Fresh) ; #6:Enc), +(b ; n(a, #1:Fresh) ; #6:Enc), -(b ; n(a, #1:Fresh) ; #6:Enc), +(sign(b ; n(a, #1:Fresh) ; #6:Enc, i)), -(sign(b ; n(a, #1:Fresh) ; #6:Enc, i)), +(sign(n(a, #1:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(b, #5:Fresh), pkey(i, b)), s), b)), -(sign(n(a, #1:Fresh) ; n(b, #4:Fresh) ; pke(#7:HEnc, s), b)), +(sign(a ; b ; n(a, #1:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(a, #3:Fresh), pkey(a, b)), s) ; pke(#7:HEnc, s), a)), -(sign(a ; b ; n(a, #1:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(a, #3:Fresh), pkey(a, b)), s) ; pke(#7:HEnc, s), a)), +(sign(a ; b ; n(a, #1:Fresh) ; n(b, #4:Fresh) ; f(hpke(data(a, #3:Fresh), pkey(a, b)), #7:HEnc), s)), -(sign(a ; b ; n(a, #1:Fresh) ; n(b, #4:Fresh) ; #8:HEnc, s)) || nil || never((#9:StrandSet & :: #10:Fresh,#11:Fresh :: [ nil | -(sign(b ; n(a, #1:Fresh) ; pke(hpke(data(a, #3:Fresh), pkey(a, b)), s), a)), +(sign(n(a, #1:Fresh) ; n(b, #10:Fresh) ; pke(hpke(data(b, #11:Fresh), pkey(a, b)), s), b)), nil] ) || #12:IntruderKnowledge)) < 1 . 6 . 2 . 7 . 3 . 2 . 3 . 4 . 8 > ( :: nil :: [ nil | -(b), -(n(a, #0:Fresh) ; #6:Enc), +(b ; n(a, #0:Fresh) ; #6:Enc), nil] & :: nil :: [ nil | -(n(a, #0:Fresh)), -(#6:Enc), +(n(a, #0:Fresh) ; #6:Enc), nil] & :: nil :: [ nil | -(b ; n(a, #0:Fresh) ; #6:Enc), +(sign(b ; n(a, #0:Fresh) ; #6:Enc, i)), nil] & :: nil :: [ nil | -(n(a, #0:Fresh) ; #1:Msg), +(n(a, #0:Fresh)), nil] & :: nil :: [ nil | -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(a, #3:Fresh), pkey(a, b)), s) ; pke(#7:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #4:Fresh) ; f(hpke(data(a, #3:Fresh), pkey(a, b)), #7:HEnc), s)), nil] & :: nil :: [ nil | -(sign(n(a, #0:Fresh) ; #1:Msg, #2:Name)), +(n(a, #0:Fresh) ; #1:Msg), nil] & :: #0:Fresh,#3:Fresh :: [ nil, +(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #3:Fresh), pkey(a, b)), s), a)) | -(sign(n(a, #0:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(b, #5:Fresh), pkey(i, b)), s), b)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(a, #3:Fresh), pkey(a, b)), s) ; pke(hpke(data(b, #5:Fresh), pkey(i, b)), s), a)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #4:Fresh) ; f(hpke(data(a, #3:Fresh), pkey(a, b)), hpke(data(b, #5:Fresh), pkey(i, b))), s)), nil] & :: #4:Fresh,#5:Fresh :: [ nil | -(sign(b ; n(a, #0:Fresh) ; #6:Enc, i)), +(sign(n(a, #0:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(b, #5:Fresh), pkey(i, b)), s), b)), nil] ) || #6:Enc !inI, n(a, #0:Fresh) !inI, (b ; n(a, #0:Fresh) ; #6:Enc) !inI, (n(a, #0:Fresh) ; #1:Msg) !inI, (n(a, #0:Fresh) ; #6:Enc) !inI, sign(a ; b ; n(a, #0:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(a, #3:Fresh), pkey(a, b)), s) ; pke(#7:HEnc, s), a) !inI, sign(a ; b ; n(a, #0:Fresh) ; n(b, #4:Fresh) ; f(hpke(data(a, #3:Fresh), pkey(a, b)), #7:HEnc), s) !inI, sign(b ; n(a, #0:Fresh) ; #6:Enc, i) !inI, sign(n(a, #0:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(b, #5:Fresh), pkey(i, b)), s), b) !inI, sign(n(a, #0:Fresh) ; #1:Msg, #2:Name) inI, inst(#7:HEnc) || -(sign(n(a, #0:Fresh) ; #1:Msg, #2:Name)), +(n(a, #0:Fresh) ; #1:Msg), -(n(a, #0:Fresh) ; #1:Msg), +(n(a, #0:Fresh)), generatedByIntruder(#6:Enc), -(n(a, #0:Fresh)), -(#6:Enc), +(n(a, #0:Fresh) ; #6:Enc), -(b), -(n(a, #0:Fresh) ; #6:Enc), +(b ; n(a, #0:Fresh) ; #6:Enc), -(b ; n(a, #0:Fresh) ; #6:Enc), +(sign(b ; n(a, #0:Fresh) ; #6:Enc, i)), -(sign(b ; n(a, #0:Fresh) ; #6:Enc, i)), +(sign(n(a, #0:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(b, #5:Fresh), pkey(i, b)), s), b)), -(sign(n(a, #0:Fresh) ; n(b, #4:Fresh) ; pke(#7:HEnc, s), b)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(a, #3:Fresh), pkey(a, b)), s) ; pke(#7:HEnc, s), a)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #4:Fresh) ; pke(hpke(data(a, #3:Fresh), pkey(a, b)), s) ; pke(#7:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #4:Fresh) ; f(hpke(data(a, #3:Fresh), pkey(a, b)), #7:HEnc), s)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #4:Fresh) ; #8:HEnc, s)) || nil || never((#9:StrandSet & :: #10:Fresh,#11:Fresh :: [ nil | -(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #3:Fresh), pkey(a, b)), s), a)), +(sign(n(a, #0:Fresh) ; n(b, #10:Fresh) ; pke(hpke(data(b, #11:Fresh), pkey(a, b)), s), b)), nil] ) || #12:IntruderKnowledge) ========================================== reduce in MAUDE-NPA : run(9) . rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second) result IdSystemSet: (< 1 . 6 . 2 . 7 . 3 . 2 . 3 . 4 . 2 . 7 > ( :: nil :: [ nil | -(b), -(n(a, #1:Fresh) ; #7:Enc), +(b ; n(a, #1:Fresh) ; #7:Enc), nil] & :: nil :: [ nil | -(n(a, #1:Fresh)), -(#7:Enc), +(n(a, #1:Fresh) ; #7:Enc), nil] & :: nil :: [ nil | -(b ; n(a, #1:Fresh) ; #7:Enc), +(sign(b ; n(a, #1:Fresh) ; #7:Enc, i)), nil] & :: nil :: [ nil | -(#0:Msg ; n(a, #1:Fresh) ; #2:Msg), +(n(a, #1:Fresh) ; #2:Msg), nil] & :: nil :: [ nil | -(n(a, #1:Fresh) ; #2:Msg), +(n(a, #1:Fresh)), nil] & :: nil :: [ nil | -(sign(a ; b ; n(a, #1:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s) ; pke(#8:HEnc, s), a)), +(sign(a ; b ; n(a, #1:Fresh) ; n(b, #5:Fresh) ; f(hpke(data(a, #4:Fresh), pkey(a, b)), #8:HEnc), s)), nil] & :: nil :: [ nil | -(sign(#0:Msg ; n(a, #1:Fresh) ; #2:Msg, #3:Name)), +(#0:Msg ; n(a, #1:Fresh) ; #2:Msg), nil] & :: #1:Fresh,#4:Fresh :: [ nil, +(sign(b ; n(a, #1:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s), a)) | -(sign(n(a, #1:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(b, #6:Fresh), pkey(i, b)), s), b)), +(sign(a ; b ; n(a, #1:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s) ; pke(hpke(data(b, #6:Fresh), pkey(i, b)), s), a)), -(sign(a ; b ; n(a, #1:Fresh) ; n(b, #5:Fresh) ; f(hpke(data(a, #4:Fresh), pkey(a, b)), hpke(data(b, #6:Fresh), pkey(i, b))), s)), nil] & :: #5:Fresh,#6:Fresh :: [ nil | -(sign(b ; n(a, #1:Fresh) ; #7:Enc, i)), +(sign(n(a, #1:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(b, #6:Fresh), pkey(i, b)), s), b)), nil] ) || #7:Enc !inI, n(a, #1:Fresh) !inI, (b ; n(a, #1:Fresh) ; #7:Enc) !inI, (#0:Msg ; n(a, #1:Fresh) ; #2:Msg) !inI, (n(a, #1:Fresh) ; #2:Msg) !inI, (n(a, #1:Fresh) ; #7:Enc) !inI, sign(a ; b ; n(a, #1:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s) ; pke(#8:HEnc, s), a) !inI, sign(a ; b ; n(a, #1:Fresh) ; n(b, #5:Fresh) ; f(hpke(data(a, #4:Fresh), pkey(a, b)), #8:HEnc), s) !inI, sign(b ; n(a, #1:Fresh) ; #7:Enc, i) !inI, sign(n(a, #1:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(b, #6:Fresh), pkey(i, b)), s), b) !inI, sign(#0:Msg ; n(a, #1:Fresh) ; #2:Msg, #3:Name) inI, inst(#8:HEnc) || -(sign(#0:Msg ; n(a, #1:Fresh) ; #2:Msg, #3:Name)), +(#0:Msg ; n(a, #1:Fresh) ; #2:Msg), -(#0:Msg ; n(a, #1:Fresh) ; #2:Msg), +(n(a, #1:Fresh) ; #2:Msg), -(n(a, #1:Fresh) ; #2:Msg), +(n(a, #1:Fresh)), generatedByIntruder(#7:Enc), -(n(a, #1:Fresh)), -(#7:Enc), +(n(a, #1:Fresh) ; #7:Enc), -(b), -(n(a, #1:Fresh) ; #7:Enc), +(b ; n(a, #1:Fresh) ; #7:Enc), -(b ; n(a, #1:Fresh) ; #7:Enc), +(sign(b ; n(a, #1:Fresh) ; #7:Enc, i)), -(sign(b ; n(a, #1:Fresh) ; #7:Enc, i)), +(sign(n(a, #1:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(b, #6:Fresh), pkey(i, b)), s), b)), -(sign(n(a, #1:Fresh) ; n(b, #5:Fresh) ; pke(#8:HEnc, s), b)), +(sign(a ; b ; n(a, #1:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s) ; pke(#8:HEnc, s), a)), -(sign(a ; b ; n(a, #1:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s) ; pke(#8:HEnc, s), a)), +(sign(a ; b ; n(a, #1:Fresh) ; n(b, #5:Fresh) ; f(hpke(data(a, #4:Fresh), pkey(a, b)), #8:HEnc), s)), -(sign(a ; b ; n(a, #1:Fresh) ; n(b, #5:Fresh) ; #9:HEnc, s)) || nil || never((#10:StrandSet & :: #11:Fresh,#12:Fresh :: [ nil | -(sign(b ; n(a, #1:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s), a)), +(sign(n(a, #1:Fresh) ; n(b, #11:Fresh) ; pke(hpke(data(b, #12:Fresh), pkey(a, b)), s), b)), nil] ) || #13:IntruderKnowledge)) < 1 . 6 . 2 . 7 . 3 . 2 . 3 . 4 . 2 . 8 > ( :: nil :: [ nil | -(b), -(n(a, #2:Fresh) ; #7:Enc), +(b ; n(a, #2:Fresh) ; #7:Enc), nil] & :: nil :: [ nil | -(n(a, #2:Fresh)), -(#7:Enc), +(n(a, #2:Fresh) ; #7:Enc), nil] & :: nil :: [ nil | -(b ; n(a, #2:Fresh) ; #7:Enc), +(sign(b ; n(a, #2:Fresh) ; #7:Enc, i)), nil] & :: nil :: [ nil | -(#1:Msg ; n(a, #2:Fresh) ; #3:Msg), +(n(a, #2:Fresh) ; #3:Msg), nil] & :: nil :: [ nil | -(#0:Msg ; #1:Msg ; n(a, #2:Fresh) ; #3:Msg), +(#1:Msg ; n(a, #2:Fresh) ; #3:Msg), nil] & :: nil :: [ nil | -(n(a, #2:Fresh) ; #3:Msg), +(n(a, #2:Fresh)), nil] & :: nil :: [ nil | -(sign(a ; b ; n(a, #2:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s) ; pke(#8:HEnc, s), a)), +(sign(a ; b ; n(a, #2:Fresh) ; n(b, #5:Fresh) ; f(hpke(data(a, #4:Fresh), pkey(a, b)), #8:HEnc), s)), nil] & :: #2:Fresh,#4:Fresh :: [ nil, +(sign(b ; n(a, #2:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s), a)) | -(sign(n(a, #2:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(b, #6:Fresh), pkey(i, b)), s), b)), +(sign(a ; b ; n(a, #2:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s) ; pke(hpke(data(b, #6:Fresh), pkey(i, b)), s), a)), -(sign(a ; b ; n(a, #2:Fresh) ; n(b, #5:Fresh) ; f(hpke(data(a, #4:Fresh), pkey(a, b)), hpke(data(b, #6:Fresh), pkey(i, b))), s)), nil] & :: #5:Fresh,#6:Fresh :: [ nil | -(sign(b ; n(a, #2:Fresh) ; #7:Enc, i)), +(sign(n(a, #2:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(b, #6:Fresh), pkey(i, b)), s), b)), nil] ) || #7:Enc !inI, n(a, #2:Fresh) !inI, (b ; n(a, #2:Fresh) ; #7:Enc) !inI, (#1:Msg ; n(a, #2:Fresh) ; #3:Msg) !inI, (n(a, #2:Fresh) ; #3:Msg) !inI, (n(a, #2:Fresh) ; #7:Enc) !inI, sign(a ; b ; n(a, #2:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s) ; pke(#8:HEnc, s), a) !inI, sign(a ; b ; n(a, #2:Fresh) ; n(b, #5:Fresh) ; f(hpke(data(a, #4:Fresh), pkey(a, b)), #8:HEnc), s) !inI, sign(b ; n(a, #2:Fresh) ; #7:Enc, i) !inI, sign(n(a, #2:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(b, #6:Fresh), pkey(i, b)), s), b) !inI, (#0:Msg ; #1:Msg ; n(a, #2:Fresh) ; #3:Msg) inI, inst(#8:HEnc) || -(#0:Msg ; #1:Msg ; n(a, #2:Fresh) ; #3:Msg), +(#1:Msg ; n(a, #2:Fresh) ; #3:Msg), -(#1:Msg ; n(a, #2:Fresh) ; #3:Msg), +(n(a, #2:Fresh) ; #3:Msg), -(n(a, #2:Fresh) ; #3:Msg), +(n(a, #2:Fresh)), generatedByIntruder(#7:Enc), -(n(a, #2:Fresh)), -(#7:Enc), +(n(a, #2:Fresh) ; #7:Enc), -(b), -(n(a, #2:Fresh) ; #7:Enc), +(b ; n(a, #2:Fresh) ; #7:Enc), -(b ; n(a, #2:Fresh) ; #7:Enc), +(sign(b ; n(a, #2:Fresh) ; #7:Enc, i)), -(sign(b ; n(a, #2:Fresh) ; #7:Enc, i)), +(sign(n(a, #2:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(b, #6:Fresh), pkey(i, b)), s), b)), -(sign(n(a, #2:Fresh) ; n(b, #5:Fresh) ; pke(#8:HEnc, s), b)), +(sign(a ; b ; n(a, #2:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s) ; pke(#8:HEnc, s), a)), -(sign(a ; b ; n(a, #2:Fresh) ; n(b, #5:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s) ; pke(#8:HEnc, s), a)), +(sign(a ; b ; n(a, #2:Fresh) ; n(b, #5:Fresh) ; f(hpke(data(a, #4:Fresh), pkey(a, b)), #8:HEnc), s)), -(sign(a ; b ; n(a, #2:Fresh) ; n(b, #5:Fresh) ; #9:HEnc, s)) || nil || never((#10:StrandSet & :: #11:Fresh,#12:Fresh :: [ nil | -(sign(b ; n(a, #2:Fresh) ; pke(hpke(data(a, #4:Fresh), pkey(a, b)), s), a)), +(sign(n(a, #2:Fresh) ; n(b, #11:Fresh) ; pke(hpke(data(b, #12:Fresh), pkey(a, b)), s), b)), nil] ) || #13:IntruderKnowledge) ========================================== reduce in MAUDE-NPA : run(10) . rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second) result IdSystemSet: (< 1 . 6 . 2 . 7 . 3 . 2 . 3 . 4 . 2 . 7 . 1 > ( :: nil :: [ nil | -(b), -(n(a, #0:Fresh) ; #4:Enc), +(b ; n(a, #0:Fresh) ; #4:Enc), nil] & :: nil :: [ nil | -(n(a, #0:Fresh)), -(#4:Enc), +(n(a, #0:Fresh) ; #4:Enc), nil] & :: nil :: [ nil | -(b ; n(a, #0:Fresh) ; #4:Enc), +(sign(b ; n(a, #0:Fresh) ; #4:Enc, i)), nil] & :: nil :: [ nil | -(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), +(n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), nil] & :: nil :: [ nil | -(n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), +(n(a, #0:Fresh)), nil] & :: nil :: [ nil | -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; f(hpke(data(a, #1:Fresh), pkey(a, b)), #5:HEnc), s)), nil] & :: nil :: [ nil | -(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a)), +(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), nil] & :: #1:Fresh,#0:Fresh :: [ nil | +(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a)), -(sign(n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(b, #3:Fresh), pkey(i, b)), s), b)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; pke(hpke(data(b, #3:Fresh), pkey(i, b)), s), a)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; f(hpke(data(a, #1:Fresh), pkey(a, b)), hpke(data(b, #3:Fresh), pkey(i, b))), s)), nil] & :: #2:Fresh,#3:Fresh :: [ nil | -(sign(b ; n(a, #0:Fresh) ; #4:Enc, i)), +(sign(n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(b, #3:Fresh), pkey(i, b)), s), b)), nil] ) || #4:Enc !inI, n(a, #0:Fresh) !inI, (b ; n(a, #0:Fresh) ; #4:Enc) !inI, (b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)) !inI, (n(a, #0:Fresh) ; #4:Enc) !inI, (n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)) !inI, sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a) !inI, sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; f(hpke(data(a, #1:Fresh), pkey(a, b)), #5:HEnc), s) !inI, sign(b ; n(a, #0:Fresh) ; #4:Enc, i) !inI, sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a) !inI, sign(n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(b, #3:Fresh), pkey(i, b)), s), b) !inI, inst(#5:HEnc) || +(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a)), -(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a)), +(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), -(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), +(n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), -(n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), +(n(a, #0:Fresh)), generatedByIntruder(#4:Enc), -(n(a, #0:Fresh)), -(#4:Enc), +(n(a, #0:Fresh) ; #4:Enc), -(b), -(n(a, #0:Fresh) ; #4:Enc), +(b ; n(a, #0:Fresh) ; #4:Enc), -(b ; n(a, #0:Fresh) ; #4:Enc), +(sign(b ; n(a, #0:Fresh) ; #4:Enc, i)), -(sign(b ; n(a, #0:Fresh) ; #4:Enc, i)), +(sign(n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(b, #3:Fresh), pkey(i, b)), s), b)), -(sign(n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(#5:HEnc, s), b)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; f(hpke(data(a, #1:Fresh), pkey(a, b)), #5:HEnc), s)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; #6:HEnc, s)) || nil || never((#7:StrandSet & :: #8:Fresh,#9:Fresh :: [ nil | -(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a)), +(sign(n(a, #0:Fresh) ; n(b, #8:Fresh) ; pke(hpke(data(b, #9:Fresh), pkey(a, b)), s), b)), nil] ) || #10:IntruderKnowledge)) (< 1 . 6 . 2 . 7 . 3 . 2 . 3 . 4 . 2 . 8 . 7 > ( :: nil :: [ nil | -(b), -(n(a, #2:Fresh) ; #8:Enc), +(b ; n(a, #2:Fresh) ; #8:Enc), nil] & :: nil :: [ nil | -(n(a, #2:Fresh)), -(#8:Enc), +(n(a, #2:Fresh) ; #8:Enc), nil] & :: nil :: [ nil | -(b ; n(a, #2:Fresh) ; #8:Enc), +(sign(b ; n(a, #2:Fresh) ; #8:Enc, i)), nil] & :: nil :: [ nil | -(#1:Msg ; n(a, #2:Fresh) ; #3:Msg), +(n(a, #2:Fresh) ; #3:Msg), nil] & :: nil :: [ nil | -(#0:Msg ; #1:Msg ; n(a, #2:Fresh) ; #3:Msg), +(#1:Msg ; n(a, #2:Fresh) ; #3:Msg), nil] & :: nil :: [ nil | -(n(a, #2:Fresh) ; #3:Msg), +(n(a, #2:Fresh)), nil] & :: nil :: [ nil | -(sign(a ; b ; n(a, #2:Fresh) ; n(b, #6:Fresh) ; pke(hpke(data(a, #5:Fresh), pkey(a, b)), s) ; pke(#9:HEnc, s), a)), +(sign(a ; b ; n(a, #2:Fresh) ; n(b, #6:Fresh) ; f(hpke(data(a, #5:Fresh), pkey(a, b)), #9:HEnc), s)), nil] & :: nil :: [ nil | -(sign(#0:Msg ; #1:Msg ; n(a, #2:Fresh) ; #3:Msg, #4:Name)), +(#0:Msg ; #1:Msg ; n(a, #2:Fresh) ; #3:Msg), nil] & :: #2:Fresh,#5:Fresh :: [ nil, +(sign(b ; n(a, #2:Fresh) ; pke(hpke(data(a, #5:Fresh), pkey(a, b)), s), a)) | -(sign(n(a, #2:Fresh) ; n(b, #6:Fresh) ; pke(hpke(data(b, #7:Fresh), pkey(i, b)), s), b)), +(sign(a ; b ; n(a, #2:Fresh) ; n(b, #6:Fresh) ; pke(hpke(data(a, #5:Fresh), pkey(a, b)), s) ; pke(hpke(data(b, #7:Fresh), pkey(i, b)), s), a)), -(sign(a ; b ; n(a, #2:Fresh) ; n(b, #6:Fresh) ; f(hpke(data(a, #5:Fresh), pkey(a, b)), hpke(data(b, #7:Fresh), pkey(i, b))), s)), nil] & :: #6:Fresh,#7:Fresh :: [ nil | -(sign(b ; n(a, #2:Fresh) ; #8:Enc, i)), +(sign(n(a, #2:Fresh) ; n(b, #6:Fresh) ; pke(hpke(data(b, #7:Fresh), pkey(i, b)), s), b)), nil] ) || #8:Enc !inI, n(a, #2:Fresh) !inI, (b ; n(a, #2:Fresh) ; #8:Enc) !inI, (#1:Msg ; n(a, #2:Fresh) ; #3:Msg) !inI, (#0:Msg ; #1:Msg ; n(a, #2:Fresh) ; #3:Msg) !inI, (n(a, #2:Fresh) ; #3:Msg) !inI, (n(a, #2:Fresh) ; #8:Enc) !inI, sign(a ; b ; n(a, #2:Fresh) ; n(b, #6:Fresh) ; pke(hpke(data(a, #5:Fresh), pkey(a, b)), s) ; pke(#9:HEnc, s), a) !inI, sign(a ; b ; n(a, #2:Fresh) ; n(b, #6:Fresh) ; f(hpke(data(a, #5:Fresh), pkey(a, b)), #9:HEnc), s) !inI, sign(b ; n(a, #2:Fresh) ; #8:Enc, i) !inI, sign(n(a, #2:Fresh) ; n(b, #6:Fresh) ; pke(hpke(data(b, #7:Fresh), pkey(i, b)), s), b) !inI, sign(#0:Msg ; #1:Msg ; n(a, #2:Fresh) ; #3:Msg, #4:Name) inI, inst(#9:HEnc) || -(sign(#0:Msg ; #1:Msg ; n(a, #2:Fresh) ; #3:Msg, #4:Name)), +(#0:Msg ; #1:Msg ; n(a, #2:Fresh) ; #3:Msg), -(#0:Msg ; #1:Msg ; n(a, #2:Fresh) ; #3:Msg), +(#1:Msg ; n(a, #2:Fresh) ; #3:Msg), -(#1:Msg ; n(a, #2:Fresh) ; #3:Msg), +(n(a, #2:Fresh) ; #3:Msg), -(n(a, #2:Fresh) ; #3:Msg), +(n(a, #2:Fresh)), generatedByIntruder(#8:Enc), -(n(a, #2:Fresh)), -(#8:Enc), +(n(a, #2:Fresh) ; #8:Enc), -(b), -(n(a, #2:Fresh) ; #8:Enc), +(b ; n(a, #2:Fresh) ; #8:Enc), -(b ; n(a, #2:Fresh) ; #8:Enc), +(sign(b ; n(a, #2:Fresh) ; #8:Enc, i)), -(sign(b ; n(a, #2:Fresh) ; #8:Enc, i)), +(sign(n(a, #2:Fresh) ; n(b, #6:Fresh) ; pke(hpke(data(b, #7:Fresh), pkey(i, b)), s), b)), -(sign(n(a, #2:Fresh) ; n(b, #6:Fresh) ; pke(#9:HEnc, s), b)), +(sign(a ; b ; n(a, #2:Fresh) ; n(b, #6:Fresh) ; pke(hpke(data(a, #5:Fresh), pkey(a, b)), s) ; pke(#9:HEnc, s), a)), -(sign(a ; b ; n(a, #2:Fresh) ; n(b, #6:Fresh) ; pke(hpke(data(a, #5:Fresh), pkey(a, b)), s) ; pke(#9:HEnc, s), a)), +(sign(a ; b ; n(a, #2:Fresh) ; n(b, #6:Fresh) ; f(hpke(data(a, #5:Fresh), pkey(a, b)), #9:HEnc), s)), -(sign(a ; b ; n(a, #2:Fresh) ; n(b, #6:Fresh) ; #10:HEnc, s)) || nil || never((#11:StrandSet & :: #12:Fresh,#13:Fresh :: [ nil | -(sign(b ; n(a, #2:Fresh) ; pke(hpke(data(a, #5:Fresh), pkey(a, b)), s), a)), +(sign(n(a, #2:Fresh) ; n(b, #12:Fresh) ; pke(hpke(data(b, #13:Fresh), pkey(a, b)), s), b)), nil] ) || #14:IntruderKnowledge)) < 1 . 6 . 2 . 7 . 3 . 2 . 3 . 4 . 2 . 8 . 8 > ( :: nil :: [ nil | -(b), -(n(a, #3:Fresh) ; #8:Enc), +(b ; n(a, #3:Fresh) ; #8:Enc), nil] & :: nil :: [ nil | -(n(a, #3:Fresh)), -(#8:Enc), +(n(a, #3:Fresh) ; #8:Enc), nil] & :: nil :: [ nil | -(b ; n(a, #3:Fresh) ; #8:Enc), +(sign(b ; n(a, #3:Fresh) ; #8:Enc, i)), nil] & :: nil :: [ nil | -(#1:Msg ; #2:Msg ; n(a, #3:Fresh) ; #4:Msg), +(#2:Msg ; n(a, #3:Fresh) ; #4:Msg), nil] & :: nil :: [ nil | -(#2:Msg ; n(a, #3:Fresh) ; #4:Msg), +(n(a, #3:Fresh) ; #4:Msg), nil] & :: nil :: [ nil | -(#0:Msg ; #1:Msg ; #2:Msg ; n(a, #3:Fresh) ; #4:Msg), +(#1:Msg ; #2:Msg ; n(a, #3:Fresh) ; #4:Msg), nil] & :: nil :: [ nil | -(n(a, #3:Fresh) ; #4:Msg), +(n(a, #3:Fresh)), nil] & :: nil :: [ nil | -(sign(a ; b ; n(a, #3:Fresh) ; n(b, #6:Fresh) ; pke(hpke(data(a, #5:Fresh), pkey(a, b)), s) ; pke(#9:HEnc, s), a)), +(sign(a ; b ; n(a, #3:Fresh) ; n(b, #6:Fresh) ; f(hpke(data(a, #5:Fresh), pkey(a, b)), #9:HEnc), s)), nil] & :: #3:Fresh,#5:Fresh :: [ nil, +(sign(b ; n(a, #3:Fresh) ; pke(hpke(data(a, #5:Fresh), pkey(a, b)), s), a)) | -(sign(n(a, #3:Fresh) ; n(b, #6:Fresh) ; pke(hpke(data(b, #7:Fresh), pkey(i, b)), s), b)), +(sign(a ; b ; n(a, #3:Fresh) ; n(b, #6:Fresh) ; pke(hpke(data(a, #5:Fresh), pkey(a, b)), s) ; pke(hpke(data(b, #7:Fresh), pkey(i, b)), s), a)), -(sign(a ; b ; n(a, #3:Fresh) ; n(b, #6:Fresh) ; f(hpke(data(a, #5:Fresh), pkey(a, b)), hpke(data(b, #7:Fresh), pkey(i, b))), s)), nil] & :: #6:Fresh,#7:Fresh :: [ nil | -(sign(b ; n(a, #3:Fresh) ; #8:Enc, i)), +(sign(n(a, #3:Fresh) ; n(b, #6:Fresh) ; pke(hpke(data(b, #7:Fresh), pkey(i, b)), s), b)), nil] ) || #8:Enc !inI, n(a, #3:Fresh) !inI, (b ; n(a, #3:Fresh) ; #8:Enc) !inI, (#1:Msg ; #2:Msg ; n(a, #3:Fresh) ; #4:Msg) !inI, (#2:Msg ; n(a, #3:Fresh) ; #4:Msg) !inI, (n(a, #3:Fresh) ; #4:Msg) !inI, (n(a, #3:Fresh) ; #8:Enc) !inI, sign(a ; b ; n(a, #3:Fresh) ; n(b, #6:Fresh) ; pke(hpke(data(a, #5:Fresh), pkey(a, b)), s) ; pke(#9:HEnc, s), a) !inI, sign(a ; b ; n(a, #3:Fresh) ; n(b, #6:Fresh) ; f(hpke(data(a, #5:Fresh), pkey(a, b)), #9:HEnc), s) !inI, sign(b ; n(a, #3:Fresh) ; #8:Enc, i) !inI, sign(n(a, #3:Fresh) ; n(b, #6:Fresh) ; pke(hpke(data(b, #7:Fresh), pkey(i, b)), s), b) !inI, (#0:Msg ; #1:Msg ; #2:Msg ; n(a, #3:Fresh) ; #4:Msg) inI, inst(#9:HEnc) || -(#0:Msg ; #1:Msg ; #2:Msg ; n(a, #3:Fresh) ; #4:Msg), +(#1:Msg ; #2:Msg ; n(a, #3:Fresh) ; #4:Msg), -(#1:Msg ; #2:Msg ; n(a, #3:Fresh) ; #4:Msg), +(#2:Msg ; n(a, #3:Fresh) ; #4:Msg), -(#2:Msg ; n(a, #3:Fresh) ; #4:Msg), +(n(a, #3:Fresh) ; #4:Msg), -(n(a, #3:Fresh) ; #4:Msg), +(n(a, #3:Fresh)), generatedByIntruder(#8:Enc), -(n(a, #3:Fresh)), -(#8:Enc), +(n(a, #3:Fresh) ; #8:Enc), -(b), -(n(a, #3:Fresh) ; #8:Enc), +(b ; n(a, #3:Fresh) ; #8:Enc), -(b ; n(a, #3:Fresh) ; #8:Enc), +(sign(b ; n(a, #3:Fresh) ; #8:Enc, i)), -(sign(b ; n(a, #3:Fresh) ; #8:Enc, i)), +(sign(n(a, #3:Fresh) ; n(b, #6:Fresh) ; pke(hpke(data(b, #7:Fresh), pkey(i, b)), s), b)), -(sign(n(a, #3:Fresh) ; n(b, #6:Fresh) ; pke(#9:HEnc, s), b)), +(sign(a ; b ; n(a, #3:Fresh) ; n(b, #6:Fresh) ; pke(hpke(data(a, #5:Fresh), pkey(a, b)), s) ; pke(#9:HEnc, s), a)), -(sign(a ; b ; n(a, #3:Fresh) ; n(b, #6:Fresh) ; pke(hpke(data(a, #5:Fresh), pkey(a, b)), s) ; pke(#9:HEnc, s), a)), +(sign(a ; b ; n(a, #3:Fresh) ; n(b, #6:Fresh) ; f(hpke(data(a, #5:Fresh), pkey(a, b)), #9:HEnc), s)), -(sign(a ; b ; n(a, #3:Fresh) ; n(b, #6:Fresh) ; #10:HEnc, s)) || nil || never((#11:StrandSet & :: #12:Fresh,#13:Fresh :: [ nil | -(sign(b ; n(a, #3:Fresh) ; pke(hpke(data(a, #5:Fresh), pkey(a, b)), s), a)), +(sign(n(a, #3:Fresh) ; n(b, #12:Fresh) ; pke(hpke(data(b, #13:Fresh), pkey(a, b)), s), b)), nil] ) || #14:IntruderKnowledge) ========================================== reduce in MAUDE-NPA : run(11) . rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second) result IdSystemSet: (< 1 . 6 . 2 . 7 . 3 . 2 . 3 . 4 . 2 . 7 . 1 > ( :: nil :: [ nil | -(b), -(n(a, #0:Fresh) ; #4:Enc), +(b ; n(a, #0:Fresh) ; #4:Enc), nil] & :: nil :: [ nil | -(n(a, #0:Fresh)), -(#4:Enc), +(n(a, #0:Fresh) ; #4:Enc), nil] & :: nil :: [ nil | -(b ; n(a, #0:Fresh) ; #4:Enc), +(sign(b ; n(a, #0:Fresh) ; #4:Enc, i)), nil] & :: nil :: [ nil | -(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), +(n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), nil] & :: nil :: [ nil | -(n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), +(n(a, #0:Fresh)), nil] & :: nil :: [ nil | -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; f(hpke(data(a, #1:Fresh), pkey(a, b)), #5:HEnc), s)), nil] & :: nil :: [ nil | -(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a)), +(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), nil] & :: #1:Fresh,#0:Fresh :: [ nil | +(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a)), -(sign(n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(b, #3:Fresh), pkey(i, b)), s), b)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; pke(hpke(data(b, #3:Fresh), pkey(i, b)), s), a)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; f(hpke(data(a, #1:Fresh), pkey(a, b)), hpke(data(b, #3:Fresh), pkey(i, b))), s)), nil] & :: #2:Fresh,#3:Fresh :: [ nil | -(sign(b ; n(a, #0:Fresh) ; #4:Enc, i)), +(sign(n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(b, #3:Fresh), pkey(i, b)), s), b)), nil] ) || #4:Enc !inI, n(a, #0:Fresh) !inI, (b ; n(a, #0:Fresh) ; #4:Enc) !inI, (b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)) !inI, (n(a, #0:Fresh) ; #4:Enc) !inI, (n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)) !inI, sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a) !inI, sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; f(hpke(data(a, #1:Fresh), pkey(a, b)), #5:HEnc), s) !inI, sign(b ; n(a, #0:Fresh) ; #4:Enc, i) !inI, sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a) !inI, sign(n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(b, #3:Fresh), pkey(i, b)), s), b) !inI, inst(#5:HEnc) || +(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a)), -(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a)), +(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), -(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), +(n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), -(n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), +(n(a, #0:Fresh)), generatedByIntruder(#4:Enc), -(n(a, #0:Fresh)), -(#4:Enc), +(n(a, #0:Fresh) ; #4:Enc), -(b), -(n(a, #0:Fresh) ; #4:Enc), +(b ; n(a, #0:Fresh) ; #4:Enc), -(b ; n(a, #0:Fresh) ; #4:Enc), +(sign(b ; n(a, #0:Fresh) ; #4:Enc, i)), -(sign(b ; n(a, #0:Fresh) ; #4:Enc, i)), +(sign(n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(b, #3:Fresh), pkey(i, b)), s), b)), -(sign(n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(#5:HEnc, s), b)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; f(hpke(data(a, #1:Fresh), pkey(a, b)), #5:HEnc), s)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; #6:HEnc, s)) || nil || never((#7:StrandSet & :: #8:Fresh,#9:Fresh :: [ nil | -(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a)), +(sign(n(a, #0:Fresh) ; n(b, #8:Fresh) ; pke(hpke(data(b, #9:Fresh), pkey(a, b)), s), b)), nil] ) || #10:IntruderKnowledge)) < 1 . 6 . 2 . 7 . 3 . 2 . 3 . 4 . 2 . 8 . 8 . 7 > ( :: nil :: [ nil | -(b), -(n(a, #3:Fresh) ; #9:Enc), +(b ; n(a, #3:Fresh) ; #9:Enc), nil] & :: nil :: [ nil | -(n(a, #3:Fresh)), -(#9:Enc), +(n(a, #3:Fresh) ; #9:Enc), nil] & :: nil :: [ nil | -(b ; n(a, #3:Fresh) ; #9:Enc), +(sign(b ; n(a, #3:Fresh) ; #9:Enc, i)), nil] & :: nil :: [ nil | -(#1:Msg ; #2:Msg ; n(a, #3:Fresh) ; #4:Msg), +(#2:Msg ; n(a, #3:Fresh) ; #4:Msg), nil] & :: nil :: [ nil | -(#2:Msg ; n(a, #3:Fresh) ; #4:Msg), +(n(a, #3:Fresh) ; #4:Msg), nil] & :: nil :: [ nil | -(#0:Msg ; #1:Msg ; #2:Msg ; n(a, #3:Fresh) ; #4:Msg), +(#1:Msg ; #2:Msg ; n(a, #3:Fresh) ; #4:Msg), nil] & :: nil :: [ nil | -(n(a, #3:Fresh) ; #4:Msg), +(n(a, #3:Fresh)), nil] & :: nil :: [ nil | -(sign(a ; b ; n(a, #3:Fresh) ; n(b, #7:Fresh) ; pke(hpke(data(a, #6:Fresh), pkey(a, b)), s) ; pke(#10:HEnc, s), a)), +(sign(a ; b ; n(a, #3:Fresh) ; n(b, #7:Fresh) ; f(hpke(data(a, #6:Fresh), pkey(a, b)), #10:HEnc), s)), nil] & :: nil :: [ nil | -(sign(#0:Msg ; #1:Msg ; #2:Msg ; n(a, #3:Fresh) ; #4:Msg, #5:Name)), +(#0:Msg ; #1:Msg ; #2:Msg ; n(a, #3:Fresh) ; #4:Msg), nil] & :: #3:Fresh,#6:Fresh :: [ nil, +(sign(b ; n(a, #3:Fresh) ; pke(hpke(data(a, #6:Fresh), pkey(a, b)), s), a)) | -(sign(n(a, #3:Fresh) ; n(b, #7:Fresh) ; pke(hpke(data(b, #8:Fresh), pkey(i, b)), s), b)), +(sign(a ; b ; n(a, #3:Fresh) ; n(b, #7:Fresh) ; pke(hpke(data(a, #6:Fresh), pkey(a, b)), s) ; pke(hpke(data(b, #8:Fresh), pkey(i, b)), s), a)), -(sign(a ; b ; n(a, #3:Fresh) ; n(b, #7:Fresh) ; f(hpke(data(a, #6:Fresh), pkey(a, b)), hpke(data(b, #8:Fresh), pkey(i, b))), s)), nil] & :: #7:Fresh,#8:Fresh :: [ nil | -(sign(b ; n(a, #3:Fresh) ; #9:Enc, i)), +(sign(n(a, #3:Fresh) ; n(b, #7:Fresh) ; pke(hpke(data(b, #8:Fresh), pkey(i, b)), s), b)), nil] ) || #9:Enc !inI, n(a, #3:Fresh) !inI, (b ; n(a, #3:Fresh) ; #9:Enc) !inI, (#1:Msg ; #2:Msg ; n(a, #3:Fresh) ; #4:Msg) !inI, (#2:Msg ; n(a, #3:Fresh) ; #4:Msg) !inI, (#0:Msg ; #1:Msg ; #2:Msg ; n(a, #3:Fresh) ; #4:Msg) !inI, (n(a, #3:Fresh) ; #4:Msg) !inI, (n(a, #3:Fresh) ; #9:Enc) !inI, sign(a ; b ; n(a, #3:Fresh) ; n(b, #7:Fresh) ; pke(hpke(data(a, #6:Fresh), pkey(a, b)), s) ; pke(#10:HEnc, s), a) !inI, sign(a ; b ; n(a, #3:Fresh) ; n(b, #7:Fresh) ; f(hpke(data(a, #6:Fresh), pkey(a, b)), #10:HEnc), s) !inI, sign(b ; n(a, #3:Fresh) ; #9:Enc, i) !inI, sign(n(a, #3:Fresh) ; n(b, #7:Fresh) ; pke(hpke(data(b, #8:Fresh), pkey(i, b)), s), b) !inI, sign(#0:Msg ; #1:Msg ; #2:Msg ; n(a, #3:Fresh) ; #4:Msg, #5:Name) inI, inst(#10:HEnc) || -(sign(#0:Msg ; #1:Msg ; #2:Msg ; n(a, #3:Fresh) ; #4:Msg, #5:Name)), +(#0:Msg ; #1:Msg ; #2:Msg ; n(a, #3:Fresh) ; #4:Msg), -(#0:Msg ; #1:Msg ; #2:Msg ; n(a, #3:Fresh) ; #4:Msg), +(#1:Msg ; #2:Msg ; n(a, #3:Fresh) ; #4:Msg), -(#1:Msg ; #2:Msg ; n(a, #3:Fresh) ; #4:Msg), +(#2:Msg ; n(a, #3:Fresh) ; #4:Msg), -(#2:Msg ; n(a, #3:Fresh) ; #4:Msg), +(n(a, #3:Fresh) ; #4:Msg), -(n(a, #3:Fresh) ; #4:Msg), +(n(a, #3:Fresh)), generatedByIntruder(#9:Enc), -(n(a, #3:Fresh)), -(#9:Enc), +(n(a, #3:Fresh) ; #9:Enc), -(b), -(n(a, #3:Fresh) ; #9:Enc), +(b ; n(a, #3:Fresh) ; #9:Enc), -(b ; n(a, #3:Fresh) ; #9:Enc), +(sign(b ; n(a, #3:Fresh) ; #9:Enc, i)), -(sign(b ; n(a, #3:Fresh) ; #9:Enc, i)), +(sign(n(a, #3:Fresh) ; n(b, #7:Fresh) ; pke(hpke(data(b, #8:Fresh), pkey(i, b)), s), b)), -(sign(n(a, #3:Fresh) ; n(b, #7:Fresh) ; pke(#10:HEnc, s), b)), +(sign(a ; b ; n(a, #3:Fresh) ; n(b, #7:Fresh) ; pke(hpke(data(a, #6:Fresh), pkey(a, b)), s) ; pke(#10:HEnc, s), a)), -(sign(a ; b ; n(a, #3:Fresh) ; n(b, #7:Fresh) ; pke(hpke(data(a, #6:Fresh), pkey(a, b)), s) ; pke(#10:HEnc, s), a)), +(sign(a ; b ; n(a, #3:Fresh) ; n(b, #7:Fresh) ; f(hpke(data(a, #6:Fresh), pkey(a, b)), #10:HEnc), s)), -(sign(a ; b ; n(a, #3:Fresh) ; n(b, #7:Fresh) ; #11:HEnc, s)) || nil || never((#12:StrandSet & :: #13:Fresh,#14:Fresh :: [ nil | -(sign(b ; n(a, #3:Fresh) ; pke(hpke(data(a, #6:Fresh), pkey(a, b)), s), a)), +(sign(n(a, #3:Fresh) ; n(b, #13:Fresh) ; pke(hpke(data(b, #14:Fresh), pkey(a, b)), s), b)), nil] ) || #15:IntruderKnowledge) ========================================== reduce in MAUDE-NPA : run(12) . rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second) result IdSystem: < 1 . 6 . 2 . 7 . 3 . 2 . 3 . 4 . 2 . 7 . 1 > ( :: nil :: [ nil | -(b), -(n(a, #0:Fresh) ; #4:Enc), +(b ; n(a, #0:Fresh) ; #4:Enc), nil] & :: nil :: [ nil | -(n(a, #0:Fresh)), -(#4:Enc), +(n(a, #0:Fresh) ; #4:Enc), nil] & :: nil :: [ nil | -(b ; n(a, #0:Fresh) ; #4:Enc), +(sign(b ; n(a, #0:Fresh) ; #4:Enc, i)), nil] & :: nil :: [ nil | -(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), +(n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), nil] & :: nil :: [ nil | -(n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), +(n(a, #0:Fresh)), nil] & :: nil :: [ nil | -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; f(hpke(data(a, #1:Fresh), pkey(a, b)), #5:HEnc), s)), nil] & :: nil :: [ nil | -(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a)), +(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), nil] & :: #1:Fresh,#0:Fresh :: [ nil | +(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a)), -(sign(n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(b, #3:Fresh), pkey(i, b)), s), b)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; pke(hpke(data(b, #3:Fresh), pkey(i, b)), s), a)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; f(hpke(data(a, #1:Fresh), pkey(a, b)), hpke(data(b, #3:Fresh), pkey(i, b))), s)), nil] & :: #2:Fresh,#3:Fresh :: [ nil | -(sign(b ; n(a, #0:Fresh) ; #4:Enc, i)), +(sign(n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(b, #3:Fresh), pkey(i, b)), s), b)), nil] ) || #4:Enc !inI, n(a, #0:Fresh) !inI, (b ; n(a, #0:Fresh) ; #4:Enc) !inI, (b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)) !inI, (n(a, #0:Fresh) ; #4:Enc) !inI, (n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)) !inI, sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a) !inI, sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; f(hpke(data(a, #1:Fresh), pkey(a, b)), #5:HEnc), s) !inI, sign(b ; n(a, #0:Fresh) ; #4:Enc, i) !inI, sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a) !inI, sign(n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(b, #3:Fresh), pkey(i, b)), s), b) !inI, inst(#5:HEnc) || +(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a)), -(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a)), +(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), -(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), +(n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), -(n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s)), +(n(a, #0:Fresh)), generatedByIntruder(#4:Enc), -(n(a, #0:Fresh)), -(#4:Enc), +(n(a, #0:Fresh) ; #4:Enc), -(b), -(n(a, #0:Fresh) ; #4:Enc), +(b ; n(a, #0:Fresh) ; #4:Enc), -(b ; n(a, #0:Fresh) ; #4:Enc), +(sign(b ; n(a, #0:Fresh) ; #4:Enc, i)), -(sign(b ; n(a, #0:Fresh) ; #4:Enc, i)), +(sign(n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(b, #3:Fresh), pkey(i, b)), s), b)), -(sign(n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(#5:HEnc, s), b)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s) ; pke(#5:HEnc, s), a)), +(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; f(hpke(data(a, #1:Fresh), pkey(a, b)), #5:HEnc), s)), -(sign(a ; b ; n(a, #0:Fresh) ; n(b, #2:Fresh) ; #6:HEnc, s)) || nil || never((#7:StrandSet & :: #8:Fresh,#9:Fresh :: [ nil | -(sign(b ; n(a, #0:Fresh) ; pke(hpke(data(a, #1:Fresh), pkey(a, b)), s), a)), +(sign(n(a, #0:Fresh) ; n(b, #8:Fresh) ; pke(hpke(data(b, #9:Fresh), pkey(a, b)), s), b)), nil] ) || #10:IntruderKnowledge) Maude> Bye. Wed Dec 5 10:57:36 CET 2012 Santiagos-MacBook-Pro:prototype-20121204 sescobar$