PSL-Syntax.maude 20.7 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
Maude-PSL, Version: [1.0] [May 15th 2015]
Copyright (c) 2015, University of Illinois
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, 
are permitted provided that the following conditions are met:
* Redistributions of source code must retain the above copyright notice, 
this list of conditions and the following disclaimer.
* Redistributions in binary form must reproduce the above copyright notice, 
this list of conditions and the following disclaimer in the documentation 
and/or other materials provided with the distribution.
* Neither the name of the University of Illinois nor the names of its contributors 
may be used to endorse or promote products derived from this software without 
specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" 
AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, 
THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE 
ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE 
FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL 
DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER 
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, 
OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-----------------------------------------------------------------------------------------------------------
Copyright (c) 2015. To the extent that a federal employee is an author of 
a portion of the software or a derivative work thereof, no copyright is 
claimed by the United States Government, as represented by the Secretary 
of the Navy ("GOVERNMENT") under Title 17, U.S. Code. All Other Rights Reserved.
Permission to use, copy, and modify this software and its documentation is 
hereby granted, provided that both the copyright notice and this permission 
notice appear in all copies of the software, derivative works or modified 
versions, and any portions thereof, and that both notices appear in 
supporting documentation.
GOVERNMENT ALLOWS FREE USE OF THIS SOFTWARE IN ITS "AS IS" CONDITION AND 
DISCLAIM ANY LIABILITY OF ANY KIND FOR ANY DAMAGES WHATSOEVER RESULTING 
FROM THE USE OF THIS SOFTWARE.
GOVERNMENT requests users of this software to return modifications, 
improvements or extensions that they make to: 
maudenpa@chacs.nrl.navy.mil]
-or-
Naval Research Laboratory, Code 5543
4555 Overlook Avenue, SW
Washington, DC 20375
---)
---(
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
The following modules contain the operators and axioms for the data structures
used in the translation from Maude-PSL to Maud-NPA specifications. Anything
prefixed by a '$' is considered "internal," and shouldn't be used outside
of the associated SEMANTICS module in psl.maude.

The translation rules can be found in psl.maude.

Note: Because of the ambiguity in Maude's multi-line syntax, I use [] instead of parenthesis inside of multi-line comments.
---)
load NPA-Syntax.maude .
---load nspk.maude
---(
    Contains the high level data structures used to store the PSL-specification
    and the derived strands. This is the core of Omega from
    Andrew Cholewa's masters thesis.
---)    
fmod TRANSLATION-SYNTAX is
    protecting DEFINITION-PROTOCOL-RULES .
    protecting PROTOCOL-EXAMPLE-SYMBOLS .
    protecting NAT .


    ---Terms of sort TranslationData are ACU soups. The soup contains the
    ---Maude-PSL specification, and all of the data structures used in the
    ---translation. Bracket operators ([_]) are used to inject various sorts
    ---into TranslationData.
    sort TranslationData .
    op mt : -> TranslationData .
    op __ : TranslationData TranslationData -> 
        TranslationData [assoc comm id: mt format(n n o)] .

    sort MyNatList .
    subsort Nat < MyNatList .
    op mt : -> MyNatList .
    op _:_ : Nat Nat -> MyNatList [assoc id: mt] .

    ---StrandData and its singular form StrandDatum are mappings from
    ---a role a to the role's associated input, strand, and output. Terms
    ---of this form are built from the Protocol section, and are used to
    ---populate the attack states.
    sort StrandDatum StrandData .
    subsort StrandDatum < StrandData .
    op mt : -> StrandData [ctor] .
    op _&_ : StrandData StrandData -> StrandData [assoc comm id: mt format(d d n d)] .
    op [_] : StrandData -> TranslationData .
    ---(
    A mapping from roles to strands.
    Arguments:
    1. The role to whom this strand and belongs
    2. The role's input.
    3. The role's strand.
    4. The role's output
    ---)
    op _|->{_}_{_} : Role MsgSet Strand MsgSet -> StrandDatum [ctor prec 30] .
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 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383
endfm


---(
    Contains the syntax for the sections Protocol, Intruder and Attacks. 
    Note that we group them within a larger Specification section in the 
    Maude code. This is an artifact of an earlier iteration of the 
    Maude-PSL syntax.
---)
fmod SECTION-SYNTAX is
    protecting TRANSLATION-SYNTAX .

    *************************Section*********************************
    sort Section SubSection SectionName Stmt Stmts .
    subsort Section < TranslationData .
    subsort Stmt < Stmts .
    op pass : -> Stmts [ctor] .
    ---These are any statements that may appear in a Maude-PSL specification.
    ---Each section will have its own subsort of Stmts for the statements
    ---that appear in that section.
    op __ : Stmts Stmts -> Stmts [assoc id: pass format(n n o) prec 55] .
    ops Protocol Intruder Attacks : -> SectionName .
    sorts ProtocolSection IntruderSection AttackSection .
    subsorts ProtocolSection IntruderSection AttackSection < SubSection .
    op mt : -> SubSection .

    op Protocol{} : -> SubSection .
    op Intruder{} : -> SubSection .
    op Attacks{} : -> SubSection .
    eq Protocol{} = Protocol{ pass } .
    eq Intruder{} = Intruder{ pass } .
    eq Attacks{} = Attacks{ pass } .
    ---(
    Subsections are treated as free floating entities within the larger
    Specification Section.
    ---)
    op __ : SubSection SubSection -> SubSection 
        [ctor assoc comm id: mt format(d n o)] .

    op Specification{_} : SubSection -> Section [ctor format(d d n o d)] .
    op _{_} : SectionName Stmts -> SubSection [prec 30 format(d o ntt nt o)] .

endfm

fmod DEFINITION-SYNTAX is
    protecting TRANSLATION-SYNTAX .
    sort Definition NeDefinitions Definitions .
    subsort Definition < NeDefinitions < Definitions .
    op _:=_ : Msg Msg -> Definition [prec 30] .
    op _,_ : Definitions Definitions -> Definitions [ctor comm assoc id: $noDefs] .
    op _,_ : NeDefinitions NeDefinitions -> NeDefinitions [ctor ditto] .
    op $noDefs : -> Definitions .
    ---(
    The following two functions make the definitions map idempotent. Basically, if we have:
    da |-> t
    dp |-> f[da]
    Then these functions will turn the above into
    da |-> t
    dp |-> f[t]

    If after Nat iterations we fail to compute an idempotent substitution, then we throw an error.
    ---)
    op $makeIdem : Definitions -> Definitions .
    ---(
    Args:
    1. Definition after n-1 applications of the other Defs.
    2. Definition after n applications of the other Defs. [If these two are equal, that Def has been fully simplified]
    3. The Definitions that have not yet been fully simplified.
    4. The original definition
    5. Our current Iteration.
    ---)
    op $makeIdem : Definition Definition Definitions Definition Nat -> Definitions .
    op [_] : Definitions -> TranslationData .
    op numIterations : -> Nat .

    op $cantMakeDefsIdempotent : Definitions Nat -> [Definitions] .

    ---(
    This structure is used to pair definitions with line numbers for any preliminary error checking that needs to be done on
    user-defined terms that don't come up while parsing the terms, or in the Python error checking. For example:
    key := (A, B, n(B, r1)) does not throw an error anywhere, however it lifts TranslationData into the kind. We need to be able
    recognize these kinds of problems and report them.
    ---)
    sort ShorthandLineNum . 
    subsort ShorthandLineNum < Msg .
    op ((_,_)) : Msg Nat -> ShorthandLineNum .
    ---(
    If a malformed definition term provided by the user lifts the definitions (and the entire specification) to the kind, then
    this function will generate an error term for Python to process.
    If the definitions are well formed, we just strip away the line number and start translating. Otherwise, we eliminate those
    definitions that are well-formed, and report the rest.
    ---)
    op $$$malformedDefs : [Definitions] -> [Definitions] .
    op $checkWellFormed : [Definitions]  -> [Definitions] .
    op $checkWellFormed : Definitions -> Definitions .

    ---(
    Given a multiset of (malformed) definitions of the form
    (shorthand, lineNum) := result
    converts the list into a list of terms of the form
    (shorthand := result$$,$$ lineNum)
    in order to simplify error processing by python.
    ---)
    op ((_$$,$$_)) : [Definition] Nat -> [Definition] . 
    op _$$;;;$$_ : [Definition] [Definition] -> [Definitions] [assoc id: $noDefs] .
    op $moveLineNum : [Definitions] -> [Definitions] .
endfm

fmod PROTOCOL-SYNTAX is
    protecting TRANSLATION-SYNTAX .
    protecting SECTION-SYNTAX .
    protecting DEFINITION-SYNTAX .

    sort ProtStmt ProtStmts .
    subsort ProtStmt < Stmt .
    subsort ProtStmt < ProtStmts < Stmts .
    op $emptyProtocol : -> ProtocolSection .
    ---Associative with identity pass.
    op __ : ProtStmts ProtStmts -> ProtStmts [ctor ditto] .

    ---The natural number at the end of each statement is the line number
    ---on which the statement begins in the original PSL specification. 
    ---This number is used when reporting translation errors to the user.
    op In`(_`) = _.[_] : Role MsgSet Nat -> ProtStmt .
    op Out`(_`) = _.[_] : Role MsgSet Nat -> ProtStmt .
    op _._->_:_|-_.[_] : Nat Role Role Msg Msg Nat -> ProtStmt [prec 30] .

endfm

fmod INTRUDER-SYNTAX is
    protecting TRANSLATION-SYNTAX .
    protecting SECTION-SYNTAX .
    protecting DEFINITION-SYNTAX .

    sort IntStmt IntStmts .
    subsort IntStmt < Stmt .
    subsort IntStmt < IntStmts < Stmts .

    ---StrandSet is declared in the Maude-NPA syntax (NPA-Syntax.maude), and
    ---is used as the target of the Intruder translation.
    op [_] : StrandSet -> TranslationData [ctor] .
    op $emptyIntruder : -> IntruderSection .
    op __ : IntStmts IntStmts -> IntStmts [ctor ditto] .
    op _=>_.[_] : MsgSet MsgSet Nat -> IntStmt [prec 50] . 
    op _=>_.[_] : MsgSet Msg Nat -> IntStmt [prec 50] .
    op =>_.[_] : MsgSet Nat -> IntStmt [prec 50] .
    op _<=>_.[_] : MsgSet MsgSet Nat -> IntStmts [prec 50] .

endfm

---(
Mappings are used both in the Attack Section, and when composing
protocols, hence its separation into its own module.
---)
fmod MAPPINGS is 
    protecting TRANSLATION-SYNTAX .
    sorts Mapping Mappings .
    subsort Mapping < Mappings .
    op id : -> Mappings [ctor] .
    op _|->_ : Msg Msg -> Mapping [ctor prec 20] .
    op _,_ : Mappings Mappings -> Mappings [ctor assoc comm id: id prec 25] .
endfm

fmod ATTACK-SYNTAX is
    protecting TRANSLATION-SYNTAX .
    protecting SECTION-SYNTAX .
    protecting PROTOCOL-SYNTAX .
    protecting DEFINITION-PROTOCOL-RULES . 
    protecting MAPPINGS .

    ---The following code allows us to simulate Maude style variable 
    ---declarations. We need to be able to add a variable of sort StrandSet,
    ---and one of sort IntruderKnowledge to the attack states. However,
    ---we can't just declare a constant S:StrandSet, because that's ambiguous. 
    ---Neither can we just insert a variable, because then Maude complains
    ---that the variable is unbound.
    ---So instead we need to have two constants S, and K and a simulation
    ---of variable declarations which can be added to the Maude module 
    ---at the end.
    sort NPA-Sort VarDecl .
    ops StrandSet IntruderKnowledge SMsgList-R : -> NPA-Sort .
    op S : -> StrandSet .
    op K : -> IntruderKnowledge .
    op LIST : -> SMsgList-R .
    op var_:_. : StrandSet NPA-Sort -> VarDecl .
    op var_:_. : IntruderKnowledge NPA-Sort -> VarDecl .
    op var_:_. : SMsgList-R NPA-Sort -> VarDecl .
    op [_] : VarDecl -> TranslationData .

    op $emptyAttacks : -> AttackSection .
    op $emptyAttackData : -> AttackData .

    sort AttDef AttDefs .
    subsort AttDef < AttDefs < Stmts .
    subsort AttDef < Stmt .
    op __ : AttDefs AttDefs -> AttDefs [ctor ditto] .
    ---An AttDef is an attack pattern.
    op _.{_} : Nat AttackPSL -> AttDef .

    sorts AttStmt AttStmts .
    subsort AttStmt < AttStmts .
    op __ : AttStmts AttStmts -> AttStmts [ctor assoc] .
    op emptyAttStmt : -> AttStmts [ctor] .

    sort Subst .
    op Subst`(_`) = _.[_] : Role Mappings Nat -> Subst [ctor prec 26] .

    sort ExecStatement .
    op _executes protocol .[_] : Role Nat -> ExecStatement [ctor prec 28] .
    op _executes up to_.[_] : Role Nat Nat -> ExecStatement [ctor prec 28] .


    sort Disequality Disequalities Constraints .
    subsort Disequality < Disequalities .
    ---Observe that this isn't exactly the same as !=. This is to avoid clashes
    ---with the operator defined in NPA-Syntax, whose connected component isn't 
    ---compatible with Disequalities'. However, the Python code will convert
    ---the != seen in PSL specifications into $!= before it ever reaches
    ---the Maude code.
    op _$!=_ : Msg Msg -> Disequality [ctor prec 26] .
    op $noIneq : -> Disequalities .
    op _,_ : Disequalities Disequalities -> Disequalities [ctor assoc comm id: $noIneq] .
    op $noConstraints : -> Constraints [ctor] .
    op With constraints_.[_] : Disequalities Nat -> Constraints [prec 31] .

    sort IntruderKnowledgeStmt .
    op Intruder learns_.[_] : MsgSet Nat -> IntruderKnowledgeStmt .

    sorts CoreAttack .
    subsort ExecStatement Subst Constraints IntruderKnowledgeStmt < CoreAttack .
    op $noCore : -> CoreAttack .
    op __ : CoreAttack CoreAttack -> CoreAttack [ctor assoc comm id: $noCore prec 33] .

    sorts WithoutBlock WithoutBlocks .
    subsort WithoutBlock < WithoutBlocks .
    op __ : WithoutBlocks WithoutBlocks -> WithoutBlocks [ctor] .
    op without:_ : CoreAttack -> WithoutBlock [ctor prec 35] .


    sort AttackPSL .
    subsort CoreAttack < AttackPSL .
    op __ : CoreAttack WithoutBlocks -> AttackPSL [ctor] .
       

    sort AttackData .
    op __ : AttackData AttackData -> AttackData 
        [ctor comm assoc id: $emptyAttackData] .
    op [_|->_] : Nat System -> AttackData .
    op [_] : AttackData -> TranslationData .
    op {_} : StrandSet -> TranslationData .
    op {_} : IntruderKnowledge -> TranslationData .

    ---Error checking operators.
    ---Takes as argument the set of all pairs that form an invalid order-sorted
    ---substitution.
    op $$$invalidSorting : MsgPairs -> [Mapping] .

    ---(
    The following sorts and operators are used as part of checking that
    a user-provided attack substitution is a valid order-sorted substitution
    that can be idempotenized.
    ---)
    sort MsgPair MsgPairs MsgNum MsgNumSet .
    subsort MsgPair < MsgPairs .
    subsort MsgNum < MsgNumSet .
    ---Ties a Msg m with a natural number n. m is meant to represent one 
    ---of the messages in the range of an attack substitution. n is the 
    ---line number in the PSL specification on which the attack was originally
    ---defined. The line number will be important when reporting error messages.
    op ${_;_}$ : Msg Nat -> MsgNum [prec 28] .
    op __ : MsgNumSet MsgNumSet -> MsgNumSet [ctor assoc comm prec 29] .
    eq ${M:Msg ; N:Nat}$ ${M:Msg ; N:Nat}$ = ${M:Msg ; N:Nat}$ .
    ---This a msg m with a set of msg pairs p_1, p_2, ... p_n. m is meant
    ---to be a message in the domain of an attack substitution, while 
    ---p_1, p_2, ..., p_n contain all of the messages that m maps to. 
    ---In a well-defined substitution, n=1. However, in an invalid substitution
    ---there may be more than one. We need to be able to extract the invalid
    ---mappings as well as the lines on which they appear.
    op _|->_ : Msg MsgNumSet -> MsgPair [prec 30] .
    op $none : -> MsgPairs .
    op __ : MsgPairs MsgPairs -> MsgPairs [ctor assoc comm id: $none] .
384
    op _$$$;;;$$$_ : [MsgPairs] [MsgPairs] -> [MsgPairs] [ctor assoc comm id: $none] .
385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513
    ---Stores the information on an invalid substitution. The Python code
    ---invoking this Maude code then scans the output for the presence of
    ---this term. If the Python code finds this term, then it extracts the
    ---arguments and uses them to build a (hopefully) useful error message.
    ---Second argument is the list of line numbers on which the offending messages are defined.
    op $$$notAFunction : MsgPairs -> [MsgPairs] .

endfm

fmod SPECIFICATION-SYNTAX is
    protecting SECTION-SYNTAX .
    protecting PROTOCOL-SYNTAX .
    protecting INTRUDER-SYNTAX .
    protecting ATTACK-SYNTAX .
endfm

fmod PSL-SYNTAX is
    protecting TRANSLATION-SYNTAX .
    protecting SPECIFICATION-SYNTAX .
endfm

fmod TRANSLATION-TO-MAUDE-NPA-SYNTAX is
    protecting PSL-SYNTAX .

    sort ModuleNPA .
    subsort ModuleNPA < TranslationData .

    op fmod PROTOCOL-SPECIFICATION is 
        protecting PROTOCOL-EXAMPLE-SYMBOLS .
        protecting DEFINITION-PROTOCOL-RULES .
        protecting DEFINITION-CONSTRAINTS-INPUT .
        eq STRANDS-DOLEVYAO =_[nonexec] .
        eq STRANDS-PROTOCOL =_[nonexec] .
        _ endfm : StrandSet StrandSet AttackList -> ModuleNPA 
        ---The format string to end all format strings.
            [format(n o d d d d n o d n o d n o d d d d d d n o d d d d d d n o d)] .

    op fmod PROTOCOL-SPECIFICATION is 
        protecting PROTOCOL-EXAMPLE-SYMBOLS .
        protecting DEFINITION-PROTOCOL-RULES .
        protecting DEFINITION-CONSTRAINTS-INPUT .
        eq STRANDS-DOLEVYAO =_[nonexec] .
        eq STRANDS-PROTOCOL =_[nonexec] .
        endfm : StrandSet StrandSet -> ModuleNPA 
            [format(n o d d d d n o d n o d n o d d d d d d n o d d d d d n o d)] .


        sort AttackEq AttackList VarDecls .
        subsort AttackEq VarDecls < AttackList .
        op eq ATTACK-STATE`(_`) = _[nonexec] . : Nat System -> AttackEq 
        [format(d d d d d d d d d d d n)] .
        op $emptyAttackList : -> AttackList .
        op __ : AttackList AttackList -> AttackList 
            [ctor assoc id: $emptyAttackList] .

        subsort VarDecl < VarDecls .
        op __ : VarDecls VarDecls -> VarDecls [ctor ditto] .

    op $translate : -> TranslationData . 
    ---Extracts the strands from a set of mappings from roles to strands.
    op convert : StrandData -> StrandSet .
    op shiftBarLeft : Strand -> Strand .

endfm


---(
    Syntax for protocol composition.
---)
fmod COMPOSITION-SYNTAX is
    protecting TRANSLATION-SYNTAX .
    protecting SECTION-SYNTAX .
    protecting MAPPINGS .
    protecting TRANSLATION-TO-MAUDE-NPA-SYNTAX .

    sort Composition CompType .
    ---One-to-One composition
    op _;1_ : Role Role -> CompType [prec 25] .
    ---One-to-many composition
    op _;*_ : Role Role -> CompType [prec 25] .
    op _:_.[_] : CompType Mappings Nat -> Composition [prec 26] .
    op __ : Composition Composition -> 
        Composition [gather(e E) prec 28 id: emptyComp] .
    op emptyComp : -> Composition .

    op var_:_. : Role NPA-Sort -> VarDecl .
    op ROLE : -> Role .

    ---(
        The TranslationData is the PSL data of one of the protocols being
        composed.
        As a part of the Python parsing, the composing sections are split
        up and assigned a number based on the order the section appears
        in the specification.
        Each protocol is assigned a number by the Python script based on the
        order in the composing statement. translate takes that number
        as first argument.
        Note that the translation performed inside of "translate" stops
        just before being converted into a Maude-NPA module.
    ---)
    op $translate : Nat TranslationData -> TranslationData .
    ---Marks that the PSL specification in the second argument has been
    ---completely translated.
    op $translated : Nat TranslationData -> TranslationData .

    ---(
    The following sorts and operators contain the information about which
    protocols are being composed.
    Essentially we convert a block of the form
    spec A;B is
        composing A ; B .
    comp A ; B 
        S_1

    into
    translate(1, codeA)
    translate(2, codeB) 
    [comp(1, 2) |-> S_1]
    Then, after codeA and codeB have been translated, we use the information in 
    S_1 to generate the composed protocol.
    ---)
    sort Composing CompList .
    op comp : Nat Nat -> Composing .
    op _|->_ : Composing Composition -> CompList [prec 30] .
    op $noCM : -> CompList .
    op __ : CompList CompList -> CompList [assoc id: $noCM prec 32] .
    op [_] : CompList -> TranslationData .

endfm