in prop-3.maude in common-3.maude in node-3.maude in addr-3.maude in state-3.maude in pki-3.maude in message-3.maude in routing-table-3.maude in ip-message-3.maude in ip-3.maude in ipsec-message-3.maude in l3a-message-1b.maude in security-assoc-3.maude in security-policy-3.maude in ipsec-3.maude in setkey-3.maude in sike-5.maude in l3a-1a.maude in l3a-client-app-2b.maude ***( a a C ----------- ------------- S | | a| |b NAS ) mod L3A-TEST is protecting L3A . protecting L3A-CLIENT-APP . mb keypair(seckey("SecretKeyOfC"), pubkey("PublicKeyOfC") ) : True . mb keypair(seckey("SecretKeyOfC'"), pubkey("PublicKeyOfC'") ) : True . mb keypair(seckey("SecretKeyOfNAS"), pubkey("PublicKeyOfNAS") ) : True . mb keypair(seckey("SecretKeyOfS"), pubkey("PublicKeyOfS") ) : True . mb keypair(seckey("SecretKeyOfS'"), pubkey("PublicKeyOfS'") ) : True . mb keypair(seckey("CredentialSecretKeyOfS"), pubkey("CredentialPublicKeyOfS") ) : True . mb keypair(seckey("CredentialSecretKeyOfS'"), pubkey("CredentialPublicKeyOfS'") ) : True . op initial : -> State . eq initial = shost(node("C")) shost(node("C'")) shost(node("NAS")) shost(node("S")) shost(node("S'")) sgw(node("NAS")) --- servers and clients are all connected via NAS (interfaces a-d) subnet(sAddrSet(addr("Ca")) sAddrSet(addr("NASa"))) subnet(sAddrSet(addr("NASb")) sAddrSet(addr("Sa"))) subnet(sAddrSet(addr("C'a")) sAddrSet(addr("NASc"))) subnet(sAddrSet(addr("NASd")) sAddrSet(addr("S'a"))) interfaces(node("C"),sAddrSet(addr("Ca"))) interfaces(node("C'"),sAddrSet(addr("C'a"))) interfaces(node("S"),sAddrSet(addr("Sa"))) interfaces(node("S'"),sAddrSet(addr("S'a"))) interfaces(node("NAS"),sAddrSet(addr("NASa")) sAddrSet(addr("NASb")) sAddrSet(addr("NASc")) sAddrSet(addr("NASd")) ) 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"),eSASet) sadb(node("C'"),eSASet) sadb(node("NAS"),eSASet) sadb(node("S"),eSASet) sadb(node("S'"),eSASet) --- C and NAS now accept all incomming traffic spdb(node("C"), sSPList(sp(any-pattern,eSAList)), sSPList(sp(any-pattern,eSAList)) ) spdb(node("C'"), sSPList(sp(any-pattern,eSAList)), sSPList(sp(any-pattern,eSAList)) ) spdb(node("NAS"), sSPList(sp(any-pattern,eSAList)), sSPList(sp(any-pattern,eSAList)) ) spdb(node("S"), sSPList(sp(any-pattern,eSAList)), sSPList(sp(any-pattern,eSAList)) ) spdb(node("S'"), sSPList(sp(any-pattern,eSAList)), sSPList(sp(any-pattern,eSAList)) ) --- initialize spi generator fresh-spi(node("C"),0) fresh-spi(node("C'"),0) fresh-spi(node("NAS"),0) fresh-spi(node("S"),0) fresh-spi(node("S'"),0) --- random number initialization fresh(0) --- start SIKE deamon on each node. siked-start(node("C") ) siked-start(node("C'") ) siked-start(node("NAS") ) siked-start(node("S") ) siked-start(node("S'") ) --- the public key info for each node. 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("NAS"),seckey("SecretKeyOfNAS"),pubkey("PublicKeyOfNAS"),cert(addr("NASa"),pubkey("PublicKeyOfNAS"))) --- what about NASb ? 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'"))) --- start up the two servers l3a-server-start(node("S")) l3a-server-start(node("S'")) --- start up the nas l3a-nas-start(node("NAS")) ***( C-- --S | | N ) l3a-client-app-start(node("C"), addr("Ca"), addr("Sa"), addr("NASa")) --- start the clients l3a-client-start(node("C"), addr("Ca")) l3a-client-start(node("C'"), addr("C'a")) . op initial2 : -> State . --- eq initial2 = op initial3 : -> State . --- eq initial3 = endm ***( rew initial . ) ***( search initial =>+ l3a-nas-terminated(node("NAS"), addr("Ca"), addr("NASa"), addr("Sa"), cert(addr("Ca"), pubkey("PublicKeyOfC")), 0, 1) remaining:State . ) ---- Aren't sure of the values so use variables. --- search initial2 =>! state:State . ***( l3a-server-expect-last-sadb-notify(node:Node,client:Addr,nas:Addr,server:Addr,cred:Cert,server-nas-spi:Nat,server-client-spi:Nat) remaining:State . ) ***( search initial3 =>! state:State . ) ***( in model-checker . mod L3A-MODEL-CHECK is protecting MODEL-CHECKER . protecting L3A-TEST . op terminated : -> Prop . eq (remaining:State l3a-client-terminated(node("C"), addr("Ca"), addr("NASa"), addr("Sa"), 0, 0) --- l3a-nas-terminated(node("NAS"), addr("Ca"), addr("NASa"), addr("Sa"), cert(addr("Ca"), pubkey("PublicKeyOfC")), 0, 1) l3a-server-terminated(node("S"), addr("Ca"), addr("NASa"), addr("Sa"), cert(addr("Ca"), pubkey("PublicKeyOfC")), 1, 0, 0)) |= terminated = true . endm )