in sectrace.maude

mod EXT-TEST-INTER is

protecting SECTRACE .

***(

   Configuration:
   
			   a
			 C1 -----|
				 |b
	       a     a	 b     a | c	 a   b	   a   b    a
	     C2 ----- SG1 ----- SG2 ----- SG3 ----- SG4 ---- S

   C1 << SG2,SG3,S
   C2 << SG1,SG3,S
   SG1 << SG2
   SG3 << SG4,S
   SG4 << S

   Expected result:
      
		  C1 ----- SG2 ----- SG3 ----- SG4 ----- S
		     =====               =====     =====
		     ===============

	     C2 ----- SG1 ----- SG2 ----- SG3 ----- SG4 ----- S
		=====     =====               =====     =====
		=========================

)

op network : -> State .

eq network = 
    shost(node("C1"))
    shost(node("C2"))
    shost(node("SG1"))
    shost(node("SG2"))
    shost(node("SG3"))
    shost(node("SG4"))
    shost(node("S"))

    sgw(node("SG1"))
    sgw(node("SG2"))
    sgw(node("SG3"))
    sgw(node("SG4"))

    sectraced(node("C1"))
    sectraced(node("C2"))
    sectraced(node("SG1"))
    sectraced(node("SG2"))
    sectraced(node("SG3"))
    sectraced(node("SG4"))
    sectraced(node("S"))

    subnet(sAddrSet(addr("C1a")) sAddrSet(addr("SG2b")))
    subnet(sAddrSet(addr("C2a")) sAddrSet(addr("SG1a")))
    subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a")))
    subnet(sAddrSet(addr("SG2c")) sAddrSet(addr("SG3a")))
    subnet(sAddrSet(addr("SG3b")) sAddrSet(addr("SG4a")))
    subnet(sAddrSet(addr("SG4b")) sAddrSet(addr("Sa")))

    interfaces(node("C1"),sAddrSet(addr("C1a")))
    interfaces(node("C2"),sAddrSet(addr("C2a")))
    interfaces(node("SG1"),sAddrSet(addr("SG1a")) sAddrSet(addr("SG1b")))
    interfaces(node("SG2"),sAddrSet(addr("SG2a")) sAddrSet(addr("SG2b")) sAddrSet(addr("SG2c")))
    interfaces(node("SG3"),sAddrSet(addr("SG3a")) sAddrSet(addr("SG3b")))
    interfaces(node("SG4"),sAddrSet(addr("SG4a")) sAddrSet(addr("SG4b")))
    interfaces(node("S"),sAddrSet(addr("Sa")))

    routetab(node("C1"),
       sRouteList(route(addr("C1a"), addr("C1a"), addr("C1a")))
       sRouteList(route(addr("C2a"), addr("C1a"), addr("SG2b")))
       sRouteList(route(addr("SG1a"), addr("C1a"), addr("SG2b")))
       sRouteList(route(addr("SG1b"), addr("C1a"), addr("SG2b")))
       sRouteList(route(addr("SG2a"), addr("C1a"), addr("SG2b")))
       sRouteList(route(addr("SG2b"), addr("C1a"), addr("SG2b")))
       sRouteList(route(addr("SG2c"), addr("C1a"), addr("SG2b")))
       sRouteList(route(addr("SG3a"), addr("C1a"), addr("SG2b")))
       sRouteList(route(addr("SG3b"), addr("C1a"), addr("SG2b")))
       sRouteList(route(addr("SG4a"), addr("C1a"), addr("SG2b")))
       sRouteList(route(addr("SG4b"), addr("C1a"), addr("SG2b")))
       sRouteList(route(addr("Sa"), addr("C1a"), addr("SG2b"))))

    routetab(node("C2"),
       sRouteList(route(addr("C1a"), addr("C2a"), addr("SG1a")))
       sRouteList(route(addr("C2a"), addr("C2a"), addr("C2a")))
       sRouteList(route(addr("SG1a"), addr("C2a"), addr("SG1a")))
       sRouteList(route(addr("SG1b"), addr("C2a"), addr("SG1a")))
       sRouteList(route(addr("SG2a"), addr("C2a"), addr("SG1a")))
       sRouteList(route(addr("SG2b"), addr("C2a"), addr("SG1a")))
       sRouteList(route(addr("SG2c"), addr("C2a"), addr("SG1a")))
       sRouteList(route(addr("SG3a"), addr("C2a"), addr("SG1a")))
       sRouteList(route(addr("SG3b"), addr("C2a"), addr("SG1a")))
       sRouteList(route(addr("SG4a"), addr("C2a"), addr("SG1a")))
       sRouteList(route(addr("SG4b"), addr("C2a"), addr("SG1a")))
       sRouteList(route(addr("Sa"), addr("C2a"), addr("SG1a"))))

    routetab(node("SG1"),
       sRouteList(route(addr("C1a"), addr("SG1b"), addr("SG2a")))
       sRouteList(route(addr("C2a"), addr("SG1a"), addr("C2a")))
       sRouteList(route(addr("SG1a"), addr("SG1a"), addr("SG1a")))
       sRouteList(route(addr("SG1b"), addr("SG1b"), addr("SG1b")))
       sRouteList(route(addr("SG2a"), addr("SG1b"), addr("SG2a")))
       sRouteList(route(addr("SG2b"), addr("SG1b"), addr("SG2a")))
       sRouteList(route(addr("SG2c"), addr("SG1b"), addr("SG2a")))
       sRouteList(route(addr("SG3a"), addr("SG1b"), addr("SG2a")))
       sRouteList(route(addr("SG3b"), addr("SG1b"), addr("SG2a")))
       sRouteList(route(addr("SG4a"), addr("SG1b"), addr("SG2a")))
       sRouteList(route(addr("SG4b"), addr("SG1b"), addr("SG2a")))
       sRouteList(route(addr("Sa"), addr("SG1b"), addr("SG2a"))))

    routetab(node("SG2"),
       sRouteList(route(addr("C1a"), addr("SG2b"), addr("C1a")))
       sRouteList(route(addr("C2a"), addr("SG2a"), addr("SG1b")))
       sRouteList(route(addr("SG1a"), addr("SG2a"), addr("SG1b")))
       sRouteList(route(addr("SG1b"), addr("SG2a"), addr("SG1b")))
       sRouteList(route(addr("SG2a"), addr("SG2a"), addr("SG2a")))
       sRouteList(route(addr("SG2b"), addr("SG2b"), addr("SG2b")))
       sRouteList(route(addr("SG2c"), addr("SG2c"), addr("SG2c")))
       sRouteList(route(addr("SG3a"), addr("SG2c"), addr("SG3a")))
       sRouteList(route(addr("SG3b"), addr("SG2c"), addr("SG3a")))
       sRouteList(route(addr("SG4a"), addr("SG2c"), addr("SG3a")))
       sRouteList(route(addr("SG4b"), addr("SG2c"), addr("SG3a")))
       sRouteList(route(addr("Sa"), addr("SG2c"), addr("SG3a"))))

    routetab(node("SG3"),
       sRouteList(route(addr("C1a"), addr("SG3a"), addr("SG2c")))
       sRouteList(route(addr("C2a"), addr("SG3a"), addr("SG2c")))
       sRouteList(route(addr("SG1a"), addr("SG3a"), addr("SG2c")))
       sRouteList(route(addr("SG1b"), addr("SG3a"), addr("SG2c")))
       sRouteList(route(addr("SG2a"), addr("SG3a"), addr("SG2c")))
       sRouteList(route(addr("SG2b"), addr("SG3a"), addr("SG2c")))
       sRouteList(route(addr("SG2c"), addr("SG3a"), addr("SG2c")))
       sRouteList(route(addr("SG3a"), addr("SG3a"), addr("SG3a")))
       sRouteList(route(addr("SG3b"), addr("SG3b"), addr("SG3b")))
       sRouteList(route(addr("SG4a"), addr("SG3b"), addr("SG4a")))
       sRouteList(route(addr("SG4b"), addr("SG3b"), addr("SG4a")))
       sRouteList(route(addr("Sa"), addr("SG3b"), addr("SG4a"))))

    routetab(node("SG4"),
       sRouteList(route(addr("C1a"), addr("SG4a"), addr("SG3b")))
       sRouteList(route(addr("C2a"), addr("SG4a"), addr("SG3b")))
       sRouteList(route(addr("SG1a"), addr("SG4a"), addr("SG3b")))
       sRouteList(route(addr("SG1b"), addr("SG4a"), addr("SG3b")))
       sRouteList(route(addr("SG2a"), addr("SG4a"), addr("SG3b")))
       sRouteList(route(addr("SG2b"), addr("SG4a"), addr("SG3b")))
       sRouteList(route(addr("SG2c"), addr("SG4a"), addr("SG3b")))
       sRouteList(route(addr("SG3a"), addr("SG4a"), addr("SG3b")))
       sRouteList(route(addr("SG3b"), addr("SG4a"), addr("SG3b")))
       sRouteList(route(addr("SG4a"), addr("SG4a"), addr("SG4a")))
       sRouteList(route(addr("SG4b"), addr("SG4b"), addr("SG4b")))
       sRouteList(route(addr("Sa"), addr("SG4b"), addr("Sa"))))

    routetab(node("S"),
       sRouteList(route(addr("C1a"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("C2a"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("SG1a"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("SG1b"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("SG2a"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("SG2b"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("SG2c"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("SG3a"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("SG3b"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("SG4a"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("SG4b"), addr("Sa"), addr("SG4b")))
       sRouteList(route(addr("Sa"), addr("Sa"), addr("Sa"))))

    rootinfo(node("C1"), addr("CAC1"), sAddrSet(addr("CAC1")))
    rootinfo(node("C2"), addr("CAC2"), sAddrSet(addr("CAC2")))
    rootinfo(node("SG1"), addr("CASG1"), sAddrSet(addr("CASG1")) sAddrSet(addr("CAC2")))
    rootinfo(node("SG2"), addr("CASG2"), sAddrSet(addr("CASG2")) sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")))
    rootinfo(node("SG3"), addr("CASG3"), sAddrSet(addr("CASG3")) sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")))
    rootinfo(node("SG4"), addr("CASG4"), sAddrSet(addr("CASG4")) sAddrSet(addr("CASG3")))
    rootinfo(node("S"), addr("CAS"), sAddrSet(addr("CAS")) sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4")))

    sadb(node("C1"),eSASet)
    sadb(node("C2"),eSASet)
    sadb(node("SG1"),eSASet)
    sadb(node("SG2"),eSASet)
    sadb(node("SG3"),eSASet)
    sadb(node("SG4"),eSASet)
    sadb(node("S"),eSASet)

    spdb(node("C1"),eSPList,
                   sSPList(sp(isinitiation,eSAList))
                   sSPList(sp(isresponse,eSAList)))
    spdb(node("C2"),eSPList,
                   sSPList(sp(isinitiation,eSAList))
                   sSPList(sp(isresponse,eSAList)))
    spdb(node("SG1"),eSPList,
                   sSPList(sp(isinitiation,eSAList))
                   sSPList(sp(isresponse,eSAList)))
    spdb(node("SG2"),eSPList,
                   sSPList(sp(isinitiation,eSAList))
                   sSPList(sp(isresponse,eSAList)))
    spdb(node("SG3"),eSPList,
                   sSPList(sp(isinitiation,eSAList))
                   sSPList(sp(isresponse,eSAList)))
    spdb(node("SG4"),eSPList,
                   sSPList(sp(isinitiation,eSAList))
                   sSPList(sp(isresponse,eSAList)))
    spdb(node("S"),eSPList,
                   sSPList(sp(isinitiation,eSAList))
                   sSPList(sp(isresponse,eSAList))) .


op start : -> State .
op terminated : -> State .

rl start =>
   sectrace-start(node("C1"), addr("C1a"), addr("Sa"))
   sectrace-start(node("C2"), addr("C2a"), addr("Sa")) .

rl sectrace-terminated(node("C1"), addr("C1a"), addr("Sa")) 
   sectrace-terminated(node("C2"), addr("C2a"), addr("Sa")) => 
   terminated .
   
endm

--- set trace on .
--- set trace select on .
--- trace select select .
--- trace select ipsec-send ipsec-delivered .

*** rew network start .

search (network start) =>! state:State .
--- gives 24 solutions (takes a while)

--- model checking is used to obtain traces of solutions:

in model-checker .

mod EXT-TEST-INTER-MODEL-CHECK is
   protecting MODEL-CHECKER .
   protecting EXT-TEST-INTER .

   ops soln1 soln2 soln3 soln4 : -> State .
   
   rl [stop] :	
        terminated
	sadb(node("S"), sSASet(sa(addr("SG4a"), addr("Sa"), 0))) =>
	soln1 .

   rl [stop] :	
        terminated
	sadb(node("S"), sSASet(sa(addr("SG3a"), addr("Sa"), 0))) =>
        soln2 .
   
   rl [stop] :	
        terminated
	sadb(node("S"), sSASet(sa(addr("SG4a"), addr("Sa"), 0)) sSASet(sa(addr("SG3a"), addr("Sa"), 0))) =>
	soln3 .

   rl [stop] :	
        ipsec-received(node("S"), addr("Sa"), eAttrSet, sSAList(sa(addr("SG3a"), addr("Sa"), 0)), 
          ip(addr("C1a"), addr("SG4a"), sareq(addr("C1a"), addr("Sa"), addr("SG4a"), addr("Sa")))) =>
        soln4 .

   op done : -> Prop .
   ops soln-type1 soln-type2 soln-type3 soln-type4 : -> Prop .
   var S : State .
   eq (S terminated) |= done = true .
   eq (S soln1) |= soln-type1 = true .
   eq (S soln2) |= soln-type2 = true .
   eq (S soln3) |= soln-type3 = true .
   eq (S soln4) |= soln-type4 = true .

endm

red network start |= ~ <> soln-type1 .
red network start |= ~ <> soln-type2 .
red network start |= ~ <> soln-type3 .
red network start |= ~ <> soln-type4 .