ISO_5_Pass_Authentication.maude 5.11 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 177 178 179 180 181 182 183 184
----ISO Five-Pass Authentication Protocol. Cryptyc's version

---------------------------------------------------
--- 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 Text .
  subsort Name Nonce  Key Text < Msg .
  subsort Masterkey  Sessionkey < Key .
  subsort SName UName < Name .
  subsort Name < Public . --- This is quite relevant and necessary
  
     --- text
  op txt : Name Name Nonce  -> Text [frozen] .
  --- Nonce operator
  op n : Name Fresh -> Nonce [frozen] .
  op mr : Name Fresh -> Nonce [frozen] . --- Nonce, run identifier

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

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

  --- MKey
  op mkey : Name Name -> Masterkey [frozen comm] .
 
  --- 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 S  : UName .  
  vars r r' r'' r''' r# r## r1 rM : Fresh .
  var TS NA NMA NB NMB NMS NB1 : Nonce .
  vars M1 M2 MA MB MS N M : Msg . 
  var K : Key .
  var SK : Sessionkey .  

  eq STRANDS-DOLEVYAO
  =  :: nil :: [ nil | +(A), nil ]  & 
     :: nil :: [ nil | +(s), nil ] &
     :: nil :: [ nil | -(K), -(M), +(d(K,M)), nil ] &
     :: nil :: [ nil | -(M), -(K), +(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,A)), nil ]  &
     :: nil :: [ nil | +(mkey(i,s)), nil ] 
  [nonexec] . 

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

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

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


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

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