***(
H&K process specification

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

(Prover) :
+(n(P?,f1)@t1) ·
−(NV @t2) ·
−(NV' @t3) ·
+(h(NV' ; n(P?,f1) ; NV ; key(V,P))@t4) ·
-(ok@t5) 


 )***
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 HonestA HonestB Honest Intruder NeTime ETime TMsg NTMsg TimeInfo Mac NameTime NameTimeSet .
  subsort Name Nonce Key Mac Real < NTMsg . 
  subsort TMsg NTMsg < Msg .
  subsort Name < Key .
  subsort Name < Public .
  subsort Honest Intruder < Name .
  subsort NameTime < NameTimeSet .

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


  --- Ok operator
  op ok : -> NTMsg .
  
  --- Principals
  op a : -> Honest . --- Alice
  op b : -> Honest . --- Bob
  op i : -> Intruder . --- 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] .
  subsort NameTime < NameTimeSet .
  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 : Fresh .
  var A B C : Name .
  var AB AB1 AB2 : Honest .
  var I : Intruder .
  vars N NA NA' NB : Nonce .
  vars C1 C2 C3 C4 C5 : Name .
  vars d t0 t1 t2 t3 t4 t5 t6 t7 t8 tA t9 t10 t11 t12 : Real .
  vars t0' t1' t2' t3' t4' t5' t6' t7' t8' t9' t10' t11' t12' : Real .
  vars t0'' t1'' t2'' t3'' t4'' t5'' t6'' t7'' t8'' t9'' t10'' : Real .
  vars t0n t1n t2n t3n t4n t5n : NeTime .
  vars AS1 AS2 AS3 AS4 AS5 : NameTimeSet .
  vars I1 I2 I3 I4 I5 : Real .

  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 | -(X @ C1 : t1 -> AS1 # i : t2), (t2 === t1 +=+ d(C1,i) and d(C1,i) >= 0/1),
                       +(h(X) @ i : t2 -> AS3), nil ] &
     :: nil :: [ nil | +(C @ i : t1 -> AS1), nil ] &
     :: nil :: [ nil | +(key(i,AB) @ i : t1 -> AS1), nil ]                                       
  [nonexec] .

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


eq ATTACK-STATE(1) = --- Mafia fraud 
:: rA , rA' :: ---Verifier --- Alice
     [ nil,  -(n(b,rB)                                       
              @ i : t1 -> a : t2), ((t2 === t1 +=+ d(i,a)) and d(i,a) > 0/1),

             +(n(a,rA)                                       
              @ a : t2 -> i : t3), 

             +(n(a,rA')                                      
              @ a : t2 -> i : t4),

             -(h(n(a,rA') ; n(b,rB) ; n(a,rA)  ; key(a,b))    
              @ i : t5 -> a : t6), (t6 >= t2), ((t6 === t5 +=+ d(i,a)) and d(i,a) > 0/1), 
              ((t6 -=- t2) <= (2/1 *=* d) and d > 0/1) | 
      nil ]
      &
:: rB :: ---Prover --- Bob
     [ nil , +(n(b,rB)                                       
              @ b : t0' -> i : t1'),

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

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

             +(h(n(a,rA') ; n(b,rB) ; n(a,rA)  ; key(a,b))    
              @ b : t5' -> i : t6')

    |  nil ]      
    || smt((d(a,i) +=+ d(b,i)) > d)
    || nil
    || nil
    || nil 
    [nonexec] .

 ***(    
  maude maude-npa.maude H\&K.maude 
         \||||||||||||||||||/
       --- Welcome to Maude ---
         /||||||||||||||||||\
       Maude 3.1 built: Oct 12 2020 20:12:31
       Copyright 1997-2020 SRI International
       Fri Oct 23 12:00:35 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: 649784 in 1196ms cpu (1196ms real) (543297 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, #0:Name) inL .  ; 
grl #0:NTMsg inL => (#1:NTMsg ; #0:NTMsg) inL .  ; 
grl #0:NTMsg inL => (#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,
   #0:NTMsg notLeq #1:Nonce ; n(#2:Name, #3:Fresh) ; #4:Nonce ; key(#2:Name, #5: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 . 
==========================================
reduce in MAUDE-NPA : summary(1, 0) .
rewrites: 6699 in 76ms cpu (76ms real) (88144 rewrites/second)
result Summary: States>> 1 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(1, 1) .
rewrites: 409727 in 572ms cpu (573ms real) (716305 rewrites/second)
result Summary: States>> 2 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(1, 2) .
rewrites: 1231928 in 1836ms cpu (1833ms real) (670984 rewrites/second)
result Summary: States>> 4 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(1, 3) .
rewrites: 3126486 in 4184ms cpu (4184ms real) (747248 rewrites/second)
result Summary: States>> 5 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(1, 4) .
rewrites: 3170290 in 4500ms cpu (4497ms real) (704508 rewrites/second)
result Summary: States>> 2 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(1, 5) .
rewrites: 998070 in 1344ms cpu (1345ms real) (742611 rewrites/second)
result Summary: States>> 0 Solutions>> 0
==========================================
)***

eq ATTACK-STATE(2)=  --- Hijacking fraud
:: rA , rA' :: ---Alice --- Verifier
 [ nil ,     -(n(b,rB)                                      
              @ b : t0 -> a : t1 # i : t2), ((t1 === t0 +=+ d(a,b)) and d(a,b) > 0/1),

             +(n(a,rA)                                      
              @ a : t1 -> b : t3 # i : t4),

             +(n(a,rA')                                     
              @ a : t5 -> b : t6 # i : t7),

             -(h(n(a,rA') ; n(b,rB) ; n(a,rA)  ; key(a,b))
              @ i : t8 -> a : t9) , ((t9 === t8 +=+ d(a,i)) and d(a,i) > 0/1), 
	      ((t9 -=- t5) <= (2/1 *=* d) and d > 0/1)  |
                                                                  
    nil]
    &
    :: rB :: --- Bob --- Prover
     [ nil ,  
             +(n(b,rB)                                       
              @ b : t0 -> a : t1 # i : t2),

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

             -(n(a,rA')                                      
              @ a : t5 -> b : t6 # i : t7), ((t6 === t5 +=+ d(a,b)) and d(a,b) > 0/1)                                                                                                  
      | nil ]
     || empty
     || nil
     || nil
     || nil
  [nonexec] .
  
***(
reduce in MAUDE-NPA : summary(2, 0) .
rewrites: 392 in 0ms cpu (2ms real) (~ rewrites/second)
result Summary: States>> 1 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(2, 1) .
rewrites: 488230 in 496ms cpu (494ms real) (984334 rewrites/second)
result Summary: States>> 1 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(2, 2) .
rewrites: 381965 in 288ms cpu (288ms real) (1326267 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(2,0) .
red summary(2,1) .
red summary(2,2) .