mod SIKE is protecting BOOL . protecting NAT . protecting STRING . protecting PKI . protecting ADDR . protecting NODE . protecting MESSAGE . protecting IP . protecting IPSEC . protecting SETKEY . --- --------------------------------------------------- --- This module performs a key exchange between two nodes --- the initiator I and responder R. --- SIKE is a lot simpler than IKE and is simply the X509 --- protocol with a cookie generation. --- There is no guarantee of perfect secrecy. No Diffe-Helman --- exchange is performed. Instead, the responder just generates --- keys and sends them to the initiator. --- There is an assumption of a public key infrastructure. --- There are four messages in this protocol. --- The initiator first generates a nonce ri and SPI value x for the I<--R --- tunnel and sends. --- I-->R. msg1: ra SPI(x,0) --- The responder generates a nonce rr and a SPI value y for the R-->I --- tunnel. The responder also forms a cookie. --- R-->I: msg2. ri,rr, SPI(x,y), certB, cookie --- The initiator sends back --- I-->R:msg3 certi, cookie, DA, Ps(i,DA) --- where DA = [ri,rr,IPR,SPI(x,y)] --- --- R<--I: msg4 DB,Ps(r,DB) --- DB=ir,IPI,ri,SPI(x,y),Pe(I,K) --- where Ps(a,W) - sig of W using private key of a. --- Pe(A,W) - encrypt W using the public key of A. --- More details about SIKE can be found in other documentation. --- --------------------------------------------------- vars n n' m m' spi-A spi-B : Nat . var inout : TBU-SPD-IN-OUT . -------------------------------------------------------------- --- we aren't using the timestamps in the models now so --- I just generate null timestatms TA and TB . op TA : -> TimeStamp . op TB : -> TimeStamp . vars tA tB : TimeStamp . --------------------- ---- The secret used to form the cookie ---- changes periodically so you have to ----- know what version was used to produce ---- the cookie. sort VerSec . op versec : -> VerSec . --------------------- ---- The first round of the protocol ---- is to generate a cookie. ---- The cookie is a represented as a ---- pair with the first component ---- being the version of the secret ---- used to generate the secret and the ---- second component being the data in the ---- cookie. The data in the second component ---- is the hash of a tuple consisting of two ---- nonces and an address. sort Cookie . ---- Constructor and projection functions for the cookie. op cookie : VerSec Data -> Cookie . op cookieversec : Cookie -> VerSec . op cookiemsg : Cookie -> Data . ---- The hash fn operates on Data so the tuple is maped ---- into type data. op cookiedat : Nonce Nonce Addr -> Data . var cookieb : Cookie . var vs : VerSec . var md : Data . eq cookieversec(cookie(vs, md)) = vs . eq cookiemsg(cookie(vs, md)) = md . -------------------------------------------------------------- --- The initiator and receiver of the setup may not --- be the same as the src and dest of the tunnel that --- gets setup. So we have to keep track of this data. sort SADir . ---- SADir constructor ---- from to op sadir : Addr Addr -> SADir . --- projection fns. op sasrc : SADir -> Addr . op sadest : SADir -> Addr . eq sasrc(sadir(addr, addr')) = addr . eq sadest(sadir(addr,addr')) = addr' . vars sad sad' : SADir . ------------------------------------- ----- rA spi op msg1 : Nonce SPI -> Message . ------- rA rB spi CertB Cookie op msg2 : Nonce Nonce SPI Cert Cookie -> Message . ------- rA rB addrB spi op msg3data : Nonce Nonce Addr SPI -> Data . -------- CertA cookie Ss(B,msg3dat) op msg3 : Cert Cookie Data -> Message . -------- rB addrA rA spi Pe(A,secret) op msg4data : Nonce Addr Nonce SPI Data -> Data . ------- DB Ss(B,DB) op msg4 : Data -> Message . ------------------------------------------------------------- vars addr addr' : Addr . vars src dest : Addr . vars addrA addrB : Addr . vars nodeA nodeB : Node . ----- I don't really care about the receive interface rightnow so I ----- just have a couple of variables that I ignore. vars rinterA rinterB : Addr . vars interfaces interfaces' : AddrSet . -------------------------------------------------------------- vars seckey seckey' : SecKey . vars pubkey pubkey' pubkey'' : PubKey . var d : Data . vars signeddataA signeddataB : Data . op sharedkey : Nonce -> Data . var sharkey : Data . var decrypted-sharkey : Data . ------------------------- var attrs : AttrSet . var sabundle : SAList . var otherSAs : SAList . -------------------------- vars cert cert' : Cert . var secret : Nonce . vars rA rB : Nonce . var payload : Data . vars spi spi' : SPI . ------------------------------ var sa-setkey-term : SA . var spl-setkey-term : SPList . var upd-term : TBU-SPD-IN-OUT . ------------------------------ --------------------------------------------------------------- --- operation constructors --------------------------------------------------------------- --- fresh is used to generate nonces op fresh : Nat -> State . ------ fresh spi is used to generate new spi values. op fresh-spi : Node Nat -> State . --- the idea is that later sike uses fresh-spi to generate --- fresh spi's at the destination of the sa --- local states of sike ------ A addrA addrB CertA SecKeyA op sike-start : Node Addr Addr Cert SecKey -> State . ------ A addrA addrB CertA SecKeyA rA spi op sike-expect-ipsec-send-ack1 : Node Addr Addr Cert SecKey Nonce SPI -> State . ------ A addrA addrB CertA SecKeyA rA spi op sike-waiting : Node Addr Addr Cert SecKey Nonce SPI -> State . ------ A addrA addrB CertA SecKeyA rA spi rB CertB cookie op sike-phase-2 : Node Addr Addr Cert SecKey Nonce SPI Nonce Cert Cookie -> State . ------ A addrA addrB CertA SecKeyA rA spi rB CertB cookie op sike-expect-ipsec-send-ack2 : Node Addr Addr Cert SecKey Nonce SPI Nonce Cert Cookie -> State . ------ A addrA addrB CertA SecKeyA rA spi rB CertB cookie op sike-waiting-2 : Node Addr Addr Cert SecKey Nonce SPI Nonce Cert Cookie -> State . ------ A addrA addrB CertA SecKeyA rA SPI rB CertB cookie sharedKey op sike-setkey-start : Node Addr Addr Cert SecKey Nonce SPI Nonce Cert Cookie Data -> State . ------ A addrA addrB certA SecKeyA rA spi rB CertB cookie sharedKey op sike-expect-setkey-term : Node Addr Addr Cert SecKey Nonce SPI Nonce Cert Cookie Data -> State . ------ A addrA addrB CertA SecKeyA rA spi rB CertB cookie sharedKey op sike-expect-setkey-term' : Node Addr Addr Cert SecKey Nonce SPI Nonce Cert Cookie Data -> State . ------ A addrA addrB CertA SecKeyA rA rB CertB cookie spi sharedKey op sike-term : Node Addr Addr Cert SecKey Nonce Nonce Cert Cookie SPI Data -> State . ------ A addrA addrB spi op sike-ack : Node Addr Addr SPI -> State . --- local states of sike daemon --------- B op siked-start : Node -> State . --------- B addrB CertB SecKeyB op siked-start' : Node Addr Cert SecKey -> State . --------- B addrB CertB SecKeyB secret spi op siked-start'' : Node Addr Cert SecKey Nonce SPI -> State . -------- B addrB CertB SecKeyB secret spi rA addrA op siked-phase-1 : Node Addr Cert SecKey Nonce SPI Nonce Addr -> State . --------- B addrB CertB SecKeyB secret spi rA addrA rB op siked-expect-ipsec-send-ack1 : Node Addr Cert SecKey Nonce SPI Nonce Addr Nonce -> State . --------- B addrB CertB SecKeyB secret spi rA addrA rB op siked-waiting : Node Addr Cert SecKey Nonce SPI Nonce Addr Nonce -> State . --------- B addrB CertB SecKeyB secret spi rA addrA rB CertA op siked-phase-2 : Node Addr Cert SecKey Nonce SPI Nonce Addr Nonce Cert -> State . --------- B addrB CertB SecKeyB secret spi rA addrA rB CertA Pe(A,K) op siked-expect-setkey-term : Node Addr Cert SecKey Nonce SPI Nonce Addr Nonce Cert Data -> State . --------- B addrB CertB SecKeyB secret spi rA addrA rB CertA Pe(A,K) op siked-sent-msg4 : Node Addr Cert SecKey Nonce SPI Nonce Addr Nonce Cert Data -> State . --------- B addrB CertB SecKeyB secret spi rA addrA rB CertA Pe(A,K) op siked-expect-setkey-term' : Node Addr Cert SecKey Nonce SPI Nonce Addr Nonce Cert Data -> State . --------- B addrB CertB SecKeyB secret rA addrA rB CertA spi Pe(A,K) op siked-term : Node Addr Cert SecKey Nonce Nonce Addr Nonce Cert SPI Data -> State . -------- B addrA addrB spi op siked-notify : Node Addr Addr SPI -> State . --------- B addrB CertB SecKeyB secret spi rA addrA rB CertA Pe(A,K) op siked-restart : Node Addr Cert SecKey Nonce SPI Nonce Addr Nonce Cert Data -> State . op debug : -> State . ---------------- State Transitions --------------------- ------------initiator of protocol----------------------- op sike : Node -> Agent . ---- each node can have a sike agent running op siked : Node -> Agent . ---- each node can have a siked agent running --- Start up the the initiator. Generate a fresh nonce and sent it --- to the receiver. Move to the sike-wait state to wait for the --- response from the responder. rl [SikeStart] : fresh(m) fresh-spi(nodeA,n) sike-start(nodeA, addrA, addrB, cert, seckey) => fresh(s m) fresh-spi(nodeA,s(n)) sike-waiting(nodeA, addrA, addrB, cert, seckey, random(m), spi(n,0)) ipsec-send(sike(nodeA), nodeA, ip(addrA, addrB, msg1(random(m), spi(n,0) ) ) ) . ----- The initiator has received the message w/ the nonce sent in the ----- last rule, the responder's nonce, the responder's cert, and a cookie. ----- Move to the state phase2 or phase2' ( see below) . crl [SikeWaiting] : sike-waiting(nodeA, addrA, addrB, cert, seckey, rA, spi' ) ipsec-delivered(nodeA, rinterA, attrs, sabundle, ip(addrB,addrA, msg2(rA, rB, spi, cert', cookieb))) => sike-phase-2(nodeA, addrA, addrB, cert, seckey, rA, spi, rB, cert', cookieb) if not(contains(attrs,discard)) . ----- In phase2 msg3 is sent out. rl [SikePhase-2] : interfaces(nodeA, interfaces) sike-phase-2(nodeA, addrA, addrB, cert, seckey, rA, spi, rB, cert', cookieb) => interfaces(nodeA, interfaces) sike-waiting-2(nodeA, addrA, addrB, cert, seckey, rA, spi, rB, cert', cookieb) ipsec-send(sike(nodeA), nodeA, ip(addrA, addrB, msg3(cert, cookieb, sign(seckey, msg3data(rA, rB, addrB, spi))))) . ---- Wait for the shared key from the responder. ----- When it is received, move to the state to update the SADB and SPB via a call to setkey. crl [SikeWaiting-2] : sike-waiting-2(nodeA, addrA, addrB, cert, seckey, rA, spi, rB, cert', cookieb) ipsec-delivered(nodeA, rinterA, attrs, sabundle, ip(addrB, addrA, msg4(signeddataB))) => sike-setkey-start(nodeA, addrA, addrB, cert, seckey, rA, spi, rB, cert', cookieb, decrypt(seckey, sharkey)) if not(contains(attrs,discard)) /\ verify(certkey(cert'), signeddataB) : True /\ msg4data(rB, addrA, rA, spi, sharkey ) := data(signeddataB) . --- Call setkey to update the SADB for the SA A-->B. Setkey also adds the policy --- A-->B:[(A->B)] to the SPDB. rl [Setkey-Start] : interfaces(nodeA, interfaces) sike-setkey-start(nodeA, addrA, addrB, cert, seckey, rA, spi, rB, cert', cookieb, decrypted-sharkey) => interfaces(nodeA, interfaces) sike-expect-setkey-term(nodeA, addrA, addrB, cert, seckey, rA, spi, rB, cert', cookieb, decrypted-sharkey) setkey-start(nodeA,addrA,addrB, spival-resp(spi), OUT-SPD) . --- Wait for setkey to terminate and add call setkey again to update the SADB with the SA --- B-->A. The policy database is updated with B->A: [(B->A)] rl [Setkey-Start'] : interfaces(nodeA, interfaces) setkey-terminate(nodeA,addrA, addrB, spi-B, inout) sike-expect-setkey-term(nodeA, addrA, addrB, cert, seckey, rA, spi, rB, cert', cookieb, decrypted-sharkey) => sike-expect-setkey-term'(nodeA, addrA, addrB, cert, seckey, rA, spi, rB, cert', cookieb,decrypted-sharkey) interfaces(nodeA, interfaces) setkey-start(nodeA, addrB, addrA, spival-init(spi), IN-SPD) . --- Wait for the second invocation of setkey to terminate. --- Pass back to the calling module the relevant stuff. Drop the nonces, cookie,..... rl sike-expect-setkey-term'(nodeA, addrA, addrB, cert, seckey, rA, spi, rB, cert', cookieb, decrypted-sharkey) setkey-terminate(nodeA,addrB, addrA, spi-A, inout) => sike-term(nodeA, addrA, addrB, cert, seckey, rA, rB, cert', cookieb, spi, decrypted-sharkey) sike-ack(nodeA, addrA, addrB, spi) . ----------------------------------------------------------------------- ------------------------- deamon -------------------------------------- ----------------------------------------------------------------------- ----- start the deamon ------- --- get the first message from the party initiating the protocol crl [SikedStart] : siked-start(nodeB) pki-info(nodeB, seckey', pubkey', cert') fresh(m) ipsec-delivered(nodeB, rinterB, attrs, sabundle, ip(addrA, addrB, msg1(rA, spi(spi-A,0) ) ) ) => fresh(s m) pki-info(nodeB, seckey', pubkey', cert') siked-phase-1(nodeB, addrB, cert', seckey', random(m), spi(spi-A,0), rA, addrA) if not(contains(attrs,discard)) . --- Form the cookie and send the second message. rl [SikedPhase-1] : fresh(m) fresh-spi(nodeB, n') siked-phase-1(nodeB, addrB, cert', seckey', secret, spi(spi-A,0), rA, addrA) => fresh(s m) fresh-spi(nodeB, s n') siked-waiting(nodeB, addrB, cert', seckey', secret, spi(spi-A, n'), rA, addrA, random(m)) ipsec-send(siked(nodeB), nodeB, ip(addrB, addrA, msg2(rA, random(m), spi(spi-A,n'), cert', cookie(versec, hash(secret, cookiedat(rA, random(m), addrA)))))) . --- Get the third message, check its signature and verify the certificate. crl [SikedWaiting] : siked-waiting(nodeB, addrB, cert', seckey', secret, spi, rA, addrA, rB) ipsec-delivered(nodeB, rinterB, attrs, sabundle, ip(addrA, addrB, msg3(cert, cookieb, signeddataA))) => siked-phase-2(nodeB, addrB, cert', seckey', secret, spi, rA, addrA, rB, cert) if not(contains(attrs,discard)) /\ cookieb == cookie(versec, hash(secret, cookiedat(rA, rB, addrA))) /\ verify(certkey(cert), signeddataA) : True /\ msg3data(rA, rB, addrB, spi) := data(signeddataA) . --- rl [SikedPhase-2] : interfaces(nodeB, interfaces') fresh(m) siked-phase-2(nodeB, addrB, cert', seckey', secret, spi, rA, addrA, rB, cert) => interfaces(nodeB, interfaces') fresh(s m) siked-expect-setkey-term(nodeB, addrB, cert', seckey', secret, spi, rA, addrA, rB, cert, sharedkey(random(m))) setkey-start(nodeB, addrA, addrB,spival-resp(spi), IN-SPD) . rl [Siked-Send-MSG4] : siked-expect-setkey-term(nodeB, addrB, cert', seckey', secret, spi, rA, addrA, rB, cert, sharedkey(random(m))) setkey-terminate(nodeB, addrA, addrB,spi-B, inout) => siked-sent-msg4(nodeB, addrB, cert', seckey', secret, spi, rA, addrA, rB, cert, sharedkey(random(m))) ipsec-send(siked(nodeB), nodeB, ip(addrB, addrA, msg4( sign(seckey', msg4data(rB, addrA, rA, spi, encrypt(certkey(cert), sharedkey(random(m)))))))) . rl siked-sent-msg4(nodeB, addrB, cert', seckey', secret, spi, rA, addrA, rB, cert, sharedkey(random(m))) => siked-expect-setkey-term'(nodeB, addrB, cert', seckey', secret, spi, rA, addrA, rB, cert, sharedkey(random(m))) setkey-start(nodeB, addrB, addrA,spival-init(spi), OUT-SPD) . rl [sikedPhase3] : siked-expect-setkey-term'(nodeB, addrB, cert', seckey', secret, spi, rA, addrA, rB, cert,sharedkey(random(m))) setkey-terminate(nodeB, addrB, addrA,spi-A, inout) => siked-term(nodeB, addrB, cert', seckey', secret, rA, addrA, rB, cert, spi, sharedkey(random(m))) siked-notify(nodeB, addrA, addrB, spi) siked-restart(nodeB, addrB, cert', seckey', secret, spi, rA, addrA, rB, cert, sharedkey(random(m))) . crl [SikedRestart] : interfaces(nodeB, interfaces') siked-restart(nodeB, addrB, cert', seckey', secret, spi, rA, addrA, rB, cert, sharedkey(random(m))) => interfaces(nodeB, interfaces') siked-start(nodeB) if contains(interfaces', addrB) . endm