--- Formal Specification of the L3A Protocol ***( Suppose that a client wishes to establish a secure connection to a server via a network access server (NAS) using the L3A protocol. The client initiates a key exchange with the NAS to establish an authentication tunnel. Upon termination of the key exchange, the SPDB of the client is updated with an entry that directs all traffic destined for the server into the recently established authentication tunnel. The client then sends a req message to the NAS containing the address of the server and a credential that the server will present on behalf of the client. Upon receipt of the req message, the NAS updates its SPDB to indicate that all traffic flowing from the client to the server will travel through the recently established authentication tunnel. The NAS now begins a key exchange with the server to establish the second authentication tunnel. Upon termination of the key exchange, the NAS updates its SPDB to indicate that all traffic flowing from the server to the client shall travel through the newly established tunnel. The NAS then sends an ack message to the server containing the credential. Upon receiving the ack message, the server checks the credential. If the credential is valid, the server updates its SPDB to direct all traffic destined for the client into the recently created authentication tunnel. The server now initiates a key exchange with the client to create a transport mode SA that provides both encryption and authentication.Upon termination of the key exchange, the server has an SPDB entry indicating that all traffic from the client will enter the server via the newly created SA. There will also be a policy directing all traffic destined for the client to travel in the newly created SA, and that this SA is nested inside the authentication tunnel that goes from the server to the NAS. The client will have two similar policies upon termination of the key exchange. The Server now sends a fin message to the client to indicate that all the SAs have been established. ) mod L3A is protecting COMMON . protecting ADDR . protecting NODE . protecting PKI . protecting STATE . including MESSAGE . including IP-MESSAGE . protecting IP . including L3A-MESSAGE . protecting SECURITY-ASSOC . protecting SECURITY-POLICY . including IPSEC-MESSAGE . protecting IPSEC . --- protecting SECURITY-ASSOC-MANAGEMENT . protecting SIKE . protecting SETKEY . -------------------- var node node' : Node . var addr addr' addr'' : Addr . var src dest : Addr . var addrlist addrlist' : AddrList . var client nas server : Addr . var interfaces interfaces' : AddrSet . var rinterface rinterface' sinterface : Addr . var attrs : AttrSet . var sabundle : SAList . var sadb : SASet . var spdb spindb spoutdb : SPList . -------------------- var sa-setkey-term : SA . var spl-setkey-term : SPList . ------------------- var client-nas-spi server-nas-spi : SPI . var client-server-spi server-client-spi : SPI . -------------------- var client-nas-sharkey server-nas-sharkey : Data . var client-server-sharkey server-client-sharkey : Data . --------------------- var client-cred : Data . --- We have to send the cert of C from NAS to S so S can check the --- signature. --- CertC Ps(C,nsinitdata(time,NASIP), server op nsinit : Cert Data Addr -> Data . op nsinit : Cert Data -> Data . op null-payload : -> Data . --------------------------------------------------- --- running l3a client and its local state --------------------------------------------------- op l3a-client-start : Node Addr -> State . op l3a-client-req : Node Addr Addr Addr -> State . op l3a-client-expect-sike-ack-1 : Node Addr Addr Addr -> State . op l3a-client-send-req : Node Addr Addr Addr SPI -> State . op l3a-client-expect-sike-notify : Node Addr Addr Addr SPI -> State . op l3a-client-expect-sike-ack-2 : Node Addr Addr Addr SPI SPI -> State . op l3a-client-last-sike-start : Node Addr Addr Addr SPI SPI -> State . op l3a-client-wait-sike-ack-3 : Node Addr Addr Addr SPI SPI -> State . op l3a-client-ack : Node Addr Addr Addr -> State . op l3a-client-terminated : Node Addr Addr Addr SPI SPI SPI -> State . --- running l3a nas deamon and its local state op l3a-nas-start : Node -> State . op l3a-nas-got-notify : Node Addr Addr Addr Cert Data SPI -> State . op l3a-nas-phase2 : Node Addr Addr Addr Cert Data SPI -> State . op l3a-nas-waiting : Node Addr Addr Addr Cert Data SPI -> State . op l3a-nas-send-nasack : Node Addr Addr Addr Cert Data SPI SPI -> State . op l3a-nas-terminated : Node Addr Addr Addr Cert Data SPI SPI -> State . --- running l3a server deamon and its local state op l3a-server-start : Node -> State . op l3a-server-expect-ack : Node Addr Addr Data Cert SPI -> State . op l3a-server-check-cred : Node Addr Addr Data Cert SPI -> State . op l3a-server-activated : Node Addr Addr Addr Data Cert SPI -> State . op l3a-server-expect-sike-ack : Node Addr Addr Addr Data Cert SPI -> State . op l3a-server-wait-cs-notify : Node Addr Addr Addr Data Cert SPI SPI -> State . op l3a-server-terminated : Node Addr Addr Addr Data Cert SPI SPI SPI -> State . -------- We don't model time here so the Timelive operator stands in for the time that -------- the connection is alive. op Timelive : -> TimeStamp . var tlive : TimeStamp . var nsgn : Data . var cred : Data . --- the credential in from nsinit(....) var signdata : Data . ---- var ccert : Cert . var initiator-cert : Cert . var spi : SPI . var cert : Cert . var pubkey : PubKey . var seckey : SecKey . var payload : Data . --- each node can run a client/nas/server process --- (or possibly more ? then we need to distinguish between them) op client : Node -> Agent . op nas : Node -> Agent . op server : Node -> Agent . --- client actions --- C initiates setting up C ->->-> NAS rl l3a-client-start(node,client) l3a-client-req(node,client,nas,server) pki-info(node,seckey,pubkey,cert) => l3a-client-expect-sike-ack-1(node,client,nas,server) pki-info(node,seckey,pubkey,cert) sike-start(node, client, nas,cert, seckey, sadir(client,nas), nsinit(cert, sign(seckey,reqdata(Timelive,nas)),server) ) . --- C receives acknowledgement that C ->->-> NAS Key X is complete. rl l3a-client-expect-sike-ack-1(node,client,nas,server) sike-ack(node, client, nas, client-nas-spi) => l3a-client-send-req(node,client,nas,server,client-nas-spi) . --- C sends a req message to the NAS contaitning the credential that it will present to the server. --- The SPD is also updated so that all traffic from the client to the server goes into --- the C==>N tunnel. rl l3a-client-send-req(node,client,nas,server,client-nas-spi) --- pki-info(node,seckey,pubkey,cert) spdb(node,spindb,spoutdb) => --- pki-info(node,seckey,pubkey,cert) --- ipsec-send(client(node),node,ip(client,nas, req(cert, sign(seckey,reqdata(Timelive,nas)),server, New) ) ) spdb(node, spindb, sSPList(sp(src-dest-pattern(client,server),sSAList(sa(client, nas, spival-resp(client-nas-spi) )))) spoutdb) l3a-client-expect-sike-notify(node,client,nas,server,client-nas-spi) . --- C receives notification that C <-<-<- S key exchange completed rl l3a-client-expect-sike-notify(node,client,nas,server,client-nas-spi) pki-info(node,seckey,pubkey,cert) siked-notify(node, server, client, server-client-spi, payload) => sike-start(node, client,server,cert,seckey,sadir(client,server), null-payload) pki-info(node,seckey,pubkey,cert) l3a-client-wait-sike-ack-3(node,client,nas,server,client-nas-spi,server-client-spi) . rl l3a-client-wait-sike-ack-3(node,client,nas,server,client-nas-spi,server-client-spi) sike-ack(node, client,server, client-server-spi) => l3a-client-ack(node,client,nas,server) l3a-client-terminated(node,client,nas,server,client-nas-spi,server-client-spi, client-server-spi) . ---------------------------------------------- --- nas actions ---------------------------------------------- --- NAS receives notification that C ->->-> NAS key exchange is complete. rl l3a-nas-start(node) siked-notify(node, client, nas, client-nas-spi,nsinit(initiator-cert,client-cred,server)) => l3a-nas-got-notify(node,client,nas,server, initiator-cert,client-cred, client-nas-spi) . --- NAS now update databases. rl l3a-nas-got-notify(node,client,nas, server, initiator-cert, client-cred, client-nas-spi) spdb(node, spindb,spoutdb) => spdb(node, sSPList(sp(src-dest-pattern(client,server), sSAList(sa(client,nas,spival-resp(client-nas-spi))))) spindb, spoutdb) l3a-nas-phase2(node,client,nas,server,initiator-cert,client-cred,client-nas-spi) . --- NAS initiates setting up NAS <-<-<--- S rl l3a-nas-phase2(node,client,nas,server,initiator-cert,client-cred,client-nas-spi) pki-info(node, seckey, pubkey, cert) => l3a-nas-waiting(node,client, nas, server,initiator-cert,client-cred, client-nas-spi) sike-start(node, nas, server, cert, seckey, sadir(server,nas),nsinit(initiator-cert, client-cred )) . --- NAS receives acknowlegement that NAS <-<-<- S key exchange complete. rl l3a-nas-waiting(node,client,nas,server,initiator-cert,client-cred,client-nas-spi ) spdb(node, spindb,spoutdb) sike-ack(node, nas, server, server-nas-spi) => spdb(node, sSPList(sp(src-dest-pattern(server,client), sSAList(sa(server,nas,spival-init(server-nas-spi))))) spindb, spoutdb) l3a-nas-terminated(node,client,nas,server,initiator-cert,client-cred,client-nas-spi, server-nas-spi) . --------------------------------------------------------------------------------------------------------------------- --- server actions --------------------------------------------------------------------------------------------------------------------- --- S receives notification that NAS <-<-<- S has been set up rl l3a-server-start(node) siked-notify(node, nas, server, server-nas-spi, nsinit(ccert,client-cred)) => l3a-server-expect-ack(node, nas,server,client-cred, ccert, server-nas-spi) . --- NAS sends server ack containing client's credential and client's cert. rl l3a-server-expect-ack(node,nas,server,client-cred, ccert, server-nas-spi) spdb(node, spindb,spoutdb) => spdb(node,spindb, sSPList(sp(src-dest-pattern(server,certaddr(ccert)), sSAList(sa(server,nas,spival-init(server-nas-spi))))) spoutdb) l3a-server-check-cred(node,nas,server,client-cred, ccert, server-nas-spi) . crl l3a-server-check-cred(node,nas,server,client-cred, ccert, server-nas-spi) => l3a-server-activated(node,certaddr(ccert),nas,server,client-cred,ccert, server-nas-spi) if verify(certkey(ccert), client-cred) : True /\ reqdata(tlive,nas) := data(client-cred) . --- S initiates setting up C <-<-<- S rl l3a-server-activated(node,client,nas,server,client-cred,ccert, server-nas-spi) pki-info(node, seckey, pubkey, cert) => l3a-server-expect-sike-ack(node,client,nas,server,client-cred,ccert, server-nas-spi ) pki-info(node, seckey, pubkey, cert) sike-start(node, server, client, cert, seckey,sadir(server,client), null-payload ) . --- S receives acknowlegement that C <-<-<- S key exchange is complete rl l3a-server-expect-sike-ack(node,client,nas,server,client-cred,ccert, server-nas-spi ) sike-ack(node, server, client, server-client-spi ) => l3a-server-wait-cs-notify(node,client,nas,server,client-cred,ccert,server-nas-spi, server-client-spi) . --- S receives notification that C ->->-> S key exchange complete. rl l3a-server-wait-cs-notify(node,client,nas,server,client-cred,ccert, server-nas-spi,server-client-spi ) siked-notify(node,client,server,client-server-spi,payload) => l3a-server-terminated(node,client,nas,server,client-cred,ccert, server-nas-spi, server-client-spi,client-server-spi) . endm