***(

Munilla process specification

(Prover) :

+(n(P?,f1)@t1) ·
-(NV@t2) ·
-(s(NV' ; t(NV ; n(P?,f1) ; key(V?,P?)))@t3) ·
+(f(s(NV' ; t(NV ; n(P?,f1) ; key(V?,P?))) ; w(n(P?,f1) ; NV ; key(V?,P?)))@t4) ·
+(h(w(n(P?,f1) ; NV ; key(V?,P?)) ; key(V?,P?))@t5) ·

(Verifier) :

-(NP@t1) ·
+(n(V?,f1)@t2) ·
+(s(n(V?,f2) ; t(n(V?,f1) ; NP ; key(V?,P?)))@t3) ·
-(f(s(n(V?,f2) ; t(n(V?,f1) ; NP ; key(V?,P?))) ; w(NP ; n(V?,f1) ; key(V?,P?)))@t4) ·
if t4−t3 ≤ 2*d then -(h(w(NP ; n(V?,f1) ; key(V?,P?)) ; key(V?,P?))@t5) ·
		    +(ok@t6) 
else nilP

  )***

fmod PROTOCOL-EXAMPLE-SYMBOLS is
  --- Importing sorts Msg, Fresh, Public, and GhostData
  protecting DEFINITION-PROTOCOL-RULES .
  
  ----------------------------------------------------------
  --- Overwrite this module with the syntax of your protocol
  --- Notes:
  --- * Sort Msg and Fresh are special and imported
  --- * Every sort must be a subsort of Msg
  --- * No sort can be a supersort of Msg
  ----------------------------------------------------------

  --- Sort Information 
  sorts Name Nonce Key Honest Intruder TMsg NTMsg TimeInfo Mac NameTime NameTimeSet .
  subsort Nonce Key Mac < NTMsg . 
  subsort TMsg NTMsg Real < Msg .
  subsort Name < Key .
  subsort Name < Public .
  subsort Honest Intruder < Name .
  subsort NameTime < NameTimeSet .


  --- Nonce operator
  op n : Name Fresh -> Nonce [frozen] .
  op h : NTMsg -> NTMsg .
  op w : NTMsg -> NTMsg .
  op s : NTMsg -> NTMsg .
  op t : NTMsg -> NTMsg .
  op f : NTMsg -> NTMsg .
  op key : Name Name -> Key [comm] .
  op _;_ : NTMsg  NTMsg  -> NTMsg [gather (e E) frozen] .


  --- Ok operator
  op ok : -> NTMsg .
  
  --- Principals
  ops a b : -> Honest .
  op i : -> Intruder .
  
  --- Time messages
  op _@_ : NTMsg TimeInfo -> TMsg [metadata "grammar-arg-1" prec 50 format (d nis d d)] .

  --- Time information
  op _:_ : Name Real -> NameTime [prec 10] .
  
  op mt : -> NameTimeSet .
  op _#_ : NameTimeSet NameTimeSet -> NameTimeSet [assoc comm id: mt prec 20] .
  op _->_ : NameTime NameTimeSet -> TimeInfo .

  --- Distance
  op d : Name Name -> Real [comm] .

endfm

fmod PROTOCOL-EXAMPLE-ALGEBRAIC is
  protecting PROTOCOL-EXAMPLE-SYMBOLS .
  
  ----------------------------------------------------------
  --- Overwrite this module with the algebraic properties 
  --- of your protocol
  ----------------------------------------------------------

  eq d(A:Name,A:Name) = 0/1 . --- Simplify search


endfm

fmod PROTOCOL-SPECIFICATION is
  protecting PROTOCOL-EXAMPLE-SYMBOLS .
  protecting DEFINITION-PROTOCOL-RULES .
  protecting DEFINITION-CONSTRAINTS-INPUT .

  ----------------------------------------------------------
  --- Overwrite this module with the strands 
  --- of your protocol
  ----------------------------------------------------------
  
  var Ke : Key .
  vars X Y Z : NTMsg .
  vars r r' rA rA' rB rB' : Fresh .
  vars A B C : Name .
  var AB AB1 AB2 : Honest .
  var I : Intruder .
  vars C1 C2 C3 C4 C5 C6 C7 : Name .
  vars N NA NA' NB NB' : Nonce .
  vars d t0 t1 t2 t3 t4 t5 t6 t7 t8 t9 : Real .
  vars t0' t1' t2' t3' t4' t5' t6' t7' t8' t9' : Real .
  vars AS1 AS2 AS3 AS4 AS5 AS6 : NameTimeSet .


  eq STRANDS-DOLEVYAO
   = 
     :: nil :: [ nil | -(X @ AB1 : t1 -> AS1 # i : t2), --- Forward from honest participants
                        (t2 === t1 +=+ d(AB1,i) and d(AB1,i) >= 0/1),
                       +(X @ i : t2 -> AB2 : t3), nil ] &

     :: r ::   [ nil | +(n(i,r) @ i : t1 -> AS1), nil ] &

     :: nil :: [ nil | -(X @ C1 : t1 -> AS1 # i : t2), (t2 === t1 +=+ d(C1,i) and d(C1,i) >= 0/1),
                       -(Y @ C2 : t3 -> AS2 # i : t4), (t4 === t3 +=+ d(C2,i) and d(C2,i) >= 0/1),
                        (t5 >= t2 and t5 >= t4),
                       +((X ; Y) @ i : t5 -> AS3), nil ] &

     :: nil :: [ nil | -(X ; Y @ C1 : t1 -> AS1 # i : t2), (t2 === t1 +=+ d(C1,i) and d(C1,i) >= 0/1),
                       +(X @ i : t2 -> AS3), nil ] &

     :: nil :: [ nil | -(X ; Y @ C1 : t1 -> AS1 # i : t2), (t2 === t1 +=+ d(C1,i) and d(C1,i) >= 0/1),
                       +(Y @ i : t2 -> AS3), nil ] &  

     :: nil :: [ nil | +(key(i,AB) @ i : t1 -> AS1), nil ] &

     :: nil :: [ nil | -(X @ AB1 : t1 -> AS1 # i : t2), (t2 === t1 +=+ d(AB1,i) and d(AB1,i) >= 0/1),
                       +(h(X) @ i : t2 -> AB2 : t3), nil ] & 

     :: nil :: [ nil | -(X @ AB1 : t1 -> AS1 # i : t2), (t2 === t1 +=+ d(AB1,i) and d(AB1,i) >= 0/1),
                       +(w(X) @ i : t2 -> AB2 : t3), nil ] & 

     :: nil :: [ nil | -(X @ AB1 : t1 -> AS1 # i : t2), (t2 === t1 +=+ d(AB1,i) and d(AB1,i) >= 0/1),
                       +(f(X) @ i : t2 -> AB2 : t3), nil ] &  

     :: nil :: [ nil | -(X @ AB1 : t1 -> AS1 # i : t2), (t2 === t1 +=+ d(AB1,i) and d(AB1,i) >= 0/1),
                       +(t(X) @ i : t2 -> AB2 : t3), nil ] & 

     :: nil :: [ nil | -(X @ AB1 : t1 -> AS1 # i : t2), (t2 === t1 +=+ d(AB1,i) and d(AB1,i) >= 0/1),
                       +(s(X) @ i : t2 -> AB2 : t3), nil ] &  

     :: nil :: [ nil | +(C @ i : t1 -> AS1), nil ]  
  [nonexec] .

  eq STRANDS-PROTOCOL
   =  --- Alice --- Prover
     :: rA :: 
     [ nil | +(n(A,rA)                                                             @ A : t1 -> AS1),
             -(NB                                                                  @ C2 : t2 -> AS2 # A : t3), ((t3 === t2 +=+ d(C2,A)) and d(C2,A) > 0/1),
             -(s(NB' ; t(NB ; n(A,rA) ; key(A,B)))                                 @ C3 : t4 -> AS3 # A : t5), ((t5 === t4 +=+ d(C3,A)) and d(C3,A) > 0/1),
             +(f(s(NB' ; t(NB ; n(A,rA) ; key(A,B))) ; w(n(A,rA) ; NB ; key(A,B))) @ A : t5 -> AS4),
             +(h(w(n(A,rA) ; NB ; key(A,B)) ; key(A,B))                            @ A : t5 -> AS5),
             -(ok                                                                  @ C6 : t6 -> AS6 # A : t7), ((t7 === t6 +=+ d(C6,A)) and d(C6,A) > 0/1),  
    nil ]
     &
     ---Bob --- Verifier
     :: rB , rB' ::
     [ nil | -(NA                                                                       @ C1 : t1 -> AS1 # B : t2), ((t2 === t1 +=+ d(C1,B)) and d(C1,B) > 0/1),
             +(n(B,rB)                                                                  @ B : t2 -> AS2), 
             +(s(n(B,rB') ; t(n(B,rB) ; NA ; key(A,B)))                                 @ B : t2 -> AS3), 
             -(f(s(n(B,rB') ; t(n(B,rB) ; NA ; key(A,B))) ; w(NA ; n(B,rB) ; key(A,B))) @ C4 : t3 -> AS4 # B : t4), ((t3 >= t2 and t4 === t3 +=+ d(C4,B)) and d(C4,B) > 0/1),
																						((t4 -=- t2) <= (2/1 *=* d) and d > 0/1), --- roundtrip check 
             -(h(w(NA ; n(B,rB) ; key(A,B)) ; key(A,B)) @ C5 : t5 -> AS5 # B : t6), ((t6 === t5 +=+ d(C5,B)) and d(C5,B) > 0/1),
             +(ok @ B : t6 -> AS6),
       nil ]
  [nonexec] .


eq ATTACK-STATE(1) =  --- Mafia fraud
:: rA :: ---Alice Prover
     [ nil , +(n(a,rA)                                                                            
              @ a : t0 -> i : t1),

             -(n(b,rB)                                                                            
              @ i : t2 -> a : t3),
              (t2 >= t0), ((t3 === t2 +=+ d(a,i)) and d(a,i) > 0/1), 

             -(s(n(b,rB') ; t(n(b,rB) ; n(a,rA) ; key(a,b)))                                      
              @ i : t4 -> a : t5), 
              ((t5 === t4 +=+ d(a,i)) and d(a,i) > 0/1), 

             +(f(s(n(b,rB') ; t(n(b,rB) ; n(a,rA) ; key(a,b))) ; w(n(a,rA) ; n(b,rB) ; key(a,b))) 
              @ a : t5 -> i : t6), 

             +(h(w(n(a,rA) ; n(b,rB) ; key(a,b)) ; key(a,b))                                      
              @ a : t5 -> i : t8) 
               
     | nil ]
     &
     ---Bob --- Verifier
     :: rB , rB' ::
     [ nil , -(n(a,rA)                                                                            
              @ i : t1' -> b : t2'), 
              ((t2' === t1' +=+ d(b,i)) and d(b,i) > 0/1),

             +(n(b,rB)                                                                            
              @ b : t2' -> i : t3'), 

             +(s(n(b,rB') ; t(n(b,rB) ; n(a,rA) ; key(a,b)))                                     
              @ b : t2' -> i : t4'), 

             -(f(s(n(b,rB') ; t(n(b,rB) ; n(a,rA) ; key(a,b))) ; w(n(a,rA) ; n(b,rB) ; key(a,b))) 
              @ i : t5' -> b : t6'), 
              (t5' >= t2'), (t6' ===  t5' +=+ d(b,i) and d(b,i) > 0/1),
              ((t6' -=- t2') <= (2/1 *=* d) and d > 0/1), --- roundtrip check

             -(h(w(n(a,rA) ; n(b,rB) ; key(a,b)) ; key(a,b))                                      
              @ i : t7' -> b : t8'), 
              ((t8' === t7' +=+ d(b,i)) and d(b,i) > 0/1) 
      | nil ]
     || smt((d(a,i) +=+ d(b,i)) > d) --- empty --- Remove to find attack
     || nil
     || nil
     || nil 

[nonexec] . 
***(
maude maude maude-npa.maude Munilla.maude 
         \||||||||||||||||||/
       --- Welcome to Maude ---
         /||||||||||||||||||\
       Maude 3.1 built: Oct 12 2020 20:12:31
       Copyright 1997-2020 SRI International
       Fri Oct 23 12:39:01 2020

      Maude-NPA Version: 3.1.5 (August 9th 2020)
      with direct composition, irreducibility constraints and time
      (To be run with Maude 3.0 or above)
      Copyright (c) 2020, 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 : displayGrammars .
rewrites: 1337314 in 1720ms cpu (1719ms real) (777508 rewrites/second)
result GrammarList: (
grl #0:NTMsg inL => (#1:NTMsg ; #0:NTMsg) inL .  ; 
grl #0:NTMsg inL => (#0:NTMsg ; #1:NTMsg) inL .  ; 
grl #0:NTMsg notInI => (#0:NTMsg ; #1:NTMsg) inL . )
| (
grl #0:NTMsg inL => (#1:NTMsg ; #0:NTMsg) inL .  ; 
grl #0:NTMsg inL => (#0:NTMsg ; #1:NTMsg) inL .  ; 
grl #0:NTMsg notInI => (#1:NTMsg ; #0:NTMsg) inL . )
| 
grl empty => d(#1:Name, #2:Name) inL . 
| (
grl #0:NTMsg inL => (#1:NTMsg ; #0:NTMsg) inL .  ; 
grl #0:NTMsg inL => (#0:NTMsg ; #1:NTMsg) inL .  ; 
grl #0:NTMsg notInI,
   #0:NTMsg notLeq s(#1:Nonce ; t(#2:Nonce ; n(#3:Name, #4:Fresh) ; key(#3:Name, #5:Name))) ; w(n(#3:Name, #4:Fresh) ; #2:Nonce ; key(#3:Name, #5:Name)) => f(#0:NTMsg)
    inL . )
| (
grl #0:NTMsg inL => (#1:NTMsg ; #0:NTMsg) inL .  ; 
grl #0:NTMsg inL => (#0:NTMsg ; #1:NTMsg) inL .  ; 
grl #0:NTMsg notInI,
   #0:NTMsg notLeq w(n(#1:Name, #2:Fresh) ; #3:Nonce ; key(#1:Name, #4:Name)) ; key(#1:Name, #4:Name) => h(#0:NTMsg) inL . )
| (
grl #0:NTMsg inL => (#1:NTMsg ; #0:NTMsg) inL .  ; 
grl #0:NTMsg inL => (#0:NTMsg ; #1:NTMsg) inL .  ; 
grl key(#1:Name, #0:Name) notLeq key(i, #2:Honest) => key(#1:Name, #0:Name) inL . )
| (
grl #0:NTMsg inL => (#1:NTMsg ; #0:NTMsg) inL .  ; 
grl #0:NTMsg inL => (#0:NTMsg ; #1:NTMsg) inL .  ; 
grl #0:NTMsg notInI,
   #0:NTMsg notLeq n(#1:Name, #2:Fresh) ; t(n(#1:Name, #3:Fresh) ; #4:Nonce ; key(#1:Name, #5:Name)) => s(#0:NTMsg) inL . )
| (
grl #0:NTMsg inL => (#1:NTMsg ; #0:NTMsg) inL .  ; 
grl #0:NTMsg inL => (#0:NTMsg ; #1:NTMsg) inL .  ; 
grl #0:NTMsg notInI => t(#0:NTMsg) inL . )
| 
grl #0:NTMsg inL => (#1:NTMsg ; #0:NTMsg) inL .  ; 
grl #0:NTMsg inL => (#0:NTMsg ; #1:NTMsg) inL .  ; 
grl #0:NTMsg notInI => w(#0:NTMsg) inL . 
==========================================
reduce in MAUDE-NPA : summary(1, 0) .
rewrites: 9776 in 92ms cpu (88ms real) (106260 rewrites/second)
result Summary: States>> 1 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(1, 1) .
rewrites: 1405708 in 1232ms cpu (1235ms real) (1140996 rewrites/second)
result Summary: States>> 4 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(1, 2) .
rewrites: 5009452 in 4588ms cpu (4585ms real) (1091859 rewrites/second)
result Summary: States>> 7 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(1, 3) .
rewrites: 12224890 in 10628ms cpu (10628ms real) (1150253 rewrites/second)
result Summary: States>> 12 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(1, 4) .
rewrites: 35153550 in 28508ms cpu (28508ms real) (1233111 rewrites/second)
result Summary: States>> 22 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(1, 5) .
rewrites: 69303530 in 56408ms cpu (56407ms real) (1228611 rewrites/second)
result Summary: States>> 25 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(1, 6) .
rewrites: 40893769 in 37976ms cpu (37977ms real) (1076831 rewrites/second)
result Summary: States>> 10 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(1, 7) .
rewrites: 5135456 in 5680ms cpu (5678ms real) (904129 rewrites/second)
result Summary: States>> 0 Solutions>> 0
==========================================


)***

eq ATTACK-STATE(2) --- Hijacking fraud
= :: rA :: ---Alice --- Prover
  [ nil , +(n(a,rA)                                                                            
            @ a : t1 -> b : t2 # i : t2'),

          -(n(b,rB)                                                                            
            @ b : t3 -> a : t4 # i : t4'), ((t4 === t3 +=+ d(a,b)) and d(a,b) > 0/1), 

          -(s(n(b,rB') ; t(n(b,rB) ; n(a,rA) ; key(a,b)))  
            @ b : t5 -> a : t6 # i : t6'), ((t6 === t5 +=+ d(a,b)) and d(a,b) > 0/1),

          +(f(s(n(b,rB') ; t(n(b,rB) ; n(a,rA) ; key(a,b))) ; w(n(a,rA) ; n(b,rB) ; key(a,b))) 
            @ a : t6 -> b : t7 # i : t7') 
  | nil ] 
  &
  :: rB,rB' :: ---Bob  --- Verifier
  [ nil , -(n(a,rA)                                                                            
           @ a : t1 -> b : t2 # i : t2'), 
           ((t2 === t1 +=+ d(a,b)) and d(a,b) > 0/1),

          +(n(b,rB)                                                                            
            @ b : t2 -> a : t3 # i : t3'),

          +(s(n(b,rB') ; t(n(b,rB) ; n(a,rA) ; key(a,b)))  
            @ b : t2 -> a : t4 # i : t4'), 

          -(f(s(n(b,rB') ; t(n(b,rB) ; n(a,rA) ; key(a,b))) ; w(n(a,rA) ; n(b,rB) ; key(a,b))) 
           @ a : t6 -> b : t7 # i : t7'), ((t7 === t6  +=+ d(a,b)) and d(a,b) > 0/1), 
           ((t7 -=- t2) <= (2/1 *=* d) and d > 0/1), --- roundtrip check

          -(h(w(n(a,rA) ; n(b,rB) ; key(a,b)) ; key(a,b))
            @ i : t8 -> b : t9), ((t9 === t8 +=+ d(i,b)) and d(i,b) > 0/1)  
   | nil ]
  || empty
  || nil
  || nil
  || nil
  [nonexec] .

***(
reduce in MAUDE-NPA : summary(2, 0) .
rewrites: 383 in 4ms cpu (1ms real) (95750 rewrites/second)
result Summary: States>> 1 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(2, 1) .
rewrites: 899296 in 940ms cpu (940ms real) (956697 rewrites/second)
result Summary: States>> 2 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(2, 2) .
rewrites: 1528280 in 1728ms cpu (1728ms real) (884421 rewrites/second)
result Summary: States>> 2 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(2, 3) .
rewrites: 1166399 in 1508ms cpu (1508ms real) (773474 rewrites/second)
result Summary: States>> 1 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(2, 4) .
rewrites: 325862 in 396ms cpu (394ms real) (822883 rewrites/second)
result Summary: States>> 0 Solutions>> 0

)***
endfm

--- THIS HAS TO BE THE LAST LOADED MODULE !!!!
select MAUDE-NPA .

red displayGrammars .

red summary(1,0) .
red summary(1,1) .
red summary(1,2) .
red summary(1,3) .
red summary(1,4) .
red summary(1,5) .
red summary(1,6) .
red summary(1,7) .

red summary(2,0) .
red summary(2,1) .
red summary(2,2) .
red summary(2,3) .
red summary(2,4) .