----  The Kao Chow Repeated Authentication Protocols

---------------------------------------------------
--- We modify only the relevant MAUDE-NPA modules 
---------------------------------------------------

fmod PROTOCOL-EXAMPLE-SYMBOLS is
  --- Importing sorts Msg, Fresh, Public
  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  UName SName Name Key Nonce  Masterkey Sessionkey .
  subsort Name Nonce  Key < Msg .
  subsort Masterkey  Sessionkey < Key .
  subsort SName UName < Name .
  subsort Name < Public . --- This is quite relevant and necessary

  --- Nonce operator
  op n : Name Fresh -> Nonce [frozen] .
  op t : Name Fresh -> Nonce [frozen] . ---Nonce del server

  --- User names
  ops a b i : -> UName .

  --- Server name
  op s : ->  SName . 

  --- MKey
  op mkey : Name Name -> Masterkey [frozen] .
 
  --- Seskey
  op seskey : Name Name Nonce -> Sessionkey [frozen] .

  ---encrypt
  op e : Key Msg -> Msg [frozen] .
  op d : Key Msg -> Msg  [frozen] .

--- successor

 op p : Msg -> Msg [frozen] .


--- Concatenation
  op _;_ : Msg Msg -> Msg [frozen gather (e E)] .

endfm

fmod PROTOCOL-EXAMPLE-ALGEBRAIC is
  protecting PROTOCOL-EXAMPLE-SYMBOLS .
  
  ----------------------------------------------------------
  --- Overwrite this module with the algebraic properties 
  --- of your protocol
  ----------------------------------------------------------
  
 eq d(K:Key, e(K:Key, Z:Msg)) = Z:Msg [variant] .
 eq e(K:Key, d(K:Key, Z:Msg)) = Z:Msg [variant] . 
   

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 A B : UName .  
  var D : Name .
  var r r' r'' r''' r# r## : Fresh . --- Comerntario chorra
  vars TS NA NB : Nonce .
  vars M1 M2 M N MA : Msg .
  var K Kt : Key . 
  var SK : Sessionkey .

  eq STRANDS-DOLEVYAO
   = :: nil :: [ nil | +(D), nil ]  & 
     :: nil :: [ nil | -(K), -(M), +(d(K,M)), nil ] &
     :: nil :: [ nil | -(K), -(M), +(e(K,M)), nil ] &
     :: nil :: [ nil | -(N), -(M), +(M ; N) , nil ] &
     :: nil :: [ nil | -(M ; N), +(M) , nil ] &
     :: nil :: [ nil | -(M ; N), +(N) , nil ] &
     :: nil :: [ nil | +(mkey(i,D)), nil ]  &
     :: nil :: [ nil | +(mkey(D,i)), nil ]  
  [nonexec] . 

  eq STRANDS-PROTOCOL =
  --- A->S : A,B,Na
  --- S->B : E(Kas:A, B, Na, Kab), E(Kbs:A, B, Na, Kab) 
  --- B->A : E(Kas:A, B, Na, Kab), E(Kab:Na), Nb
  --- A->B : E(Kab:Nb)
   --- Alice's Strand
    :: r ::
    [ nil | +(A ; B ; n(A,r)),
            -(e(mkey(A,s), A ; B ; n(A,r) ; SK) ; e(SK, n(A,r)) ; NB),
            +(e(SK, NB)) , nil ]
 &
    --- Bob's Strand
    :: r :: 
    [ nil | -(MA ; e(mkey(B,s), A ; B ; NA ; SK)) , 
            +(MA ; e(SK, NA) ; n(B,r)),
            -(e(SK, n(B,r))), nil ] 
 &
     :: r ::
     --- Server's Strand 
    [ nil | -(A ; B ; NA),
            +( e(mkey(A,s), A ; B ; NA ; seskey(A,B,n(s,r))) 
             ; e(mkey(B,s), A ; B ; NA ; seskey(A,B,n(s,r)))), nil ]

  [nonexec] .
  
eq ATTACK-STATE(0) =
    :: r ::
--- A normal execution of the protocol
    [ nil , -(MA ; e(mkey(b,s), a ; b ; NA ; SK)) , 
            +(MA ; e(SK, NA) ; n(b,r)),
            -(e(SK, n(b,r))) | nil ]  
    || empty
    || nil
    || nil
    || nil
[nonexec] .

eq ATTACK-STATE(1) =
:: r ::
--- An execution where the intruder finds out the Session key generated by the server 
[ nil,      -(MA ; e(mkey(b,s), a ; b ; NA ; SK)) , 
            +(MA ; e(SK, NA) ; n(b,r)),
            -(e(SK, n(b,r))) 
         | nil ]
|| SK inI
|| nil
|| nil
|| nil
[nonexec] .

eq ATTACK-STATE(2) =
:: r ::
---An execution where Bob completed the protocol believing that talks to Alice, but it is not so
    [ nil , -(MA ; e(mkey(b,s), a ; b ; NA ; SK)) , 
            +(MA ; e(SK, NA) ; n(b,r)),
            -(e(SK, n(b,r))) | nil ]  
     || empty
     || nil
     || nil
     || never
     *** Pattern for authentication
     (:: R:FreshSet ::
     [ nil | +(A ; B ; NA),
             -(MA ; e(SK, NA) ; n(b,r)),
             +(e(SK, n(b,r))),  nil ]
      & S:StrandSet || K:IntruderKnowledge)
  [nonexec] .

  
---eq USER-GRAMMARS
---= (grl empty => e(#1:Key, #2:Msg) inL . ! S2) 
---[nonexec] .
 

endfm

--- THIS HAS TO BE THE LAST LOADED MODULE !!!!
fmod MAUDE-NPA is
  protecting GENERIC-TOOLS .
endfm