secret06.maude 3.42 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
***(
The informal journal-level description of this protocol is as follows,
where S is the server:

S --> A: N_S
A --> B: sk(A,N_S ; S)
A --> B: sk(A,B ; N_A ; S)

where N_A, N_S, and N_B are nonces, and sk(x,y) means message y encripted 
using private key x. Moreover, concatenation and encription/decription
have the following property:

  X ; (Y ; Z) = (X ; Y) ; Z
  pk(K,sk(K,M)) = M
  sk(K,pk(K,M)) = M

However, note that the associativity property is bounded to depth 3 below by
using appopriate sorts.
)***

fmod PROTOCOL-EXAMPLE-SYMBOLS is
  protecting DEFINITION-PROTOCOL-RULES . --- Importing sort Msg, Fresh, Public
  
  ----------------------------------------------------------
  --- 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 Name Nonce Key .
  sorts List Elm .
  subsort Name < Key .
  subsort Name Nonce Key < Elm .
  subsort Elm < Msg .
  subsort List < Msg .
  subsort Name < Public .

  --- Encoding operators for public/private encryption
  op pk : Key Msg -> Msg [frozen] .
  op sk : Key Msg -> Msg [frozen] .

  --- Keys known by intruder
  op s : -> Name . --- Name for the Server
  op a : -> Name . --- Name for the Initiator
  op b : -> Name . --- Name for the Responder
  op i : -> Name . --- Name for the Intruder

  --- Nonce operator
  op n : Name Fresh -> Nonce [frozen] .
  
  --- Associativity operator
  op _;_ : Msg  Msg  -> List [frozen] .
  
endfm

fmod PROTOCOL-EXAMPLE-ALGEBRAIC is
  protecting PROTOCOL-EXAMPLE-SYMBOLS .
  
  ----------------------------------------------------------
  --- Overwrite this module with the algebraic properties 
  --- of your protocol
  ----------------------------------------------------------

  var Z : Msg .
  var Ke : Key .
  vars Xe Ye Ze : Elm .
  
  *** Encryption/Decryption Cancellation
  eq pk(Ke,sk(Ke,Z)) = Z [variant] .
  eq sk(Ke,pk(Ke,Z)) = Z [variant] .
  
  *** Bounded Associativity (for 3-depth)
  eq Xe ; (Ye ; Ze) = (Xe ; Ye) ; Ze [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 Ke : Key .
  vars X Y Z : Msg .
  var r : Fresh .
  var N : Nonce .

  eq STRANDS-DOLEVYAO
   = :: nil :: [ nil | -(X), -(Y), +(X ; Y), nil ]
     &
     :: nil :: [ nil | -(X ; Y), +(X), nil ]
     &
     :: nil :: [ nil | -(X ; Y), +(Y), nil ]
     &
     --- Private encryption only his key
     :: nil :: [ nil | -(X), +(sk(i,X)), nil ] 
     &
      --- Public encryption any key
     :: nil :: [ nil | -(X), +(pk(Ke,X)), nil ]
  [nonexec] .

  eq STRANDS-PROTOCOL
   = --- server 
     :: r :: [nil | +(n(s,r)), nil ] &
     --- initiator
     :: r :: [nil | -(N), +(sk(a,N ; s)), +(sk(a,b ; (n(a,r) ; s))), nil] &
     --- responder
     :: nil :: [nil | -(sk(a,X ; s)), -(sk(a,(b ; Z) ; s)), nil]
  [nonexec] .

  eq ATTACK-STATE(0)
   = :: nil :: [nil, -(sk(a,X ; s)), -(sk(a,(b ; N) ; s)) | nil]
     || empty
     || nil
     || nil
     || nil
  [nonexec] .

endfm

--- THIS HAS TO BE THE LAST LOADED MODULE !!!!
select MAUDE-NPA .