Tue Apr 24 18:56:41 CEST 2018
		     \||||||||||||||||||/
		   --- Welcome to Maude ---
		     /||||||||||||||||||\
	   Maude alpha116 built: Mar 16 2018 17:40:28
	    Copyright 1997-2017 SRI International
		   Tue Apr 24 18:56:41 2018

	    Maude-NPA Version: 3.1.1 (April 24th 2018)
	    with direct composition and irreducibility constraints
	    (To be run with Maude alpha 115 or above)
	    Copyright (c) 2018, University of Illinois
	    All rights reserved.

 Commands:
 red unification? .           returns the unification algorithm to be used
 red new-strands? .           returns the actual protocol strands
 red displayGrammars .        for generating grammars
 red run(X,Y).                for Y backwards analysis steps for attack pattern
    X
 red debug(X,Y).              more information than run command
 red digest(X,Y).             less information than run command
 red summary(X,Y).            for summary of analysis steps
 red ids(X,Y).                for set of state ids
 red initials(X,Y).           for showing only initial steps
==========================================
reduce in MAUDE-NPA : summary(0, (1).NzNat) .
rewrites: 3510055 in 11352ms cpu (39291ms real) (309201 rewrites/second)
result Summary: States>> 4 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(0, 2) .
rewrites: 1078418 in 2080ms cpu (7097ms real) (518470 rewrites/second)
result Summary: States>> 6 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(0, 3) .
rewrites: 5654122 in 7980ms cpu (25896ms real) (708536 rewrites/second)
result Summary: States>> 11 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(0, 4) .
rewrites: 30868808 in 34624ms cpu (104770ms real) (891543 rewrites/second)
result Summary: States>> 26 Solutions>> 1
==========================================
reduce in MAUDE-NPA : initials(0,4) .
rewrites: 982 in 0ms cpu (0ms real) (~ rewrites/second)
result ShortIdSystem: < 1 . 3 . 2 . 1 . 1 > (
:: nil ::
[ nil | 
   -(senc(cmode(#0:FrNonce), Fr(#1:Fresh)) ; mac(mt, Fr(#1:Fresh))), 
   +(senc(cmode(#0:FrNonce), Fr(#1:Fresh))), nil]  & 
:: nil ::
[ nil | 
   {YubiHSM -> YubiHSM ;; 1-1 ;; YSM-AEAD-GENERATE(Fr(#2:Fresh)) @ HSM(Fr(
    #2:Fresh), Fr(#1:Fresh)) |> MasterKey(Fr(#1:Fresh))}, 
   -(mt), 
   -(Fr(#2:Fresh)), 
   -(#0:FrNonce), 
   +(senc(cmode(#0:FrNonce), Fr(#1:Fresh)) ; mac(mt, Fr(#1:Fresh))), nil]  & 
:: #1:Fresh,#2:Fresh ::
[ nil | 
   +(Fr(#2:Fresh)), 
   {YubiHSM -> YubiHSM ;; 1-1 ;; YSM-AEAD-GENERATE(Fr(#2:Fresh)) @ HSM(Fr(
    #2:Fresh), Fr(#1:Fresh)) |> MasterKey(Fr(#1:Fresh))}, nil] )
| 
mt !inI,
#0:FrNonce !inI,
Fr(#2:Fresh) !inI,
(senc(cmode(#0:FrNonce), Fr(#1:Fresh)) ; mac(mt, Fr(#1:Fresh))) !inI,
senc(cmode(#0:FrNonce), Fr(#1:Fresh)) !inI
| 
+(Fr(#2:Fresh)), 
{YubiHSM -> YubiHSM ;; 1-1 ;; YSM-AEAD-GENERATE(Fr(#2:Fresh)) @ HSM(Fr(
    #2:Fresh), Fr(#1:Fresh)) |> MasterKey(Fr(#1:Fresh))}, 
generatedByIntruder(mt), 
generatedByIntruder(#0:FrNonce), 
-(mt), 
-(Fr(#2:Fresh)), 
-(#0:FrNonce), 
+(senc(cmode(#0:FrNonce), Fr(#1:Fresh)) ; mac(mt, Fr(#1:Fresh))), 
-(senc(cmode(#0:FrNonce), Fr(#1:Fresh)) ; mac(mt, Fr(#1:Fresh))), 
+(senc(cmode(#0:FrNonce), Fr(#1:Fresh)))
| 
nil
Bye.
Tue Apr 24 18:59:45 CEST 2018