Solution 1 (state 56785)
states: 56786  rewrites: 16092423 in 56410ms cpu (62010ms real) (285276
    rewrites/second)
state:State --> subnet(sAddrSet(addr("C'a")) sAddrSet(addr("NASc")))
subnet(sAddrSet(addr("Ca")) sAddrSet(addr("NASa")))
subnet(sAddrSet(addr("NASb")) sAddrSet(addr("Sa")))
subnet(sAddrSet(addr("NASd")) sAddrSet(addr("S'a")))
shost(node("C"))
shost(node("C'"))
shost(node("NAS"))
shost(node("S"))
shost(node("S'"))
sgw(node("NAS"))
fresh(12)
siked-start(node("C"))
siked-start(node("C'"))
siked-start(node("NAS"))
siked-start(node("S"))
siked-start(node("S'"))
l3a-server-start(node("S'"))
interfaces(node("C"), sAddrSet(addr("Ca")))
interfaces(node("C'"), sAddrSet(addr("C'a")))
interfaces(node("NAS"), sAddrSet(addr("NASa")) sAddrSet(addr("NASb")) sAddrSet(
    addr("NASc")) sAddrSet(addr("NASd")))
interfaces(node("S"), sAddrSet(addr("Sa")))
interfaces(node("S'"), sAddrSet(addr("S'a")))
routetab(node("C"), sRouteList(route(addr("Ca"), addr("Ca"), addr("Ca")))
    sRouteList(route(addr("C'a"), addr("Ca"), addr("NASa"))) sRouteList(route(
    addr("NASa"), addr("Ca"), addr("NASa"))) sRouteList(route(addr("NASb"),
    addr("Ca"), addr("NASa"))) sRouteList(route(addr("NASc"), addr("Ca"), addr(
    "NASa"))) sRouteList(route(addr("NASd"), addr("Ca"), addr("NASa")))
    sRouteList(route(addr("Sa"), addr("Ca"), addr("NASa"))) sRouteList(route(
    addr("S'a"), addr("Ca"), addr("NASa"))))
routetab(node("C'"), sRouteList(route(addr("C'a"), addr("C'a"), addr("C'a")))
    sRouteList(route(addr("Ca"), addr("C'a"), addr("NASc"))) sRouteList(route(
    addr("NASa"), addr("C'a"), addr("NASc"))) sRouteList(route(addr("NASb"),
    addr("C'a"), addr("NASc"))) sRouteList(route(addr("NASc"), addr("C'a"),
    addr("NASc"))) sRouteList(route(addr("NASd"), addr("C'a"), addr("NASc")))
    sRouteList(route(addr("Sa"), addr("C'a"), addr("NASc"))) sRouteList(route(
    addr("S'a"), addr("C'a"), addr("NASc"))))
routetab(node("NAS"), sRouteList(route(addr("NASa"), addr("NASa"), addr(
    "NASa"))) sRouteList(route(addr("NASb"), addr("NASb"), addr("NASb")))
    sRouteList(route(addr("NASc"), addr("NASc"), addr("NASc"))) sRouteList(
    route(addr("NASd"), addr("NASd"), addr("NASd"))) sRouteList(route(addr(
    "Ca"), addr("NASa"), addr("Ca"))) sRouteList(route(addr("C'a"), addr(
    "NASc"), addr("C'a"))) sRouteList(route(addr("Sa"), addr("NASb"), addr(
    "Sa"))) sRouteList(route(addr("S'a"), addr("NASd"), addr("S'a"))))
routetab(node("S"), sRouteList(route(addr("Sa"), addr("Sa"), addr("Sa")))
    sRouteList(route(addr("S'a"), addr("Sa"), addr("NASb"))) sRouteList(route(
    addr("Ca"), addr("Sa"), addr("NASb"))) sRouteList(route(addr("C'a"), addr(
    "Sa"), addr("NASb"))) sRouteList(route(addr("NASb"), addr("Sa"), addr(
    "NASb"))) sRouteList(route(addr("NASa"), addr("Sa"), addr("NASb")))
    sRouteList(route(addr("NASc"), addr("Sa"), addr("NASb"))) sRouteList(route(
    addr("NASd"), addr("Sa"), addr("NASb"))))
routetab(node("S'"), sRouteList(route(addr("S'a"), addr("S'a"), addr("S'a")))
    sRouteList(route(addr("Sa"), addr("S'a"), addr("NASd"))) sRouteList(route(
    addr("Ca"), addr("S'a"), addr("NASd"))) sRouteList(route(addr("C'a"), addr(
    "S'a"), addr("NASd"))) sRouteList(route(addr("NASd"), addr("S'a"), addr(
    "NASd"))) sRouteList(route(addr("NASa"), addr("S'a"), addr("NASd")))
    sRouteList(route(addr("NASb"), addr("S'a"), addr("NASd"))) sRouteList(
    route(addr("NASc"), addr("S'a"), addr("NASd"))))
sadb(node("C"), sSASet(sa(addr("Ca"), addr("NASa"), 0)) sSASet(sa(addr("Ca"),
    addr("Sa"), 1)) sSASet(sa(addr("NASa"), addr("Ca"), 0)) sSASet(sa(addr(
    "Sa"), addr("Ca"), 1)))
sadb(node("C'"), eSASet)
sadb(node("NAS"), sSASet(sa(addr("Ca"), addr("NASa"), 0)) sSASet(sa(addr(
    "NASa"), addr("Ca"), 0)) sSASet(sa(addr("NASa"), addr("Sa"), 0)) sSASet(sa(
    addr("Sa"), addr("NASa"), 1)))
sadb(node("S"), sSASet(sa(addr("Ca"), addr("Sa"), 1)) sSASet(sa(addr("NASa"),
    addr("Sa"), 0)) sSASet(sa(addr("Sa"), addr("Ca"), 1)) sSASet(sa(addr("Sa"),
    addr("NASa"), 1)))
sadb(node("S'"), eSASet)
fresh-spi(node("C"), 2)
fresh-spi(node("C'"), 0)
fresh-spi(node("NAS"), 2)
fresh-spi(node("S"), 2)
fresh-spi(node("S'"), 0)
l3a-client-start(node("C'"), addr("C'a"))
spdb(node("C"), sSPList(sp(src-dest-pattern(addr("Sa"), addr("Ca")), sSAList(
    sa(addr("Sa"), addr("Ca"), 1)))) sSPList(sp(src-dest-pattern(addr("NASa"),
    addr("Ca")), sSAList(sa(addr("NASa"), addr("Ca"), 0)))) sSPList(sp(
    any-pattern, eSAList)), sSPList(sp(src-dest-pattern(addr("Ca"), addr(
    "Sa")), sSAList(sa(addr("Ca"), addr("Sa"), 1)) sSAList(sa(addr("Ca"), addr(
    "NASa"), 0)))) sSPList(sp(src-dest-pattern(addr("Ca"), addr("NASa")),
    sSAList(sa(addr("Ca"), addr("NASa"), 0)))) sSPList(sp(any-pattern,
    eSAList)))
spdb(node("C'"), sSPList(sp(any-pattern, eSAList)), sSPList(sp(any-pattern,
    eSAList)))
spdb(node("NAS"), sSPList(sp(src-dest-pattern(addr("Sa"), addr("Ca")), sSAList(
    sa(addr("Sa"), addr("NASa"), 1)))) sSPList(sp(src-dest-pattern(addr("Sa"),
    addr("NASa")), sSAList(sa(addr("Sa"), addr("NASa"), 1)))) sSPList(sp(
    src-dest-pattern(addr("Ca"), addr("Sa")), sSAList(sa(addr("Ca"), addr(
    "NASa"), 0)))) sSPList(sp(src-dest-pattern(addr("Ca"), addr("NASa")),
    sSAList(sa(addr("Ca"), addr("NASa"), 0)))) sSPList(sp(any-pattern,
    eSAList)), sSPList(sp(src-dest-pattern(addr("NASa"), addr("Sa")), sSAList(
    sa(addr("NASa"), addr("Sa"), 0)))) sSPList(sp(src-dest-pattern(addr(
    "NASa"), addr("Ca")), sSAList(sa(addr("NASa"), addr("Ca"), 0)))) sSPList(
    sp(any-pattern, eSAList)))
spdb(node("S"), sSPList(sp(src-dest-pattern(addr("Ca"), addr("Sa")), sSAList(
    sa(addr("Ca"), addr("Sa"), 1)))) sSPList(sp(src-dest-pattern(addr("NASa"),
    addr("Sa")), sSAList(sa(addr("NASa"), addr("Sa"), 0)))) sSPList(sp(
    any-pattern, eSAList)), sSPList(sp(src-dest-pattern(addr("Sa"), addr(
    "Ca")), sSAList(sa(addr("Sa"), addr("Ca"), 1)) sSAList(sa(addr("Sa"), addr(
    "NASa"), 1)))) sSPList(sp(src-dest-pattern(addr("Sa"), addr("NASa")),
    sSAList(sa(addr("Sa"), addr("NASa"), 1)))) sSPList(sp(any-pattern,
    eSAList)))
spdb(node("S'"), sSPList(sp(any-pattern, eSAList)), sSPList(sp(any-pattern,
    eSAList)))
pki-info(node("C"), seckey("SecretKeyOfC"), pubkey("PublicKeyOfC"), cert(addr(
    "Ca"), pubkey("PublicKeyOfC")))
pki-info(node("C'"), seckey("SecretKeyOfC'"), pubkey("PublicKeyOfC'"), cert(
    addr("C'a"), pubkey("PublicKeyOfC'")))
pki-info(node("S"), seckey("SecretKeyOfS"), pubkey("PublicKeyOfS"), cert(addr(
    "Sa"), pubkey("PublicKeyOfS")))
pki-info(node("S'"), seckey("SecretKeyOfS'"), pubkey("PublicKeyOfS'"), cert(
    addr("S'a"), pubkey("PublicKeyOfS'")))
l3a-client-app-terminated(node("C"), addr("Ca"), addr("Sa"), addr("NASa"))
l3a-client-terminated(node("C"), addr("Ca"), addr("NASa"), addr("Sa"), spi(0,
    0), spi(1, 1))
l3a-nas-terminated(node("NAS"), addr("Ca"), addr("NASa"), addr("Sa"), cert(
    addr("Ca"), pubkey("PublicKeyOfC")), sign(seckey("SecretKeyOfC"), reqdata(
    Timelive, addr("NASa"))), spi(0, 0), spi(1, 0))
l3a-server-terminated(node("S"), addr("Ca"), addr("NASa"), addr("Sa"), sign(
    seckey("SecretKeyOfC"), reqdata(Timelive, addr("NASa"))), cert(addr("Ca"),
    pubkey("PublicKeyOfC")), spi(1, 0), spi(1, 1))
sike-term(node("C"), addr("Ca"), addr("NASa"), cert(addr("Ca"), pubkey(
    "PublicKeyOfC")), seckey("SecretKeyOfC"), random(0), random(2), cert(addr(
    "NASa"), pubkey("PublicKeyOfNAS")), cookie(versec, hash(random(1),
    cookiedat(random(0), random(2), addr("Ca")))), spi(0, 0), sharedkey(random(
    3)))
sike-term(node("NAS"), addr("NASa"), addr("Sa"), cert(addr("NASa"), pubkey(
    "PublicKeyOfNAS")), seckey("SecretKeyOfNAS"), random(4), random(6), cert(
    addr("Sa"), pubkey("PublicKeyOfS")), cookie(versec, hash(random(5),
    cookiedat(random(4), random(6), addr("NASa")))), spi(1, 0), sharedkey(
    random(7)))
sike-term(node("S"), addr("Sa"), addr("Ca"), cert(addr("Sa"), pubkey(
    "PublicKeyOfS")), seckey("SecretKeyOfS"), random(8), random(10), cert(addr(
    "Ca"), pubkey("PublicKeyOfC")), cookie(versec, hash(random(9), cookiedat(
    random(8), random(10), addr("Sa")))), spi(1, 1), sharedkey(random(11)))
siked-term(node("C"), addr("Ca"), cert(addr("Ca"), pubkey("PublicKeyOfC")),
    seckey("SecretKeyOfC"), random(9), random(8), addr("Sa"), random(10), cert(
    addr("Sa"), pubkey("PublicKeyOfS")), spi(1, 1), sharedkey(random(11)))
siked-term(node("NAS"), addr("NASa"), cert(addr("NASa"), pubkey(
    "PublicKeyOfNAS")), seckey("SecretKeyOfNAS"), random(1), random(0), addr(
    "Ca"), random(2), cert(addr("Ca"), pubkey("PublicKeyOfC")), spi(0, 0),
    sharedkey(random(3)))
siked-term(node("S"), addr("Sa"), cert(addr("Sa"), pubkey("PublicKeyOfS")),
    seckey("SecretKeyOfS"), random(5), random(4), addr("NASa"), random(6),
    cert(addr("NASa"), pubkey("PublicKeyOfNAS")), spi(1, 0), sharedkey(random(
    7)))