Kao-Chow_Repeated_Authentication.maude 4.75 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176
----  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