Solution 1 (state 18036) states: 18184 rewrites: 5164293 in 13930ms cpu (14240ms real) (370731 rewrites/second) state:State --> subnet(sAddrSet(addr("Ca")) sAddrSet(addr("NASa"))) subnet(sAddrSet(addr("NASb")) sAddrSet(addr("Sa"))) 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'")) l3a-server-start(node("S'")) interfaces(node("C"), sAddrSet(addr("Ca"))) interfaces(node("NAS"), sAddrSet(addr("NASa")) sAddrSet(addr("NASb"))) interfaces(node("S"), sAddrSet(addr("Sa"))) routetab(node("C"), sRouteList(route(addr("Ca"), addr("Ca"), addr("Ca"))) sRouteList(route(addr("NASa"), addr("Ca"), addr("NASa"))) sRouteList(route( addr("NASb"), addr("Ca"), addr("NASa"))) sRouteList(route(addr("Sa"), addr( "Ca"), addr("NASa")))) routetab(node("NAS"), sRouteList(route(addr("NASa"), addr("NASa"), addr( "NASa"))) sRouteList(route(addr("NASb"), addr("NASb"), addr("NASb"))) sRouteList(route(addr("Ca"), addr("NASa"), addr("Ca"))) sRouteList(route( addr("Sa"), addr("NASb"), addr("Sa")))) routetab(node("S"), sRouteList(route(addr("Sa"), addr("Sa"), addr("Sa"))) sRouteList(route(addr("Ca"), addr("Sa"), addr("NASb"))) sRouteList(route( addr("NASb"), addr("Sa"), addr("NASb"))) sRouteList(route(addr("NASa"), addr("Sa"), addr("NASb")))) sadb(node("C"), sSASet(sa(addr("Ca"), addr("NASa"), 0))) sadb(node("C'"), eSASet) sadb(node("NAS"), sSASet(sa(addr("Ca"), addr("NASa"), 0))) 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("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)))))) ipsec-delivered(node("NAS"), addr("NASa"), eAttrSet, eSAList, ip(addr("Sa"), addr("NASa"), sec(1, ip(addr("Sa"), addr("NASa"), msg4(sign(seckey( "SecretKeyOfS"), msg4data(random(6), addr("NASa"), random(4), spi(1, 0), encrypt(pubkey("PublicKeyOfNAS"), sharedkey(random(7)))))))))) l3a-client-expect-sike-notify(node("C"), addr("Ca"), addr("NASa"), addr("Sa"), spi(0, 0)) l3a-nas-waiting(node("NAS"), addr("Ca"), addr("NASa"), addr("Sa"), cert(addr( "Ca"), pubkey("PublicKeyOfC")), sign(seckey("SecretKeyOfC"), reqdata( Timelive, addr("NASa"))), 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)) 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-waiting-2(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), spi( 1, 0), random(6), cert(addr("Sa"), pubkey("PublicKeyOfS")), cookie(versec, hash(random(5), cookiedat(random(4), random(6), addr("NASa"))))) 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))) 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 18613) states: 18663 rewrites: 5260346 in 14320ms cpu (14680ms real) (367342 rewrites/second) state:State --> subnet(sAddrSet(addr("Ca")) sAddrSet(addr("NASa"))) subnet(sAddrSet(addr("NASb")) sAddrSet(addr("Sa"))) 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'")) l3a-server-start(node("S'")) interfaces(node("C"), sAddrSet(addr("Ca"))) interfaces(node("NAS"), sAddrSet(addr("NASa")) sAddrSet(addr("NASb"))) interfaces(node("S"), sAddrSet(addr("Sa"))) routetab(node("C"), sRouteList(route(addr("Ca"), addr("Ca"), addr("Ca"))) sRouteList(route(addr("NASa"), addr("Ca"), addr("NASa"))) sRouteList(route( addr("NASb"), addr("Ca"), addr("NASa"))) sRouteList(route(addr("Sa"), addr( "Ca"), addr("NASa")))) routetab(node("NAS"), sRouteList(route(addr("NASa"), addr("NASa"), addr( "NASa"))) sRouteList(route(addr("NASb"), addr("NASb"), addr("NASb"))) sRouteList(route(addr("Ca"), addr("NASa"), addr("Ca"))) sRouteList(route( addr("Sa"), addr("NASb"), addr("Sa")))) routetab(node("S"), sRouteList(route(addr("Sa"), addr("Sa"), addr("Sa"))) sRouteList(route(addr("Ca"), addr("Sa"), addr("NASb"))) sRouteList(route( addr("NASb"), addr("Sa"), addr("NASb"))) sRouteList(route(addr("NASa"), addr("Sa"), addr("NASb")))) 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 30644) states: 30645 rewrites: 8096466 in 24090ms cpu (25370ms real) (336092 rewrites/second) state:State --> subnet(sAddrSet(addr("Ca")) sAddrSet(addr("NASa"))) subnet(sAddrSet(addr("NASb")) sAddrSet(addr("Sa"))) 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'")) l3a-server-start(node("S'")) interfaces(node("C"), sAddrSet(addr("Ca"))) interfaces(node("NAS"), sAddrSet(addr("NASa")) sAddrSet(addr("NASb"))) interfaces(node("S"), sAddrSet(addr("Sa"))) routetab(node("C"), sRouteList(route(addr("Ca"), addr("Ca"), addr("Ca"))) sRouteList(route(addr("NASa"), addr("Ca"), addr("NASa"))) sRouteList(route( addr("NASb"), addr("Ca"), addr("NASa"))) sRouteList(route(addr("Sa"), addr( "Ca"), addr("NASa")))) routetab(node("NAS"), sRouteList(route(addr("NASa"), addr("NASa"), addr( "NASa"))) sRouteList(route(addr("NASb"), addr("NASb"), addr("NASb"))) sRouteList(route(addr("Ca"), addr("NASa"), addr("Ca"))) sRouteList(route( addr("Sa"), addr("NASb"), addr("Sa")))) routetab(node("S"), sRouteList(route(addr("Sa"), addr("Sa"), addr("Sa"))) sRouteList(route(addr("Ca"), addr("Sa"), addr("NASb"))) sRouteList(route( addr("NASb"), addr("Sa"), addr("NASb"))) sRouteList(route(addr("NASa"), addr("Sa"), addr("NASb")))) 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)))