Denning-Sacco.maude 3.8 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
----  Denning Sacco 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] .
  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] .

  --- 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 : Nonce .
  vars M1 M2 M N : Msg .
  var K : 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 
   --- S -> A : E(Kas: B, Kab, T, E(Kbs: A, Kab, T)) 
   --- A -> B : E(Kbs: A, Kab, T)

   --- Alice's Strand
    :: nil ::
    [ nil | +(A ; B),
            -(e(mkey(A,s), B ; SK ; TS ; M)),
            +(M), 
            nil ]
 &
    --- Bob's Strand
    :: nil :: 
    [ nil | -(e(mkey(B,s), A ; SK ; TS)), 
            nil ] 
 &
     :: r,r' ::
     --- Server's Strand 
    [ nil | -(A ; B),
            +(e(mkey(A,s), B 
                         ; seskey(A,B,n(s,r)) 
                         ; t(s,r') 
                         ; e(mkey(B,s), A ; seskey(A,B,n(s,r)) ; t(s,r')))),
            nil ]

  [nonexec] .
  
eq ATTACK-STATE(0) =
    :: r,r' ::
     --- Server's Strand 
    [ nil,  -(a ; b),
            +(e(mkey(a,s), b 
                         ; seskey(a,b,n(s,r)) 
                         ; t(s,r') 
                         ; e(mkey(b,s), a ; seskey(a,b,n(s,r)) ; t(s,r')))) | nil ]
    || seskey(a,b,n(s,r)) inI
    || nil
    || nil
    || nil
    [nonexec] .
endfm

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