NPA-Syntax.maude 9.76 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 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272
---(
    Changes made by Andrew Cholewa Wed Oct 30:
    Removed the {_} : Module -> ParsedData operator and made Module a subsort of 
    ParsedData to match FModule, and so that it doesn't clash with the wrapper
    being used in parsePSL to put modules in Data.
    Commented out the error Sort and constant around line 520 in the module
    GEN-MOD in order to avoid clashes with the error in parsePSL. Plus, error
    checking at this point should not be necessary.

    Changed the System sort to System to avoid clashes with the System imported from
    prelude and used in the psl-loop module for the user input.  

    Added a rule for processing the attack states to handle the case where there is
    an empty never pattern.
---)

---(About changing System to System: In order to avoid confusion and conflicting with Maude-NPA, we assume that we don't need to load our modules together with Maude-NPA. --Fan
---)

fmod DEFINITION-PROTOCOL-RULES is
  protecting META-LEVEL .
  sort Universal . --- Special sort used for unsorted actions (don't remove)
  sort Msg . --- Generic sort for messages
  sort Fresh . --- Sort for private information.
  sort Public . --- Handy sort to say what is public
  subsort Public < Msg .
  op emptyPublic : -> Public .
  op nullFresh : -> Fresh .

  op pair : Msg Msg -> Msg [frozen] . --- Special treatment for indistinguishability

  sort MsgSet .
  subsort Msg < MsgSet .
  op emptyMsgSet : -> MsgSet [ctor] .
  op _,_ : MsgSet MsgSet -> MsgSet [ctor assoc comm id: emptyMsgSet] .

  op noMsg : -> Msg . --- Auxiliar useless message used as a marker

  sort SMsg .

  sort SignedSMsg . 
  subsort SignedSMsg < SMsg .
  op +`(_`) : Msg -> SignedSMsg [format (nir d d d o)] .
  op -`(_`) : Msg -> SignedSMsg [format (nib d d d o)] .

  sort Resuscitated .
  subsort Resuscitated < SMsg .
  op resuscitated`(_`) : Msg -> Resuscitated [ctor format (nic d d d o)] .

  sort LazyLearnt .
  subsort LazyLearnt < SMsg .
  op generatedByIntruder`(_`) : Msg -> LazyLearnt [ctor format (nic d d d o)] .

  sort EmptyList .
  op nil : -> EmptyList [ctor format (ni d)] .
  op _,_ : EmptyList EmptyList -> EmptyList
    [ctor assoc id: nil format (d d s d)] .

  sort SMsgList .
  subsort SMsg Synchro Resuscitated < SMsgList .
  subsort EmptyList < SMsgList .
  subsort ResuscitatedList < SMsgList .
  op _,_ : SMsgList SMsgList -> SMsgList
    [ctor assoc id: nil format (d d s d)] .

  sort ResuscitatedList .
  subsort Resuscitated < ResuscitatedList .
  subsort EmptyList < ResuscitatedList .
  op _,_ : ResuscitatedList ResuscitatedList -> ResuscitatedList
    [ctor assoc id: nil format (d d s d)] .

  --- We duplicate the SMsgList sort because A-unification may generate
  --- an infinite number of most-general unifiers.
  sort SMsgList-L SMsgList-R .

  op nil : -> SMsgList-R [ctor] .
  op _,_ : SMsg SMsgList-R -> SMsgList-R
    [ctor format (d d s d) gather (e E)] .
  op _,_ : Synchro SMsgList-R -> SMsgList-R
    [ctor format (d d s d) gather (e E)] .

  op nil : -> SMsgList-L [ctor] .
  op _,_ : SMsgList-L SMsg -> SMsgList-L
    [ctor format (d d s d) gather (E e)] .
  op _,_ : SMsgList-L Synchro -> SMsgList-L
    [ctor format (d d s d) gather (E e)] .

  --- Composition
  sort Synchro .
  op {_->_;;_;;_} : Role Role How Msg -> Synchro [format (nig d d d d d d d d o)] .

  sort Role .
  op initiator : -> Role .
  op responder : -> Role .

  sort How .
  op 1-1 : -> How .
  op 1-* : -> How .
    
  --- Strands
  sort FreshSet .
  subsort Fresh < FreshSet .
  op nil : -> FreshSet [ctor] .
  op _,_ : FreshSet FreshSet -> FreshSet 
    [ctor comm assoc id: nil] .
    
  sort Strand .
  op ::_::[_|_] : FreshSet SMsgList-L SMsgList-R -> Strand 
                  [format (ni d d ni s+++ s--- s+++ d s---)] .

  sort StrandSet .
  subsort Strand < StrandSet .
  op empty : -> StrandSet [ctor] .
  op _&_ : StrandSet StrandSet -> StrandSet
    [ctor assoc comm id: empty format (d d d d)] .

  sort Knowledge-!inI Knowledge-inI Knowledge-!= Knowledge 
       Knowledge-irr Knowledge-inst Knowledge-CPSA .
  subsort Knowledge-!inI Knowledge-inI Knowledge-!=
          Knowledge-irr Knowledge-inst Knowledge-CPSA < Knowledge .
  op _!inI : Msg -> Knowledge-!inI [format (ni d o)] .
  op _inI : Msg -> Knowledge-inI [format (niu d o)] .
  ---prec 26 added by Andrew Cholewa to ensure Maude parses != correctly in
  ---Maude-PSL 10/27/14
  op _!=_ : Msg Msg -> Knowledge-!= [comm format (nig d d o) prec 26] .
  op irr`(_`) : Msg -> Knowledge-irr [format (nim d d d o)] .
  op inst`(_`) : Msg -> Knowledge-inst [format (nim d d d o)] .
  op _before_ : MsgInStrand MsgInStrand -> Knowledge-CPSA [format (nim d d o)] .
  op secret`(_`) : Msg -> Knowledge-CPSA [format (nim d d d o)] .

  sort MsgInStrand PosNat .
  op `(_InStrand_`) : PosNat Fresh -> MsgInStrand .

  ops 1st 2nd 3rd 4th 5th 6th 7th 8th 9th 10th 11th 12th 13th 14th 15th 16th 17th 18th 19th 20th : -> PosNat .
  op z : -> PosNat .
  op s : PosNat -> PosNat [iter] .
  
  sort Ghost .
  op ghost`(_`,_`,_`,_`,_`) : Msg StrandSet IntruderKnowledge SMsgList Properties 
                        -> Ghost 
     [frozen format (ni d s+++ d d d si d si d si s--- d)] .

  sort GhostList .
  subsort Ghost < GhostList .
  op nil : -> GhostList [ctor format (ni d)] .
  op _,_ : GhostList GhostList -> GhostList 
           [ctor assoc id: nil format (d d n d)] .
  
  sort IntruderKnowledge-!inI IntruderKnowledge-inI 
       IntruderKnowledge-!= IntruderKnowledgeElem IntruderKnowledge 
       IntruderKnowledge-irr IntruderKnowledge-inst IntruderKnowledge-CPSA 
       IntruderKnowledge-empty .
  subsort IntruderKnowledge-empty < IntruderKnowledge-!inI .
  subsort IntruderKnowledge-empty < IntruderKnowledge-inI .
  subsort IntruderKnowledge-empty < IntruderKnowledge-!= .
  subsort IntruderKnowledge-empty < IntruderKnowledge-irr .
  subsort IntruderKnowledge-empty < IntruderKnowledge-inst .
  subsort IntruderKnowledge-empty < IntruderKnowledge-CPSA .
  subsort IntruderKnowledge-empty < IntruderKnowledge .
  subsort IntruderKnowledge-!inI IntruderKnowledge-inI 
          IntruderKnowledge-!= 
          IntruderKnowledge-irr 
          IntruderKnowledge-inst 
          IntruderKnowledge-CPSA
          < IntruderKnowledge .
  subsort Knowledge-!inI < IntruderKnowledge-!inI .
  subsort Knowledge-inI < IntruderKnowledge-inI .
  subsort Knowledge-!= < IntruderKnowledge-!= .
  subsort Knowledge-irr < IntruderKnowledge-irr .
  subsort Knowledge-inst < IntruderKnowledge-inst .
  subsort Knowledge-CPSA < IntruderKnowledge-CPSA .
  subsort Knowledge < IntruderKnowledgeElem < IntruderKnowledge .
  op empty : -> IntruderKnowledge-empty [ctor] .
  op _,_ : IntruderKnowledge IntruderKnowledge -> IntruderKnowledge
    [ctor assoc comm id: empty format (d d d d) prec 28] .
  op _,_ : IntruderKnowledge-!inI IntruderKnowledge-!inI 
           -> IntruderKnowledge-!inI [ditto] .
  op _,_ : IntruderKnowledge-inI IntruderKnowledge-inI 
           -> IntruderKnowledge-inI [ditto] .
  op _,_ : IntruderKnowledge-!= IntruderKnowledge-!=
           -> IntruderKnowledge-!= [ditto] .
  op _,_ : IntruderKnowledge-irr IntruderKnowledge-irr
           -> IntruderKnowledge-irr [ditto] .
  op _,_ : IntruderKnowledge-inst IntruderKnowledge-inst
           -> IntruderKnowledge-inst [ditto] .
  op _,_ : IntruderKnowledge-CPSA IntruderKnowledge-CPSA
           -> IntruderKnowledge-CPSA [ditto] .
  op _,_ : IntruderKnowledge-empty IntruderKnowledge-empty
           -> IntruderKnowledge-empty [ditto] .

  sort Properties .
  op nil : -> Properties [ctor format (ni d)] .

  sort System .

  ************************
  --- Stuff for never patterns
  sort ExclusionPattern .
  subsort ExclusionPattern < Properties .

  --- neverPattern as StrandSet + IntruderKnowledge
  sort NeverPattern .
  sort NeverPatternSet .
  subsort  NeverPattern < NeverPatternSet .

  op _||_ : StrandSet IntruderKnowledge -> NeverPattern .
  op nil : -> NeverPatternSet .
  op __ : NeverPatternSet NeverPatternSet -> NeverPatternSet  
  [ctor assoc comm id: nil format (d n d)]  .

  op never : NeverPatternSet -> ExclusionPattern .
  ************************

  op _||_||_||_||_
    : StrandSet IntruderKnowledge SMsgList GhostList Properties -> System
      [format (d n d n d n d n d d)] .

  --- Auxiliary sorts for comparing strands in _implies_ function
  sort SMsgSet .
  subsort SMsg < SMsgSet .
  op emptySMsgSet : -> SMsgSet [ctor] .
  op _;_ : SMsgSet SMsgSet -> SMsgSet
    [ctor assoc comm id: emptySMsgSet] .

  sort SMsgList$ .
  subsort SMsgList < SMsgList$ .
  subsort SMsgSet < SMsgList$ .
  subsort Synchro < SMsgList$ .
  op _,_ : SMsgList$ SMsgList$ -> SMsgList$ [ditto] . --- assoc
  
  sort SMsgList-L$ SMsgList-R$ .
  subsort SMsgList-L < SMsgList-L$ .
  subsort SMsgList-R < SMsgList-R$ .
  op _,_ : SMsgSet SMsgList-R$ -> SMsgList-R$ [ditto] .
  op _,_ : Synchro SMsgList-R$ -> SMsgList-R$ [ditto] .
  op _,_ : SMsgList-L$ SMsgSet -> SMsgList-L$ [ditto] .
  op _,_ : SMsgList-L$ Synchro -> SMsgList-L$ [ditto] .
    
  sort Strand$ .
  subsort Strand < Strand$ .
  op ::_::[_|_] : FreshSet SMsgList-L$ SMsgList-R$ -> Strand$ [ditto] .

  sort StrandSet$ .
  subsort Strand$ < StrandSet$ .
  subsort StrandSet < StrandSet$ .
  op _&_ : StrandSet$ StrandSet$ -> StrandSet$ [ditto] .

  *** System$ ********************************************
  sort System$ .
  subsort System < System$ .
  op _||_||_||_||_
    : StrandSet$ IntruderKnowledge SMsgList GhostList Properties 
   -> System$ [ditto] .
      
  subsort SMsgSet < SMsgList .
  op _,_ : SMsgSet SMsgList-R -> SMsgList-R [ditto] .
  op _,_ : SMsgList-L SMsgSet -> SMsgList-L [ditto] .

  sort Attack .
  subsort SystemSet < Attack .

  sort SystemSet .
  subsort System < SystemSet .
  op empty : -> SystemSet .
  op __ : SystemSet SystemSet -> SystemSet
    [ctor assoc comm id: empty format (d n d)] .
  
  op STRANDS-DOLEVYAO : -> StrandSet .
  op STRANDS-PROTOCOL : -> StrandSet .
  op ATTACK-STATE : Nat -> Attack .
endfm