esorics12-variant.maude 3.02 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
fmod PROTOCOL-EXAMPLE-SYMBOLS is
  --- Importing sorts Msg, Fresh, Public, and GhostData
  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 Name Nonce NNSet Null .
  subsort Name Nonce NNSet < Msg .
  subsort Name < Public .
  subsort Null < Public .
  subsort  Nonce < NNSet .
  subsort  Null < NNSet .

  --- Encoding operators for public/private encryption
  op pk : Name Msg -> Msg [frozen] .
  op sk : Name Msg -> Msg [frozen] .  --- (?)

   --- Nonce operator
  op n : Name Fresh -> Nonce [frozen] .
  
  --- Principals
  op a : -> Name . --- Alice
  op b : -> Name . --- Bob
  op i : -> Name . --- Intruder
  
 --- Exclusive or
  op _*_ : NNSet NNSet -> NNSet [frozen assoc comm] .
  op null : -> Null .

endfm

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

  var A : Name .
  vars X Y Z : Msg .
  vars XN YN ZN : Msg .


  *** Exclusive or properties
  eq null * XN = XN [variant] .
  eq XN * XN = null [variant] .
  eq XN * XN * YN = YN [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
  ----------------------------------------------------------
  
  vars X Y Z : Msg .
  vars r r' : Fresh .
  vars A B : Name .
  vars N NA NB : Nonce .
  vars XN YN : NNSet .

  eq STRANDS-DOLEVYAO
   = :: nil :: [ nil | -(XN), -(YN), +(XN * YN), nil ] &
     :: nil :: [ nil | -(X), +(sk(i,X)), nil ] & 
     :: nil :: [ nil | -(pk(i,X)), +(X), nil ] & 
     :: nil :: [ nil | -(X), +(pk(A,X)), nil ] &
     :: nil :: [ nil | -(sk(A,X)), +(X), nil ] &
     :: nil :: [ nil | +(null), nil ] & 
     :: r   :: [ nil | +(n(i,r)), nil ] & 
     :: nil :: [ nil | +(A), nil ]
  [nonexec] .

  eq STRANDS-PROTOCOL
  = :: r ::  *** Bob ***
    [nil |  +(pk(A, n(B,r))), 
            -(pk(B, YN)), 
            +(YN * n(B,r)), nil] 
    &
    :: r' :: *** Alice ***
    [nil |  -(pk(A, XN)), 
            +(pk(B, n(A,r'))), 
            -(XN * n(A,r')), nil]
  [nonexec] .

  eq EXTRA-GRAMMARS
   = (grl XN notInI => pk(A,XN) inL . 
      ! S1 )
  [nonexec] .

  eq ATTACK-STATE(0)
  =  :: r' :: *** Alice ***
     [nil,  -(pk(a, XN)), 
             +(pk(b, n(a,r'))), 
             -(XN * n(a,r')) | nil]
     || empty
     || nil
     || nil
     || nil
  [nonexec] .
endfm

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