Wide_Mouthed_Frog.maude 4.06 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
----Wide Mouthed Frog Protocol

---------------------------------------------------
--- 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] .

  --- 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 S T : UName .  
  var r r' r'' r''' r# r## rM : Fresh .
  vars NA NMA NB NMB NMS : 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(A,i)), nil ]  &
     :: nil :: [ nil | +(mkey(i,A)), nil ]  &
     :: nil :: [ nil | +(mkey(i,s)), nil ] 
  [nonexec] . 

  eq STRANDS-PROTOCOL
 
  --- Alice's Strand. 
   = :: r ::
     [ nil | +(A ; e(mkey(A,s) , B ; seskey(A,B,n(A,r)))) ,
             +(A ; e(seskey(A,B,n(A,r)), NMA)), nil ]
   &
     :: nil :: 
   --- Bob's Strand.
     [ nil | -(e(mkey(B,s), A ; SK)),
             -(A ; e(SK,NMA)), nil ] 
   & 
     :: nil ::
     --- Server's Strand 
    [ nil | -(A ; e(mkey(A,s) , B ; SK)),
            +(e(mkey(B,s) , A  ; SK)) , nil]
 
  [nonexec] .


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

eq ATTACK-STATE(1) =
--- An execution where the intruder finds out a message that share between the participants
:: r ::
     [ nil, +(a ; e(mkey(a,s) , b ; seskey(a,b,n(a,r)))) ,
            +(a ; e(seskey(a,b,n(a,r)), NMA)) | nil ]
   &
:: nil ::
    [ nil,  -(e(mkey(b,s), a ; seskey(a,b,n(a,r)))),
            -(a ; e(seskey(a,b,n(a,r)), NMA)) | nil ]  
     || NMA inI
     || nil
     || nil
     || nil
[nonexec] .


endfm

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