mod IPSEC is

protecting COMMON .

including MESSAGE .
including IP-MESSAGE .
protecting IP .
including IPSEC-MESSAGE .

protecting SECURITY-ASSOC .
protecting SECURITY-POLICY .

including STATE .


--- -----------------------------------------------------------
--- This module provides an abstract model of IPSEC.
--- We don't try to model encryption and authentication. 
--- We are mostly concerned with setting up the SADB and
--- the SPDB. This is because we are trying to studying how
--- to compose IPSEC tunnels and the difficulties in getting
--- these configurations correct. 

--- We also model only ESP as AH isn't used anymore.
--- A tunnel is just a header with a source, destination and SPI.
--- We allow tunnels to be nested. Although we don't 
--- do authentication and encryption, our model of IPSEC does
--- check if a message is in the correct tunnel. 
--- When an IPSEC message is sent, the message contains a list of SAs.
--- When the message is received, the system checks  that destination 
--- is correct, that the SPI in the message header matches what the SADB.
--- The SPDB is also checked to make sure that there is a matching policy
--- for that message arriving on a particular SA.  


--- ip-sec-send-req  issues an ip-req. When the ip-ack is returned, an
--- ipsec-send-ack is send to the caller. This guarantees that a message
--- is out in the soup. 

--- -------------------------------------------------------------


sort Attr . --- message attributes
op discard : -> Attr .

var attr attr' : Attr .

------------------------

sort AttrSet .
op sAttrSet : Attr -> AttrSet .
op eAttrSet : -> AttrSet .
op __ : AttrSet AttrSet -> AttrSet [assoc comm id: eAttrSet] .

var attrset attrset' attrset'' : AttrSet .
var attrs : AttrSet .

op contains : AttrSet Attr -> Bool .
eq contains(eAttrSet, attr') = false .
eq contains((sAttrSet(attr) attrset), attr') = 
     (attr' == attr) or contains(attrset, attr') .

op add : AttrSet Attr -> AttrSet .
eq add(attrset,attr) = (attrset sAttrSet(attr)) .

op  add' : AttrSet Attr -> AttrSet .
ceq add'(attrset,attr) = attrset 
    if contains(attrset, attr) .
ceq add'(attrset,attr) = (attrset sAttrSet(attr)) 
    if not(contains(attrset, attr)) .

op  rm : AttrSet Attr -> AttrSet .
eq  rm(eAttrSet,attr) = eAttrSet .
ceq rm((sAttrSet(attr) attrset),attr') = rm(attrset,attr')
    if (attr' == attr) .
ceq rm((sAttrSet(attr) attrset),attr') = (sAttrSet(attr) rm(attrset,attr'))
    if (attr' =/= attr) .

op subset : AttrSet AttrSet -> Bool .
eq subset(eAttrSet,attrset') = true .
eq subset((sAttrSet(attr) attrset), attrset') = 
    contains(attrset',attr) and subset(attrset,attrset') .

---------------------

--- ipsec interface 

var agent : Agent .

--- We assume that each node can run several agents (usually simply
--- processes). So system calls like xxx-req are always associated
--- with a particular agent, and xxx-ack must be again associated with
--- that agent (and not stolen by somebody else).

op ipsec-send-req : Agent Node Message -> State .
op ipsec-send-ack : Agent Node  -> State .

op ipsec-received : Node Addr AttrSet SAList Message -> State .
op ipsec-delivered : Node Addr AttrSet SAList Message -> State .

op ipsec-expect-ip-ack : Agent Node Addr Addr Message -> State .

op ipsec-forward-expect-ack : Node Addr AttrSet SAList Message -> State .

op ipsec-forward-terminate : Node Addr AttrSet SAList Message -> State .


--- ipsec layer state

op spdb : Node SPList SPList -> State . --- security association policy data base
op sadb : Node SASet -> State . --- security association data base


------------------------------- IPSEC -------------------------------------

var node node' : Node .
var addr addr' addr'' : Addr .
var src dest : Addr .
var interfaces interfaces' : AddrSet .
var rinterface rinterface' sinterface : Addr .

var message message' sent-msg : Message .
var messagelist messagelist' : MessageList .

var sa sa' : SA .
var sabundle sabundle' : SAList .
var splist : SPList .

var sadb : SASet .
var spdb spindb spoutdb : SPList .
var pattern pattern' : Pattern .

--- node capabilities

op shost : Node -> State . --- node has ipsec host capabilities 
op sgw : Node -> State .   --- node has additionally ipsec gateway capabilities

op ipsec : SAList Message -> Message .
eq ipsec(eSAList,message) = message .
eq ipsec(sSAList(sa) sabundle,message) =
   ipsec(sabundle,ip(src(sa),dest(sa),sec(spi(sa),message))) .

--- outgoing ip/ipsec traffic (with or without (nested) encapsulation)

crl [ipsec-send] : 
    ipsec-send-req(agent,node, ip(src,dest,message))
    sadb(node,sadb)
    spdb(node,spindb,spoutdb) =>
    ip-send-req(agent,node, ipsec(sabundle(spoutdb,ip(src,dest,message)),ip(src,dest,message)))
    sadb(node,sadb)
    spdb(node,spindb,spoutdb)
    ipsec-expect-ip-ack(agent,node,src,dest,message)
    if contains(spoutdb,ip(src,dest,message)) and 
       contains(sadb,sabundle(spoutdb,ip(src,dest,message))) .

rl  ipsec-expect-ip-ack(agent,node,src,dest,message)
    ip-send-ack(agent,node) =>
    ipsec-send-ack(agent,node) .

--- incoming ip traffic (with or without (nested) encapsulation)

rl  [ipsec-receive]:
    shost(node)
    sadb(node,sadb)
    spdb(node,spindb,spoutdb)
    ip-received(node, rinterface, ip(src,dest,message)) =>
    shost(node)
    sadb(node,sadb)
    spdb(node,spindb,spoutdb)
    ipsec-received(node, rinterface, eAttrSet, eSAList, ip(src,dest,message)) .

--- process incoming ipsec traffic (remove encapsulation)

crl [ipsec-strip]:
    shost(node)
    sadb(node,sadb)
    spdb(node,spindb,spoutdb)
    ipsec-received(node, rinterface, attrs, sabundle, message) =>
    shost(node)
    sadb(node,sadb)
    spdb(node,spindb,spoutdb)
    ipsec-received(node, rinterface, attrs, (sSAList(sa(sasrc(message),sadest(message),saspi(message))) sabundle), ipsecstrip(message))
    if ip(message) /\ 
       if ipsec(message) then contains(sadb,sadest(message),saspi(message)) else false fi .

--- delivering incoming ipsec traffic (check spdb)

crl [ipsec-deliver]: 
    shost(node)
    sadb(node,sadb)
    spdb(node,spindb,spoutdb)
    ipsec-received(node, rinterface, attrs, sabundle, message) =>
    shost(node)
    sadb(node,sadb)
    spdb(node,spindb,spoutdb)
    ipsec-delivered(node, rinterface, attrs, sabundle, message)
    if ip(message) /\
       not(if ipsec(message) then contains(sadb,sadest(message),saspi(message)) else false fi) /\
       dest(message) == rinterface /\ contains(spindb,message,sabundle) .

--- forwarding ipsec traffic

op sgwagent : Node -> Agent . --- each node has a forwarding sgw agent running represented by sgw(node)

crl [ipsec-forward]:
    sgw(node)
    sadb(node,sadb)
    spdb(node,spindb,spoutdb)
    ipsec-received(node, rinterface, attrs, sabundle, message) =>
    sadb(node,sadb)
    spdb(node,spindb,spoutdb)
    ipsec-send-req(sgwagent(node), node, message)
    ipsec-forward-expect-ack(node, rinterface, attrs, sabundle, message)
    if ip(message) /\ 
       not(if ipsec(message) then contains(sadb,sadest(message),saspi(message)) else false fi) /\
       dest(message) =/= rinterface /\ contains(spindb,message,sabundle) .
 
rl  ipsec-forward-expect-ack(node, rinterface, attrs, sabundle, message)
    ipsec-send-ack(sgwagent(node),node) =>
    sgw(node) .

--- dropping ipsec traffic (delivered in discard mode)

crl [ipsec-discard]:
    shost(node)
    sadb(node,sadb)
    spdb(node,spindb,spoutdb)
    ipsec-received(node, rinterface, attrs, sabundle, message) =>
    shost(node)
    sadb(node,sadb)
    spdb(node,spindb,spoutdb)
    ipsec-delivered(node, rinterface, (attrs sAttrSet(discard)), sabundle, message)
    if ip(message) /\
       not(if ipsec(message) then contains(sadb,sadest(message),saspi(message)) else false fi) /\
       not(contains(spindb,message,sabundle))/\
       dest(message)== rinterface .

endm