reduce in EXT-TEST-INTER-MODEL-CHECK : network start |= ~ <> soln-type3 . rewrites: 5994428 in 5120ms cpu (5160ms real) (1170786 rewrites/second) result ModelCheckResult: counterexample({start subnet(sAddrSet(addr("C2a")) sAddrSet(addr("SG1a"))) subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a"))) subnet(sAddrSet(addr("C1a")) sAddrSet(addr("SG2b"))) subnet(sAddrSet(addr("SG2c")) sAddrSet(addr("SG3a"))) subnet(sAddrSet(addr("SG3b")) sAddrSet(addr("SG4a"))) subnet(sAddrSet(addr("SG4b")) sAddrSet(addr("Sa"))) shost(node("C1")) shost(node("C2")) shost(node("S")) shost(node("SG1")) shost(node("SG2")) shost(node("SG3")) shost(node("SG4")) sgw(node("SG1")) sgw(node("SG2")) sgw(node("SG3")) sgw(node("SG4")) sectraced(node("C1")) sectraced(node("C2")) sectraced(node("S")) sectraced(node("SG1")) sectraced(node("SG2")) sectraced(node("SG3")) sectraced(node("SG4")) interfaces(node("C1"), sAddrSet(addr("C1a"))) interfaces(node("C2"), sAddrSet(addr("C2a"))) interfaces(node("S"), sAddrSet(addr("Sa"))) 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"))) 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("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")))) 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")))) sadb(node("C1"), eSASet) sadb(node("C2"), eSASet) sadb(node("S"), eSASet) sadb(node("SG1"), eSASet) sadb(node("SG2"), eSASet) sadb(node("SG3"), eSASet) sadb(node("SG4"), eSASet) rootinfo(node("C1"), addr("CAC1"), sAddrSet(addr("CAC1"))) rootinfo(node("C2"), addr("CAC2"), sAddrSet(addr("CAC2"))) rootinfo(node("S"), addr("CAS"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CAS")) sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) rootinfo(node("SG1"), addr("CASG1"), sAddrSet(addr("CAC2")) sAddrSet(addr("CASG1"))) rootinfo(node("SG2"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")) sAddrSet(addr("CASG2"))) rootinfo(node("SG3"), addr("CASG3"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CASG3"))) rootinfo(node("SG4"), addr("CASG4"), sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) 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("S"), 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))),unlabeled} {subnet(sAddrSet(addr("C2a")) sAddrSet(addr( "SG1a"))) subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a"))) subnet(sAddrSet(addr("C1a")) sAddrSet(addr("SG2b"))) subnet(sAddrSet(addr("SG2c")) sAddrSet(addr("SG3a"))) subnet(sAddrSet(addr("SG3b")) sAddrSet(addr("SG4a"))) subnet(sAddrSet(addr("SG4b")) sAddrSet(addr("Sa"))) shost(node("C1")) shost(node("C2")) shost(node("S")) shost(node("SG1")) shost(node("SG2")) shost(node("SG3")) shost(node("SG4")) sgw(node("SG1")) sgw(node("SG2")) sgw(node("SG3")) sgw(node("SG4")) sectraced(node("C1")) sectraced(node("C2")) sectraced(node("S")) sectraced(node("SG1")) sectraced(node("SG2")) sectraced(node("SG3")) sectraced(node("SG4")) interfaces(node("C1"), sAddrSet(addr("C1a"))) interfaces(node("C2"), sAddrSet(addr("C2a"))) interfaces(node("S"), sAddrSet(addr("Sa"))) 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"))) 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("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")))) 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")))) sadb(node("C1"), eSASet) sadb(node("C2"), eSASet) sadb(node("S"), eSASet) sadb(node("SG1"), eSASet) sadb(node("SG2"), eSASet) sadb(node("SG3"), eSASet) sadb(node("SG4"), eSASet) rootinfo(node("C1"), addr("CAC1"), sAddrSet(addr("CAC1"))) rootinfo(node("C2"), addr("CAC2"), sAddrSet(addr("CAC2"))) rootinfo(node("S"), addr("CAS"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CAS")) sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) rootinfo(node("SG1"), addr("CASG1"), sAddrSet(addr("CAC2")) sAddrSet(addr("CASG1"))) rootinfo(node("SG2"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")) sAddrSet(addr("CASG2"))) rootinfo(node("SG3"), addr("CASG3"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CASG3"))) rootinfo(node("SG4"), addr("CASG4"), sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) 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("S"), 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))) sectrace-start(node("C1"), addr("C1a"), addr("Sa")) sectrace-start(node("C2"), addr("C2a"), addr("Sa")),'sectrace-start} {subnet(sAddrSet(addr("C2a")) sAddrSet(addr("SG1a"))) subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a"))) subnet(sAddrSet(addr("C1a")) sAddrSet(addr("SG2b"))) subnet(sAddrSet(addr("SG2c")) sAddrSet(addr("SG3a"))) subnet(sAddrSet(addr("SG3b")) sAddrSet(addr("SG4a"))) subnet(sAddrSet(addr("SG4b")) sAddrSet(addr("Sa"))) shost(node("C1")) shost(node("C2")) shost(node("S")) shost(node("SG1")) shost(node("SG2")) shost(node("SG3")) shost(node("SG4")) sgw(node("SG1")) sgw(node("SG2")) sgw(node("SG3")) sgw(node("SG4")) sectraced(node("C1")) sectraced(node("C2")) sectraced(node("S")) sectraced(node("SG1")) sectraced(node("SG2")) sectraced(node("SG3")) sectraced(node("SG4")) interfaces(node("C1"), sAddrSet(addr("C1a"))) interfaces(node("C2"), sAddrSet(addr("C2a"))) interfaces(node("S"), sAddrSet(addr("Sa"))) 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"))) ipsec-send(node("C1"), ip(addr("C1a"), addr("Sa"), rreq(addr("C1a"), 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("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")))) 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")))) sadb(node("C1"), eSASet) sadb(node("C2"), eSASet) sadb(node("S"), eSASet) sadb(node("SG1"), eSASet) sadb(node("SG2"), eSASet) sadb(node("SG3"), eSASet) sadb(node("SG4"), eSASet) rootinfo(node("C1"), addr("CAC1"), sAddrSet(addr("CAC1"))) rootinfo(node("C2"), addr("CAC2"), sAddrSet(addr("CAC2"))) rootinfo(node("S"), addr("CAS"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CAS")) sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) rootinfo(node("SG1"), addr("CASG1"), sAddrSet(addr("CAC2")) sAddrSet(addr("CASG1"))) rootinfo(node("SG2"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")) sAddrSet(addr("CASG2"))) rootinfo(node("SG3"), addr("CASG3"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CASG3"))) rootinfo(node("SG4"), addr("CASG4"), sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) 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("S"), 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))) sectrace-start(node("C2"), addr("C2a"), addr("Sa")) sectrace-rreq(node("C1"), addr("C1a"), addr("Sa"), sMessageList(rreq(addr("C1a"), addr("Sa"))), eMessageList),'ipsec-send} {subnet(sAddrSet(addr("C2a")) sAddrSet(addr("SG1a"))) subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a"))) subnet(sAddrSet(addr("C1a")) sAddrSet(addr("SG2b"))) subnet(sAddrSet(addr("SG2c")) sAddrSet(addr("SG3a"))) subnet(sAddrSet(addr("SG3b")) sAddrSet(addr("SG4a"))) subnet(sAddrSet(addr("SG4b")) sAddrSet(addr("Sa"))) shost(node("C1")) shost(node("C2")) shost(node("S")) shost(node("SG1")) shost(node("SG2")) shost(node("SG3")) shost(node("SG4")) sgw(node("SG1")) sgw(node("SG2")) sgw(node("SG3")) sgw(node("SG4")) sectraced(node("C1")) sectraced(node("C2")) sectraced(node("S")) sectraced(node("SG1")) sectraced(node("SG2")) sectraced(node("SG3")) sectraced(node("SG4")) interfaces(node("C1"), sAddrSet(addr("C1a"))) interfaces(node("C2"), sAddrSet(addr("C2a"))) interfaces(node("S"), sAddrSet(addr("Sa"))) 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"))) ip-send(node("C1"), ip(addr("C1a"), addr("Sa"), rreq(addr("C1a"), 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("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")))) 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")))) sadb(node("C1"), eSASet) sadb(node("C2"), eSASet) sadb(node("S"), eSASet) sadb(node("SG1"), eSASet) sadb(node("SG2"), eSASet) sadb(node("SG3"), eSASet) sadb(node("SG4"), eSASet) rootinfo(node("C1"), addr("CAC1"), sAddrSet(addr("CAC1"))) rootinfo(node("C2"), addr("CAC2"), sAddrSet(addr("CAC2"))) rootinfo(node("S"), addr("CAS"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CAS")) sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) rootinfo(node("SG1"), addr("CASG1"), sAddrSet(addr("CAC2")) sAddrSet(addr("CASG1"))) rootinfo(node("SG2"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")) sAddrSet(addr("CASG2"))) rootinfo(node("SG3"), addr("CASG3"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CASG3"))) rootinfo(node("SG4"), addr("CASG4"), sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) 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("S"), 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))) sectrace-start(node("C2"), addr("C2a"), addr("Sa")) sectrace-rreq(node("C1"), addr("C1a"), addr("Sa"), sMessageList(rreq(addr("C1a"), addr("Sa"))), eMessageList),'ip-receive} {subnet(sAddrSet(addr("C2a")) sAddrSet(addr("SG1a"))) subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a"))) subnet(sAddrSet(addr("C1a")) sAddrSet(addr("SG2b"))) subnet(sAddrSet(addr("SG2c")) sAddrSet(addr("SG3a"))) subnet(sAddrSet(addr("SG3b")) sAddrSet(addr("SG4a"))) subnet(sAddrSet(addr("SG4b")) sAddrSet(addr("Sa"))) shost(node("C1")) shost(node("C2")) shost(node("S")) shost(node("SG1")) shost(node("SG2")) shost(node("SG3")) shost(node("SG4")) sgw(node("SG1")) sgw(node("SG2")) sgw(node("SG3")) sgw(node("SG4")) sectraced(node("C1")) sectraced(node("C2")) sectraced(node("S")) sectraced(node("SG1")) sectraced(node("SG2")) sectraced(node("SG3")) sectraced(node("SG4")) interfaces(node("C1"), sAddrSet(addr("C1a"))) interfaces(node("C2"), sAddrSet(addr("C2a"))) interfaces(node("S"), sAddrSet(addr("Sa"))) 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"))) 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("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")))) 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")))) sadb(node("C1"), eSASet) sadb(node("C2"), eSASet) sadb(node("S"), eSASet) sadb(node("SG1"), eSASet) sadb(node("SG2"), eSASet) sadb(node("SG3"), eSASet) sadb(node("SG4"), eSASet) ip-received(node("SG2"), addr("SG2b"), ip(addr("C1a"), addr("Sa"), rreq(addr("C1a"), addr("Sa")))) rootinfo(node("C1"), addr("CAC1"), sAddrSet(addr("CAC1"))) rootinfo(node("C2"), addr("CAC2"), sAddrSet(addr("CAC2"))) rootinfo(node("S"), addr("CAS"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CAS")) sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) rootinfo(node("SG1"), addr("CASG1"), sAddrSet(addr("CAC2")) sAddrSet(addr("CASG1"))) rootinfo(node("SG2"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")) sAddrSet(addr("CASG2"))) rootinfo(node("SG3"), addr("CASG3"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CASG3"))) rootinfo(node("SG4"), addr("CASG4"), sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) 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("S"), 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))) sectrace-start(node("C2"), addr("C2a"), addr("Sa")) sectrace-rreq(node("C1"), addr("C1a"), addr("Sa"), sMessageList(rreq(addr("C1a"), addr("Sa"))), eMessageList),'ipsec-receive} {subnet(sAddrSet(addr( "C2a")) sAddrSet(addr("SG1a"))) subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a"))) subnet(sAddrSet(addr("C1a")) sAddrSet(addr("SG2b"))) subnet(sAddrSet(addr("SG2c")) sAddrSet(addr("SG3a"))) subnet(sAddrSet(addr("SG3b")) sAddrSet(addr("SG4a"))) subnet(sAddrSet(addr("SG4b")) sAddrSet(addr("Sa"))) shost(node("C1")) shost(node("C2")) shost(node("S")) shost(node("SG1")) shost(node("SG2")) shost(node("SG3")) shost(node("SG4")) sgw(node("SG1")) sgw(node("SG2")) sgw(node("SG3")) sgw(node("SG4")) sectraced(node("C1")) sectraced(node("C2")) sectraced(node("S")) sectraced(node("SG1")) sectraced(node("SG2")) sectraced(node("SG3")) sectraced(node("SG4")) interfaces(node("C1"), sAddrSet(addr("C1a"))) interfaces(node("C2"), sAddrSet(addr("C2a"))) interfaces(node("S"), sAddrSet(addr("Sa"))) 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"))) 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("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")))) 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")))) sadb(node("C1"), eSASet) sadb(node("C2"), eSASet) sadb(node("S"), eSASet) sadb(node("SG1"), eSASet) sadb(node("SG2"), eSASet) sadb(node("SG3"), eSASet) sadb(node("SG4"), eSASet) rootinfo(node("C1"), addr("CAC1"), sAddrSet(addr("CAC1"))) rootinfo(node("C2"), addr("CAC2"), sAddrSet(addr("CAC2"))) rootinfo(node("S"), addr("CAS"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CAS")) sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) rootinfo(node("SG1"), addr("CASG1"), sAddrSet(addr("CAC2")) sAddrSet(addr("CASG1"))) rootinfo(node("SG2"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")) sAddrSet(addr("CASG2"))) rootinfo(node("SG3"), addr("CASG3"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CASG3"))) rootinfo(node("SG4"), addr("CASG4"), sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) 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("S"), 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))) sectrace-start(node("C2"), addr("C2a"), addr("Sa")) ipsec-received(node("SG2"), addr("SG2b"), eAttrSet, eSAList, ip(addr("C1a"), addr("Sa"), rreq(addr("C1a"), addr("Sa")))) sectrace-rreq(node("C1"), addr("C1a"), addr("Sa"), sMessageList(rreq(addr("C1a"), addr("Sa"))), eMessageList),'ipsec-discard} {subnet(sAddrSet(addr( "C2a")) sAddrSet(addr("SG1a"))) subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a"))) subnet(sAddrSet(addr("C1a")) sAddrSet(addr("SG2b"))) subnet(sAddrSet(addr("SG2c")) sAddrSet(addr("SG3a"))) subnet(sAddrSet(addr("SG3b")) sAddrSet(addr("SG4a"))) subnet(sAddrSet(addr("SG4b")) sAddrSet(addr("Sa"))) shost(node("C1")) shost(node("C2")) shost(node("S")) shost(node("SG1")) shost(node("SG2")) shost(node("SG3")) shost(node("SG4")) sgw(node("SG1")) sgw(node("SG2")) sgw(node("SG3")) sgw(node("SG4")) sectraced(node("C1")) sectraced(node("C2")) sectraced(node("S")) sectraced(node("SG1")) sectraced(node("SG2")) sectraced(node("SG3")) sectraced(node("SG4")) interfaces(node("C1"), sAddrSet(addr("C1a"))) interfaces(node("C2"), sAddrSet(addr("C2a"))) interfaces(node("S"), sAddrSet(addr("Sa"))) 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"))) 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("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")))) 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")))) sadb(node("C1"), eSASet) sadb(node("C2"), eSASet) sadb(node("S"), eSASet) sadb(node("SG1"), eSASet) sadb(node("SG2"), eSASet) sadb(node("SG3"), eSASet) sadb(node("SG4"), eSASet) rootinfo(node("C1"), addr("CAC1"), sAddrSet(addr("CAC1"))) rootinfo(node("C2"), addr("CAC2"), sAddrSet(addr("CAC2"))) rootinfo(node("S"), addr("CAS"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CAS")) sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) rootinfo(node("SG1"), addr("CASG1"), sAddrSet(addr("CAC2")) sAddrSet(addr("CASG1"))) rootinfo(node("SG2"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")) sAddrSet(addr("CASG2"))) rootinfo(node("SG3"), addr("CASG3"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CASG3"))) rootinfo(node("SG4"), addr("CASG4"), sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) 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("S"), 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))) sectrace-start(node("C2"), addr("C2a"), addr("Sa")) ipsec-delivered(node("SG2"), addr("SG2b"), sAttrSet(discard), eSAList, ip(addr("C1a"), addr("Sa"), rreq(addr("C1a"), addr("Sa")))) sectrace-rreq(node("C1"), addr("C1a"), addr("Sa"), sMessageList(rreq(addr("C1a"), addr("Sa"))), eMessageList),'sectraced-receive-unauth-rreq} {subnet( sAddrSet(addr("C2a")) sAddrSet(addr("SG1a"))) subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a"))) subnet(sAddrSet(addr("C1a")) sAddrSet(addr("SG2b"))) subnet(sAddrSet(addr("SG2c")) sAddrSet(addr("SG3a"))) subnet(sAddrSet(addr("SG3b")) sAddrSet(addr("SG4a"))) subnet(sAddrSet(addr("SG4b")) sAddrSet(addr("Sa"))) shost(node("C1")) shost(node("C2")) shost(node("S")) shost(node("SG1")) shost(node("SG2")) shost(node("SG3")) shost(node("SG4")) sgw(node("SG1")) sgw(node("SG2")) sgw(node("SG3")) sgw(node("SG4")) sectraced(node("C1")) sectraced(node("C2")) sectraced(node("S")) sectraced(node("SG1")) sectraced(node("SG2")) sectraced(node("SG3")) sectraced(node("SG4")) interfaces(node("C1"), sAddrSet(addr("C1a"))) interfaces(node("C2"), sAddrSet(addr("C2a"))) interfaces(node("S"), sAddrSet(addr("Sa"))) 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"))) ipsec-send(node("SG2"), ip(addr("SG2b"), addr("C1a"), rrep(addr("C1a"), addr("Sa"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")) sAddrSet(addr("CASG2")), false))) 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("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")))) 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")))) sadb(node("C1"), eSASet) sadb(node("C2"), eSASet) sadb(node("S"), eSASet) sadb(node("SG1"), eSASet) sadb(node("SG2"), eSASet) sadb(node("SG3"), eSASet) sadb(node("SG4"), eSASet) rootinfo(node("C1"), addr("CAC1"), sAddrSet(addr("CAC1"))) rootinfo(node("C2"), addr("CAC2"), sAddrSet(addr("CAC2"))) rootinfo(node("S"), addr("CAS"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CAS")) sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) rootinfo(node("SG1"), addr("CASG1"), sAddrSet(addr("CAC2")) sAddrSet(addr("CASG1"))) rootinfo(node("SG2"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")) sAddrSet(addr("CASG2"))) rootinfo(node("SG3"), addr("CASG3"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CASG3"))) rootinfo(node("SG4"), addr("CASG4"), sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) 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("S"), 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))) sectrace-start(node("C2"), addr("C2a"), addr("Sa")) sectrace-rreq(node("C1"), addr("C1a"), addr("Sa"), sMessageList(rreq(addr("C1a"), addr("Sa"))), eMessageList),'ipsec-send} {subnet(sAddrSet(addr("C2a")) sAddrSet(addr("SG1a"))) subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a"))) subnet(sAddrSet(addr("C1a")) sAddrSet(addr("SG2b"))) subnet(sAddrSet(addr("SG2c")) sAddrSet(addr("SG3a"))) subnet(sAddrSet(addr("SG3b")) sAddrSet(addr("SG4a"))) subnet(sAddrSet(addr("SG4b")) sAddrSet(addr("Sa"))) shost(node("C1")) shost(node("C2")) shost(node("S")) shost(node("SG1")) shost(node("SG2")) shost(node("SG3")) shost(node("SG4")) sgw(node("SG1")) sgw(node("SG2")) sgw(node("SG3")) sgw(node("SG4")) sectraced(node("C1")) sectraced(node("C2")) sectraced(node("S")) sectraced(node("SG1")) sectraced(node("SG2")) sectraced(node("SG3")) sectraced(node("SG4")) interfaces(node("C1"), sAddrSet(addr("C1a"))) interfaces(node("C2"), sAddrSet(addr("C2a"))) interfaces(node("S"), sAddrSet(addr("Sa"))) 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"))) ip-send(node("SG2"), ip(addr("SG2b"), addr("C1a"), rrep(addr("C1a"), addr("Sa"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")) sAddrSet( addr("CASG2")), false))) 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("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")))) 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")))) sadb(node("C1"), eSASet) sadb(node("C2"), eSASet) sadb(node("S"), eSASet) sadb(node("SG1"), eSASet) sadb(node("SG2"), eSASet) sadb(node("SG3"), eSASet) sadb(node("SG4"), eSASet) rootinfo(node("C1"), addr("CAC1"), sAddrSet(addr("CAC1"))) rootinfo(node("C2"), addr("CAC2"), sAddrSet(addr("CAC2"))) rootinfo(node("S"), addr("CAS"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CAS")) sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) rootinfo(node("SG1"), addr("CASG1"), sAddrSet(addr("CAC2")) sAddrSet(addr("CASG1"))) rootinfo(node("SG2"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")) sAddrSet(addr("CASG2"))) rootinfo(node("SG3"), addr("CASG3"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CASG3"))) rootinfo(node("SG4"), addr("CASG4"), sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) 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("S"), 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))) sectrace-start(node("C2"), addr("C2a"), addr("Sa")) sectrace-rreq(node("C1"), addr("C1a"), addr("Sa"), sMessageList(rreq(addr("C1a"), addr("Sa"))), eMessageList),'ip-receive} {subnet(sAddrSet(addr("C2a")) sAddrSet(addr("SG1a"))) subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a"))) subnet(sAddrSet(addr("C1a")) sAddrSet(addr("SG2b"))) subnet(sAddrSet(addr("SG2c")) sAddrSet(addr("SG3a"))) subnet(sAddrSet(addr("SG3b")) sAddrSet(addr("SG4a"))) subnet(sAddrSet(addr("SG4b")) sAddrSet(addr("Sa"))) shost(node("C1")) shost(node("C2")) shost(node("S")) shost(node("SG1")) shost(node("SG2")) shost(node("SG3")) shost(node("SG4")) sgw(node("SG1")) sgw(node("SG2")) sgw(node("SG3")) sgw(node("SG4")) sectraced(node("C1")) sectraced(node("C2")) sectraced(node("S")) sectraced(node("SG1")) sectraced(node("SG2")) sectraced(node("SG3")) sectraced(node("SG4")) interfaces(node("C1"), sAddrSet(addr("C1a"))) interfaces(node("C2"), sAddrSet(addr("C2a"))) interfaces(node("S"), sAddrSet(addr("Sa"))) 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"))) 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("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")))) 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")))) sadb(node("C1"), eSASet) sadb(node("C2"), eSASet) sadb(node("S"), eSASet) sadb(node("SG1"), eSASet) sadb(node("SG2"), eSASet) sadb(node("SG3"), eSASet) sadb(node("SG4"), eSASet) ip-received(node("C1"), addr("C1a"), ip(addr("SG2b"), addr("C1a"), rrep(addr("C1a"), addr("Sa"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr( "CASG1")) sAddrSet(addr("CASG2")), false))) rootinfo(node("C1"), addr("CAC1"), sAddrSet(addr("CAC1"))) rootinfo(node("C2"), addr("CAC2"), sAddrSet(addr("CAC2"))) rootinfo(node("S"), addr("CAS"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CAS")) sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) rootinfo(node("SG1"), addr("CASG1"), sAddrSet(addr("CAC2")) sAddrSet(addr("CASG1"))) rootinfo(node("SG2"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")) sAddrSet(addr("CASG2"))) rootinfo(node("SG3"), addr("CASG3"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CASG3"))) rootinfo(node("SG4"), addr("CASG4"), sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) 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("S"), 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))) sectrace-start(node("C2"), addr("C2a"), addr("Sa")) sectrace-rreq(node("C1"), addr("C1a"), addr("Sa"), sMessageList(rreq(addr("C1a"), addr("Sa"))), eMessageList),'ipsec-receive} {subnet(sAddrSet(addr( "C2a")) sAddrSet(addr("SG1a"))) subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a"))) subnet(sAddrSet(addr("C1a")) sAddrSet(addr("SG2b"))) subnet(sAddrSet(addr("SG2c")) sAddrSet(addr("SG3a"))) subnet(sAddrSet(addr("SG3b")) sAddrSet(addr("SG4a"))) subnet(sAddrSet(addr("SG4b")) sAddrSet(addr("Sa"))) shost(node("C1")) shost(node("C2")) shost(node("S")) shost(node("SG1")) shost(node("SG2")) shost(node("SG3")) shost(node("SG4")) sgw(node("SG1")) sgw(node("SG2")) sgw(node("SG3")) sgw(node("SG4")) sectraced(node("C1")) sectraced(node("C2")) sectraced(node("S")) sectraced(node("SG1")) sectraced(node("SG2")) sectraced(node("SG3")) sectraced(node("SG4")) interfaces(node("C1"), sAddrSet(addr("C1a"))) interfaces(node("C2"), sAddrSet(addr("C2a"))) interfaces(node("S"), sAddrSet(addr("Sa"))) 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"))) 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("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")))) 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")))) sadb(node("C1"), eSASet) sadb(node("C2"), eSASet) sadb(node("S"), eSASet) sadb(node("SG1"), eSASet) sadb(node("SG2"), eSASet) sadb(node("SG3"), eSASet) sadb(node("SG4"), eSASet) rootinfo(node("C1"), addr("CAC1"), sAddrSet(addr("CAC1"))) rootinfo(node("C2"), addr("CAC2"), sAddrSet(addr("CAC2"))) rootinfo(node("S"), addr("CAS"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CAS")) sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) rootinfo(node("SG1"), addr("CASG1"), sAddrSet(addr("CAC2")) sAddrSet(addr("CASG1"))) rootinfo(node("SG2"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")) sAddrSet(addr("CASG2"))) rootinfo(node("SG3"), addr("CASG3"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CASG3"))) rootinfo(node("SG4"), addr("CASG4"), sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) 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("S"), 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))) sectrace-start(node("C2"), addr("C2a"), addr("Sa")) ipsec-received(node("C1"), addr("C1a"), eAttrSet, eSAList, ip(addr("SG2b"), addr("C1a"), rrep(addr("C1a"), addr("Sa"), addr("CASG2"), sAddrSet(addr( "CAC1")) sAddrSet(addr("CASG1")) sAddrSet(addr("CASG2")), false))) sectrace-rreq(node("C1"), addr("C1a"), addr("Sa"), sMessageList(rreq(addr("C1a"), addr("Sa"))), eMessageList),'ipsec-discard} {subnet(sAddrSet(addr( "C2a")) sAddrSet(addr("SG1a"))) subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a"))) subnet(sAddrSet(addr("C1a")) sAddrSet(addr("SG2b"))) subnet(sAddrSet(addr("SG2c")) sAddrSet(addr("SG3a"))) subnet(sAddrSet(addr("SG3b")) sAddrSet(addr("SG4a"))) subnet(sAddrSet(addr("SG4b")) sAddrSet(addr("Sa"))) shost(node("C1")) shost(node("C2")) shost(node("S")) shost(node("SG1")) shost(node("SG2")) shost(node("SG3")) shost(node("SG4")) sgw(node("SG1")) sgw(node("SG2")) sgw(node("SG3")) sgw(node("SG4")) sectraced(node("C1")) sectraced(node("C2")) sectraced(node("S")) sectraced(node("SG1")) sectraced(node("SG2")) sectraced(node("SG3")) sectraced(node("SG4")) interfaces(node("C1"), sAddrSet(addr("C1a"))) interfaces(node("C2"), sAddrSet(addr("C2a"))) interfaces(node("S"), sAddrSet(addr("Sa"))) 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"))) 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("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")))) 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")))) sadb(node("C1"), eSASet) sadb(node("C2"), eSASet) sadb(node("S"), eSASet) sadb(node("SG1"), eSASet) sadb(node("SG2"), eSASet) sadb(node("SG3"), eSASet) sadb(node("SG4"), eSASet) rootinfo(node("C1"), addr("CAC1"), sAddrSet(addr("CAC1"))) rootinfo(node("C2"), addr("CAC2"), sAddrSet(addr("CAC2"))) rootinfo(node("S"), addr("CAS"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CAS")) sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) rootinfo(node("SG1"), addr("CASG1"), sAddrSet(addr("CAC2")) sAddrSet(addr("CASG1"))) rootinfo(node("SG2"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")) sAddrSet(addr("CASG2"))) rootinfo(node("SG3"), addr("CASG3"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CASG3"))) rootinfo(node("SG4"), addr("CASG4"), sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) 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("S"), 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))) sectrace-start(node("C2"), addr("C2a"), addr("Sa")) ipsec-delivered(node("C1"), addr("C1a"), sAttrSet(discard), eSAList, ip(addr("SG2b"), addr("C1a"), rrep(addr("C1a"), addr("Sa"), addr("CASG2"), sAddrSet( addr("CAC1")) sAddrSet(addr("CASG1")) sAddrSet(addr("CASG2")), false))) sectrace-rreq(node("C1"), addr("C1a"), addr("Sa"), sMessageList(rreq(addr("C1a"), addr("Sa"))), eMessageList),'sectrace-rrep-2} {subnet(sAddrSet(addr( "C2a")) sAddrSet(addr("SG1a"))) subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a"))) subnet(sAddrSet(addr("C1a")) sAddrSet(addr("SG2b"))) subnet(sAddrSet(addr("SG2c")) sAddrSet(addr("SG3a"))) subnet(sAddrSet(addr("SG3b")) sAddrSet(addr("SG4a"))) subnet(sAddrSet(addr("SG4b")) sAddrSet(addr("Sa"))) shost(node("C1")) shost(node("C2")) shost(node("S")) shost(node("SG1")) shost(node("SG2")) shost(node("SG3")) shost(node("SG4")) sgw(node("SG1")) sgw(node("SG2")) sgw(node("SG3")) sgw(node("SG4")) sectraced(node("C1")) sectraced(node("C2")) sectraced(node("S")) sectraced(node("SG1")) sectraced(node("SG2")) sectraced(node("SG3")) sectraced(node("SG4")) interfaces(node("C1"), sAddrSet(addr("C1a"))) interfaces(node("C2"), sAddrSet(addr("C2a"))) interfaces(node("S"), sAddrSet(addr("Sa"))) 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"))) 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("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")))) 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")))) sadb(node("C1"), eSASet) sadb(node("C2"), eSASet) sadb(node("S"), eSASet) sadb(node("SG1"), eSASet) sadb(node("SG2"), eSASet) sadb(node("SG3"), eSASet) sadb(node("SG4"), eSASet) rootinfo(node("C1"), addr("CAC1"), sAddrSet(addr("CAC1"))) rootinfo(node("C2"), addr("CAC2"), sAddrSet(addr("CAC2"))) rootinfo(node("S"), addr("CAS"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CAS")) sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) rootinfo(node("SG1"), addr("CASG1"), sAddrSet(addr("CAC2")) sAddrSet(addr("CASG1"))) rootinfo(node("SG2"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")) sAddrSet(addr("CASG2"))) rootinfo(node("SG3"), addr("CASG3"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CASG3"))) rootinfo(node("SG4"), addr("CASG4"), sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) 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("S"), 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))) sectrace-start(node("C2"), addr("C2a"), addr("Sa")) addsp-req(node("C1"), addr("C1a"), addr("SG2b"), addr("C1a"), addr("Sa")) sectrace-rrep2(node("C1"), addr("C1a"), addr("SG2b"), addr("C1a"), addr("Sa"), sMessageList(rreq(addr("C1a"), addr("Sa"))), sMessageList(ip(addr("SG2b"), addr("C1a"), rrep(addr("C1a"), addr("Sa"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")) sAddrSet(addr("CASG2")), false)))), 'addsp-req-responder} {subnet(sAddrSet(addr("C2a")) sAddrSet(addr("SG1a"))) subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a"))) subnet(sAddrSet(addr("C1a")) sAddrSet(addr("SG2b"))) subnet(sAddrSet(addr("SG2c")) sAddrSet(addr("SG3a"))) subnet(sAddrSet(addr("SG3b")) sAddrSet(addr("SG4a"))) subnet(sAddrSet(addr("SG4b")) sAddrSet(addr("Sa"))) shost(node("C1")) shost(node("C2")) shost(node("S")) shost(node("SG1")) shost(node("SG2")) shost(node("SG3")) shost(node("SG4")) sgw(node("SG1")) sgw(node("SG2")) sgw(node("SG3")) sgw(node("SG4")) sectraced(node("C1")) sectraced(node("C2")) sectraced(node("S")) sectraced(node("SG1")) sectraced(node("SG2")) sectraced(node("SG3")) sectraced(node("SG4")) interfaces(node("C1"), sAddrSet(addr("C1a"))) interfaces(node("C2"), sAddrSet(addr("C2a"))) interfaces(node("S"), sAddrSet(addr("Sa"))) 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"))) 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("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")))) 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")))) sadb(node("C1"), eSASet) sadb(node("C2"), eSASet) sadb(node("S"), eSASet) sadb(node("SG1"), eSASet) sadb(node("SG2"), sSASet(sa(addr("C1a"), addr("SG2b"), 0))) sadb(node("SG3"), eSASet) sadb(node("SG4"), eSASet) rootinfo(node("C1"), addr("CAC1"), sAddrSet(addr("CAC1"))) rootinfo(node("C2"), addr("CAC2"), sAddrSet(addr("CAC2"))) rootinfo(node("S"), addr("CAS"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CAS")) sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) rootinfo(node("SG1"), addr("CASG1"), sAddrSet(addr("CAC2")) sAddrSet(addr("CASG1"))) rootinfo(node("SG2"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")) sAddrSet(addr("CASG2"))) rootinfo(node("SG3"), addr("CASG3"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CASG3"))) rootinfo(node("SG4"), addr("CASG4"), sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) 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("S"), eSPList, sSPList(sp(isinitiation, eSAList)) sSPList(sp(isresponse, eSAList))) spdb(node("SG1"), eSPList, sSPList(sp(isinitiation, eSAList)) sSPList(sp(isresponse, eSAList))) spdb(node("SG2"), sSPList(sp(towards(addr("Sa")), sSAList(sa(addr("C1a"), addr("SG2b"), 0)))), 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))) sectrace-start(node("C2"), addr("C2a"), addr("Sa")) addsp-req'(node("C1"), addr("C1a"), addr("SG2b"), addr("C1a"), addr("Sa")) sectrace-rrep2(node("C1"), addr("C1a"), addr("SG2b"), addr("C1a"), addr("Sa"), sMessageList(rreq(addr("C1a"), addr("Sa"))), sMessageList(ip(addr("SG2b"), addr("C1a"), rrep(addr("C1a"), addr("Sa"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")) sAddrSet(addr("CASG2")), false)))), 'addsp-req-inititator} {subnet(sAddrSet(addr("C2a")) sAddrSet(addr("SG1a"))) subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a"))) subnet(sAddrSet(addr("C1a")) sAddrSet(addr("SG2b"))) subnet(sAddrSet(addr("SG2c")) sAddrSet(addr("SG3a"))) subnet(sAddrSet(addr("SG3b")) sAddrSet(addr("SG4a"))) subnet(sAddrSet(addr("SG4b")) sAddrSet(addr("Sa"))) shost(node("C1")) shost(node("C2")) shost(node("S")) shost(node("SG1")) shost(node("SG2")) shost(node("SG3")) shost(node("SG4")) sgw(node("SG1")) sgw(node("SG2")) sgw(node("SG3")) sgw(node("SG4")) sectraced(node("C1")) sectraced(node("C2")) sectraced(node("S")) sectraced(node("SG1")) sectraced(node("SG2")) sectraced(node("SG3")) sectraced(node("SG4")) interfaces(node("C1"), sAddrSet(addr("C1a"))) interfaces(node("C2"), sAddrSet(addr("C2a"))) interfaces(node("S"), sAddrSet(addr("Sa"))) 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"))) 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("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")))) 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")))) sadb(node("C1"), sSASet(sa(addr("C1a"), addr("SG2b"), 0))) sadb(node("C2"), eSASet) sadb(node("S"), eSASet) sadb(node("SG1"), eSASet) sadb(node("SG2"), sSASet(sa(addr("C1a"), addr("SG2b"), 0))) sadb(node("SG3"), eSASet) sadb(node("SG4"), eSASet) rootinfo(node("C1"), addr("CAC1"), sAddrSet(addr("CAC1"))) rootinfo(node("C2"), addr("CAC2"), sAddrSet(addr("CAC2"))) rootinfo(node("S"), addr("CAS"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CAS")) sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) rootinfo(node("SG1"), addr("CASG1"), sAddrSet(addr("CAC2")) sAddrSet(addr("CASG1"))) rootinfo(node("SG2"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")) sAddrSet(addr("CASG2"))) rootinfo(node("SG3"), addr("CASG3"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CASG3"))) rootinfo(node("SG4"), addr("CASG4"), sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) spdb(node("C1"), eSPList, sSPList(sp(towards(addr("Sa")), sSAList(sa(addr("C1a"), addr("SG2b"), 0)))) sSPList(sp(isinitiation, eSAList)) sSPList(sp( isresponse, eSAList))) spdb(node("C2"), eSPList, sSPList(sp(isinitiation, eSAList)) sSPList(sp(isresponse, eSAList))) spdb(node("S"), eSPList, sSPList(sp(isinitiation, eSAList)) sSPList(sp(isresponse, eSAList))) spdb(node("SG1"), eSPList, sSPList(sp(isinitiation, eSAList)) sSPList(sp(isresponse, eSAList))) spdb(node("SG2"), sSPList(sp(towards(addr("Sa")), sSAList(sa(addr("C1a"), addr("SG2b"), 0)))), 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))) sectrace-start(node("C2"), addr("C2a"), addr("Sa")) addsp-ack(node("C1"), addr("C1a"), addr("SG2b"), addr("C1a"), addr("Sa")) sectrace-rrep2(node("C1"), addr("C1a"), addr("SG2b"), addr("C1a"), addr("Sa"), sMessageList(rreq(addr("C1a"), addr("Sa"))), sMessageList(ip(addr("SG2b"), addr("C1a"), rrep(addr("C1a"), addr("Sa"), addr("CASG2"), sAddrSet(addr("CAC1")) sAddrSet(addr("CASG1")) sAddrSet(addr("CASG2")), false)))), 'sectrace-rrep-2'} {subnet(sAddrSet(addr("C2a")) sAddrSet(addr("SG1a"))) subnet(sAddrSet(addr("SG1b")) sAddrSet(addr("SG2a"))) subnet(sAddrSet(addr("C1a")) sAddrSet(addr("SG2b"))) subnet(sAddrSet(addr("SG2c")) sAddrSet(addr("SG3a"))) subnet(sAddrSet(addr("SG3b")) sAddrSet(addr("SG4a"))) subnet(sAddrSet(addr("SG4b")) sAddrSet(addr("Sa"))) shost(node("C1")) shost(node("C2")) shost(node("S")) shost(node("SG1")) shost(node("SG2")) shost(node("SG3")) shost(node("SG4")) sgw(node("SG1")) sgw(node("SG2")) sgw(node("SG3")) sgw(node("SG4")) sectraced(node("C1")) sectraced(node("C2")) sectraced(node("S")) sectraced(node("SG1")) sectraced(node("SG2")) sectraced(node("SG3")) sectraced(node("SG4")) interfaces(node("C1"), sAddrSet(addr("C1a"))) interfaces(node("C2"), sAddrSet(addr("C2a"))) interfaces(node("S"), sAddrSet(addr("Sa"))) 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"))) ipsec-send(node("C1"), ip(addr("C1a"), addr("Sa"), rreq(addr("C1a"), 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("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")))) 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")))) sadb(node("C1"), sSASet(sa(addr("C1a"), addr("SG2b"), 0))) sadb(node("C2"), eSASet) sadb(node("S"), eSASet) sadb(node("SG1"), eSASet) sadb(node("SG2"), sSASet(sa(addr("C1a"), addr("SG2b"), 0))) sadb(node("SG3"), eSASet) sadb(node("SG4"), eSASet) rootinfo(node("C1"), addr("CAC1"), sAddrSet(addr("CAC1"))) rootinfo(node("C2"), addr("CAC2"), sAddrSet(addr("CAC2"))) rootinfo(node("S"), addr("CAS"), sAddrSet(addr("CAC1")) sAddrSet(addr("CAC2")) sAddrSet(addr("CAS")) sAddrSet(addr("CASG3")) sAddrSet(addr("CASG4"))) rootinfo(node("SG1"), addr("CASG1"), sAddrSet(addr("CAC2")) sAddrSet(addr("CASG1"))) rootinfo(node("SG2"), addr("CASG2"), sAddrSet(addr(