Maude> search initial =>! state:State .
search in L3A-TEST : initial =>! state:State .

Solution 1 (state 76010)
states: 76974  rewrites: 25691586 in 29590ms cpu (106988ms real) (868252
    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(9)
siked-start(node("C"))
siked-start(node("C'"))
siked-start(node("NAS"))
siked-start(node("S"))
siked-start(node("S'"))
DEBUG1(node("C"))
DEBUG1(node("NAS"))
DEBUG2(node("C"))
DEBUG2(node("NAS"))
DEBUG3(node("NAS"))
DEBUG3(node("S"))
DEBUG4(node("NAS"))
DEBUG4(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("NASa"), addr("NASb"), 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"))))
ipsec-send-ack(sike(node("S")), node("S"))
sadb(node("C"), sSASet(sa(addr("Ca"), addr("NASa"), 0)))
sadb(node("C'"), eSASet)
sadb(node("NAS"), sSASet(sa(addr("Ca"), addr("NASa"), 0)) sSASet(sa(addr("Sa"),
    addr("NASa"), 1)))
sadb(node("S"), sSASet(sa(addr("Sa"), addr("NASa"), 1)))
sadb(node("S'"), eSASet)
fresh-spi(node("C"), 1)
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(any-pattern, eSAList)), 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)))
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(any-pattern, eSAList)))
spdb(node("S"), sSPList(sp(any-pattern, eSAList)), 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(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-waiting1(node("C"), addr("Ca"), addr("Sa"), addr("NASa"))
ipsec-delivered(node("NAS"), addr("NASb"), sAttrSet(discard), sSAList(sa(addr(
    "Sa"), addr("NASa"), 1)), ip(addr("Sa"), addr("Ca"), msg1(random(8), spi(1,
    0))))
l3a-client-expect-sike-notify(node("C"), addr("Ca"), addr("NASa"), addr("Sa"),
    spi(0, 0))
l3a-server-expect-sike-ack(node("S"), addr("Ca"), addr("NASa"), addr("Sa"),
    sign(seckey("SecretKeyOfC"), reqdata(Timelive, addr("NASa"))), cert(addr(
    "Ca"), pubkey("PublicKeyOfC")), spi(1, 0))
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))
sike-waiting(node("S"), addr("Sa"), addr("Ca"), cert(addr("Sa"), pubkey(
    "PublicKeyOfS")), seckey("SecretKeyOfS"), sadir(addr("Sa"), addr("Ca")),
    null-payload, random(8), spi(1, 0))
sike-term(node("C"), addr("Ca"), addr("NASa"), cert(addr("Ca"), pubkey(
    "PublicKeyOfC")), seckey("SecretKeyOfC"), sadir(addr("Ca"), addr("NASa")),
    nsinit(cert(addr("Ca"), pubkey("PublicKeyOfC")), sign(seckey(
    "SecretKeyOfC"), reqdata(Timelive, addr("NASa"))), addr("Sa")), 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"), sadir(addr("Sa"), addr(
    "NASa")), nsinit(cert(addr("Ca"), pubkey("PublicKeyOfC")), sign(seckey(
    "SecretKeyOfC"), reqdata(Timelive, addr("NASa")))), 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)))
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),
    sadir(addr("Ca"), addr("NASa")), nsinit(cert(addr("Ca"), pubkey(
    "PublicKeyOfC")), sign(seckey("SecretKeyOfC"), reqdata(Timelive, addr(
    "NASa"))), addr("Sa")), 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), sadir(addr("Sa"),
    addr("NASa")), nsinit(cert(addr("Ca"), pubkey("PublicKeyOfC")), sign(
    seckey("SecretKeyOfC"), reqdata(Timelive, addr("NASa")))), sharedkey(
    random(7)))

Solution 2 (state 79568)
states: 80119  rewrites: 26969368 in 31750ms cpu (115342ms real) (849428
    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(9)
siked-start(node("C"))
siked-start(node("C'"))
siked-start(node("NAS"))
siked-start(node("S"))
siked-start(node("S'"))
DEBUG1(node("C"))
DEBUG1(node("NAS"))
DEBUG2(node("C"))
DEBUG2(node("NAS"))
DEBUG3(node("NAS"))
DEBUG3(node("S"))
DEBUG4(node("NAS"))
DEBUG4(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("NASa"), addr("NASb"), 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"))))
ipsec-send-ack(sike(node("S")), node("S"))
sadb(node("C"), sSASet(sa(addr("Ca"), addr("NASa"), 0)))
sadb(node("C'"), eSASet)
sadb(node("NAS"), sSASet(sa(addr("Ca"), addr("NASa"), 0)) sSASet(sa(addr("Sa"),
    addr("NASa"), 1)))
sadb(node("S"), sSASet(sa(addr("Sa"), addr("NASa"), 1)))
sadb(node("S'"), eSASet)
fresh-spi(node("C"), 1)
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(any-pattern, eSAList)), 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)))
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(any-pattern, eSAList)))
spdb(node("S"), sSPList(sp(any-pattern, eSAList)), 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(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-waiting1(node("C"), addr("Ca"), addr("Sa"), addr("NASa"))
ipsec-delivered(node("NAS"), addr("NASa"), eAttrSet, eSAList, ip(addr("Sa"),
    addr("NASa"), sec(1, ip(addr("Sa"), addr("Ca"), msg1(random(8), spi(1,
    0))))))
l3a-client-expect-sike-notify(node("C"), addr("Ca"), addr("NASa"), addr("Sa"),
    spi(0, 0))
l3a-server-expect-sike-ack(node("S"), addr("Ca"), addr("NASa"), addr("Sa"),
    sign(seckey("SecretKeyOfC"), reqdata(Timelive, addr("NASa"))), cert(addr(
    "Ca"), pubkey("PublicKeyOfC")), spi(1, 0))
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))
sike-waiting(node("S"), addr("Sa"), addr("Ca"), cert(addr("Sa"), pubkey(
    "PublicKeyOfS")), seckey("SecretKeyOfS"), sadir(addr("Sa"), addr("Ca")),
    null-payload, random(8), spi(1, 0))
sike-term(node("C"), addr("Ca"), addr("NASa"), cert(addr("Ca"), pubkey(
    "PublicKeyOfC")), seckey("SecretKeyOfC"), sadir(addr("Ca"), addr("NASa")),
    nsinit(cert(addr("Ca"), pubkey("PublicKeyOfC")), sign(seckey(
    "SecretKeyOfC"), reqdata(Timelive, addr("NASa"))), addr("Sa")), 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"), sadir(addr("Sa"), addr(
    "NASa")), nsinit(cert(addr("Ca"), pubkey("PublicKeyOfC")), sign(seckey(
    "SecretKeyOfC"), reqdata(Timelive, addr("NASa")))), 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)))
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),
    sadir(addr("Ca"), addr("NASa")), nsinit(cert(addr("Ca"), pubkey(
    "PublicKeyOfC")), sign(seckey("SecretKeyOfC"), reqdata(Timelive, addr(
    "NASa"))), addr("Sa")), 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), sadir(addr("Sa"),
    addr("NASa")), nsinit(cert(addr("Ca"), pubkey("PublicKeyOfC")), sign(
    seckey("SecretKeyOfC"), reqdata(Timelive, addr("NASa")))), sharedkey(
    random(7)))

Solution 3 (state 80119)
states: 80691  rewrites: 27258753 in 32230ms cpu (116246ms real) (845757
    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(9)
siked-start(node("C"))
siked-start(node("C'"))
siked-start(node("NAS"))
siked-start(node("S"))
siked-start(node("S'"))
DEBUG1(node("C"))
DEBUG1(node("NAS"))
DEBUG2(node("C"))
DEBUG2(node("NAS"))
DEBUG3(node("NAS"))
DEBUG3(node("S"))
DEBUG4(node("NAS"))
DEBUG4(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("NASa"), addr("NASb"), 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"))))
ipsec-send-ack(sike(node("S")), node("S"))
sadb(node("C"), sSASet(sa(addr("Ca"), addr("NASa"), 0)))
sadb(node("C'"), eSASet)
sadb(node("NAS"), sSASet(sa(addr("Ca"), addr("NASa"), 0)) sSASet(sa(addr("Sa"),
    addr("NASa"), 1)))
sadb(node("S"), sSASet(sa(addr("Sa"), addr("NASa"), 1)))
sadb(node("S'"), eSASet)
fresh-spi(node("C"), 1)
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(any-pattern, eSAList)), 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)))
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(any-pattern, eSAList)))
spdb(node("S"), sSPList(sp(any-pattern, eSAList)), 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(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-waiting1(node("C"), addr("Ca"), addr("Sa"), addr("NASa"))
ipsec-delivered(node("NAS"), addr("NASa"), sAttrSet(discard), sSAList(sa(addr(
    "Sa"), addr("NASa"), 1)), ip(addr("Sa"), addr("Ca"), msg1(random(8), spi(1,
    0))))
l3a-client-expect-sike-notify(node("C"), addr("Ca"), addr("NASa"), addr("Sa"),
    spi(0, 0))
l3a-server-expect-sike-ack(node("S"), addr("Ca"), addr("NASa"), addr("Sa"),
    sign(seckey("SecretKeyOfC"), reqdata(Timelive, addr("NASa"))), cert(addr(
    "Ca"), pubkey("PublicKeyOfC")), spi(1, 0))
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))
sike-waiting(node("S"), addr("Sa"), addr("Ca"), cert(addr("Sa"), pubkey(
    "PublicKeyOfS")), seckey("SecretKeyOfS"), sadir(addr("Sa"), addr("Ca")),
    null-payload, random(8), spi(1, 0))
sike-term(node("C"), addr("Ca"), addr("NASa"), cert(addr("Ca"), pubkey(
    "PublicKeyOfC")), seckey("SecretKeyOfC"), sadir(addr("Ca"), addr("NASa")),
    nsinit(cert(addr("Ca"), pubkey("PublicKeyOfC")), sign(seckey(
    "SecretKeyOfC"), reqdata(Timelive, addr("NASa"))), addr("Sa")), 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"), sadir(addr("Sa"), addr(
    "NASa")), nsinit(cert(addr("Ca"), pubkey("PublicKeyOfC")), sign(seckey(
    "SecretKeyOfC"), reqdata(Timelive, addr("NASa")))), 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)))
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),
    sadir(addr("Ca"), addr("NASa")), nsinit(cert(addr("Ca"), pubkey(
    "PublicKeyOfC")), sign(seckey("SecretKeyOfC"), reqdata(Timelive, addr(
    "NASa"))), addr("Sa")), 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), sadir(addr("Sa"),
    addr("NASa")), nsinit(cert(addr("Ca"), pubkey("PublicKeyOfC")), sign(
    seckey("SecretKeyOfC"), reqdata(Timelive, addr("NASa")))), sharedkey(
    random(7)))

Solution 4 (state 214211)
states: 214212  rewrites: 74327574 in 149470ms cpu (591604ms real) (497274
    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(16)
siked-start(node("C"))
siked-start(node("C'"))
siked-start(node("NAS"))
siked-start(node("S"))
siked-start(node("S'"))
DEBUG1(node("C"))
DEBUG1(node("C"))
DEBUG1(node("NAS"))
DEBUG1(node("S"))
DEBUG2(node("C"))
DEBUG2(node("C"))
DEBUG2(node("NAS"))
DEBUG2(node("S"))
DEBUG3(node("C"))
DEBUG3(node("NAS"))
DEBUG3(node("S"))
DEBUG3(node("S"))
DEBUG4(node("C"))
DEBUG4(node("NAS"))
DEBUG4(node("S"))
DEBUG4(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("NASa"), addr("NASb"), 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"), 2)) sSASet(sa(addr("Sa"), addr("Ca"), 1)))
sadb(node("C'"), eSASet)
sadb(node("NAS"), sSASet(sa(addr("Ca"), addr("NASa"), 0)) sSASet(sa(addr("Sa"),
    addr("NASa"), 1)))
sadb(node("S"), sSASet(sa(addr("Ca"), addr("Sa"), 2)) sSASet(sa(addr("Sa"),
    addr("Ca"), 1)) sSASet(sa(addr("Sa"), addr("NASa"), 1)))
sadb(node("S'"), eSASet)
fresh-spi(node("C"), 3)
fresh-spi(node("C'"), 0)
fresh-spi(node("NAS"), 2)
fresh-spi(node("S"), 3)
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(any-pattern, eSAList)),
    sSPList(sp(src-dest-pattern(addr("Ca"), addr("Sa")), sSAList(sa(addr("Ca"),
    addr("Sa"), 2)) 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(any-pattern, eSAList)))
spdb(node("S"), sSPList(sp(src-dest-pattern(addr("Ca"), addr("Sa")), sSAList(
    sa(addr("Ca"), addr("Sa"), 2)))) 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), spi(2, 2))
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), spi(2, 2))
sike-term(node("C"), addr("Ca"), addr("NASa"), cert(addr("Ca"), pubkey(
    "PublicKeyOfC")), seckey("SecretKeyOfC"), sadir(addr("Ca"), addr("NASa")),
    nsinit(cert(addr("Ca"), pubkey("PublicKeyOfC")), sign(seckey(
    "SecretKeyOfC"), reqdata(Timelive, addr("NASa"))), addr("Sa")), 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("C"), addr("Ca"), addr("Sa"), cert(addr("Ca"), pubkey(
    "PublicKeyOfC")), seckey("SecretKeyOfC"), sadir(addr("Ca"), addr("Sa")),
    null-payload, random(12), random(14), cert(addr("Sa"), pubkey(
    "PublicKeyOfS")), cookie(versec, hash(random(13), cookiedat(random(12),
    random(14), addr("Ca")))), spi(2, 2), sharedkey(random(15)))
sike-term(node("NAS"), addr("NASa"), addr("Sa"), cert(addr("NASa"), pubkey(
    "PublicKeyOfNAS")), seckey("SecretKeyOfNAS"), sadir(addr("Sa"), addr(
    "NASa")), nsinit(cert(addr("Ca"), pubkey("PublicKeyOfC")), sign(seckey(
    "SecretKeyOfC"), reqdata(Timelive, addr("NASa")))), 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"), sadir(addr("Sa"), addr("Ca")),
    null-payload, 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), sadir(addr("Sa"), addr(
    "Ca")), null-payload, 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),
    sadir(addr("Ca"), addr("NASa")), nsinit(cert(addr("Ca"), pubkey(
    "PublicKeyOfC")), sign(seckey("SecretKeyOfC"), reqdata(Timelive, addr(
    "NASa"))), addr("Sa")), 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), sadir(addr("Sa"),
    addr("NASa")), nsinit(cert(addr("Ca"), pubkey("PublicKeyOfC")), sign(
    seckey("SecretKeyOfC"), reqdata(Timelive, addr("NASa")))), sharedkey(
    random(7)))
siked-term(node("S"), addr("Sa"), cert(addr("Sa"), pubkey("PublicKeyOfS")),
    seckey("SecretKeyOfS"), random(13), random(12), addr("Ca"), random(14),
    cert(addr("Ca"), pubkey("PublicKeyOfC")), spi(2, 2), sadir(addr("Ca"),
    addr("Sa")), null-payload, sharedkey(random(15)))

No more solutions.
states: 214212  rewrites: 74327574 in 149500ms cpu (591816ms real) (497174
    rewrites/second)
Maude>