--- Preliminary Specification of Sectrace on the basis of
--- SECURE TRACEROUTE (SECTRACE), Draft 0, December 2002,
--- Carl A. Gunter, Alwyn Goodloe, and Michael McDougall

mod SECTRACE is

protecting BOOL .
protecting NAT .
protecting STRING .

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

--- Note: To stay within Core Maude, we explicitly give all required
--- instantiations of parameterized sorts in the following.  In a
--- future version we should use Full Maude and its parameterized
--- modules.

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

var n : Nat .
var nat nat' : Nat .

sort NatList .
op sNatList : Nat -> NatList .
op eNatList : -> NatList .
op __ : NatList NatList -> NatList [assoc id: eNatList] .

var natlist natlist' : NatList .

op contains : NatList Nat -> Bool .
eq contains(eNatList, nat') = false .
eq contains((sNatList(nat) natlist), nat') = 
     (nat' == nat) or contains(natlist, nat') .

op add : NatList Nat -> NatList .
eq add(natlist,nat) = (natlist sNatList(nat)) .

op  add' : NatList Nat -> NatList .
ceq add'(natlist,nat) = natlist 
    if contains(natlist, nat) .
ceq add'(natlist,nat) = (natlist sNatList(nat)) 
    if not(contains(natlist, nat)) .

op  rm : NatList Nat -> NatList .
eq  rm(eNatList,nat) = eNatList .
ceq rm((sNatList(nat) natlist),nat') = rm(natlist,nat')
    if (nat' == nat) .
ceq rm((sNatList(nat) natlist),nat') = (sNatList(nat) rm(natlist,nat'))
    if (nat' =/= nat) .

op subset : NatList NatList -> Bool .
eq subset(eNatList,natlist') = true .
eq subset((sNatList(nat) natlist), natlist') = 
    contains(natlist',nat) and subset(natlist,natlist') .

op ith : NatList Nat -> Nat .
eq ith(sNatList(nat) natlist, 0) = nat .
eq ith(sNatList(nat) natlist, (s n)) = ith(natlist,n) .

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

sort Node .
op node : String -> Node .

var node node' : Node .

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

sort Addr .
op addr : String -> Addr .
op anyaddr : -> Addr .

var addr addr' addr'' : Addr .

op match : Addr Addr -> Bool .
eq match(anyaddr,addr') = true .
ceq match(addr,addr') = (addr == addr') if addr =/= anyaddr .

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

sort AddrList .
op sAddrList : Addr -> AddrList .
op eAddrList : -> AddrList .
op __ : AddrList AddrList -> AddrList [assoc id: eAddrList] .

var addrlist addrlist' : AddrList .

op contains : AddrList Addr -> Bool .
eq contains(eAddrList, addr') = false .
eq contains((sAddrList(addr) addrlist), addr') = 
     (addr' == addr) or contains(addrlist, addr') .

op add : AddrList Addr -> AddrList .
eq add(addrlist,addr) = (addrlist sAddrList(addr)) .

op  add' : AddrList Addr -> AddrList .
ceq add'(addrlist,addr) = addrlist 
    if contains(addrlist, addr) .
ceq add'(addrlist,addr) = (addrlist sAddrList(addr)) 
    if not(contains(addrlist, addr)) .

op  rm : AddrList Addr -> AddrList .
eq  rm(eAddrList,addr) = eAddrList .
ceq rm((sAddrList(addr) addrlist),addr') = rm(addrlist,addr')
    if (addr' == addr) .
ceq rm((sAddrList(addr) addrlist),addr') = (sAddrList(addr) rm(addrlist,addr'))
    if (addr' =/= addr) .

op subset : AddrList AddrList -> Bool .
eq subset(eAddrList,addrlist') = true .
eq subset((sAddrList(addr) addrlist), addrlist') = 
    contains(addrlist',addr) and subset(addrlist,addrlist') .

op ith : AddrList Nat -> Addr .
eq ith(sAddrList(addr) addrlist, 0) = addr .
eq ith(sAddrList(addr) addrlist, (s n)) = ith(addrlist,n) .

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

sort AddrSet .
op sAddrSet : Addr -> AddrSet .
op eAddrSet : -> AddrSet .
op __ : AddrSet AddrSet -> AddrSet [assoc comm id: eAddrSet] .

var addrset addrset' addrset'' : AddrSet .

op contains : AddrSet Addr -> Bool .
eq contains(eAddrSet, addr') = false .
eq contains((sAddrSet(addr) addrset), addr') = 
     (addr' == addr) or contains(addrset, addr') .

op add : AddrSet Addr -> AddrSet .
eq add(addrset,addr) = (addrset sAddrSet(addr)) .

op  add' : AddrSet Addr -> AddrSet .
ceq add'(addrset,addr) = addrset 
    if contains(addrset, addr) .
ceq add'(addrset,addr) = (addrset sAddrSet(addr)) 
    if not(contains(addrset, addr)) .

op  rm : AddrSet Addr -> AddrSet .
eq  rm(eAddrSet,addr) = eAddrSet .
ceq rm((sAddrSet(addr) addrset),addr') = rm(addrset,addr')
    if (addr' == addr) .
ceq rm((sAddrSet(addr) addrset),addr') = (sAddrSet(addr) rm(addrset,addr'))
    if (addr' =/= addr) .

op subset : AddrSet AddrSet -> Bool .
eq subset(eAddrSet,addrset') = true .
eq subset((sAddrSet(addr) addrset), addrset') = 
    contains(addrset',addr) and subset(addrset,addrset') .

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

sort AddrPair .
op `(_`,_`) : Addr Addr -> AddrPair .

var addrpair addrpair' : AddrPair .

sort AddrPairSet .
op sAddrPairSet : AddrPair -> AddrPairSet .
op eAddrPairSet : -> AddrPairSet .
op __ : AddrPairSet AddrPairSet -> AddrPairSet [assoc comm id: eAddrPairSet] .

var addrpairset addrpairset' addrpairset'' : AddrPairSet .

op contains : AddrPairSet AddrPair -> Bool .
eq contains(eAddrPairSet, addrpair') = false .
eq contains((sAddrPairSet(addrpair) addrpairset), addrpair') = 
     (addrpair' == addrpair) or contains(addrpairset, addrpair') .

op add : AddrPairSet AddrPair -> AddrPairSet .
eq add(addrpairset,addrpair) = (addrpairset sAddrPairSet(addrpair)) .

op  add' : AddrPairSet AddrPair -> AddrPairSet .
ceq add'(addrpairset,addrpair) = addrpairset 
    if contains(addrpairset, addrpair) .
ceq add'(addrpairset,addrpair) = (addrpairset sAddrPairSet(addrpair)) 
    if not(contains(addrpairset, addrpair)) .

op  rm : AddrPairSet AddrPair -> AddrPairSet .
eq  rm(eAddrPairSet,addrpair) = eAddrPairSet .
ceq rm((sAddrPairSet(addrpair) addrpairset),addrpair') = rm(addrpairset,addrpair')
    if (addrpair' == addrpair) .
ceq rm((sAddrPairSet(addrpair) addrpairset),addrpair') = (sAddrPairSet(addrpair) rm(addrpairset,addrpair'))
    if (addrpair' =/= addrpair) .

op subset : AddrPairSet AddrPairSet -> Bool .
eq subset(eAddrPairSet,addrpairset') = true .
eq subset((sAddrPairSet(addrpair) addrpairset), addrpairset') = 
    contains(addrpairset',addrpair) and subset(addrpairset,addrpairset') .

op  lookup : AddrPairSet Addr ~> Addr .
ceq lookup(sAddrPairSet((addr,addr')) addrpairset, addr'') = addr'
    if addr == addr'' .
ceq lookup(sAddrPairSet((addr,addr')) addrpairset, addr'') = 
    lookup(addrpairset,addr'')
    if addr =/= addr'' .

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

sort AddrSetList .
op sAddrSetList : AddrSet -> AddrSetList .
op eAddrSetList : -> AddrSetList .
op __ : AddrSetList AddrSetList -> AddrSetList [assoc id: eAddrSetList] .

var addrsetlist addrsetlist' : AddrSetList .

op contains : AddrSetList AddrSet -> Bool .
eq contains(eAddrSetList, addrset') = false .
eq contains((sAddrSetList(addrset) addrsetlist), addrset') = 
     (addrset' == addrset) or contains(addrsetlist, addrset') .

op add : AddrSetList AddrSet -> AddrSetList .
eq add(addrsetlist,addrset) = (addrsetlist sAddrSetList(addrset)) .

op  add' : AddrSetList AddrSet -> AddrSetList .
ceq add'(addrsetlist,addrset) = addrsetlist 
    if contains(addrsetlist, addrset) .
ceq add'(addrsetlist,addrset) = (addrsetlist sAddrSetList(addrset)) 
    if not(contains(addrsetlist, addrset)) .

op  rm : AddrSetList AddrSet -> AddrSetList .
eq  rm(eAddrSetList,addrset) = eAddrSetList .
ceq rm((sAddrSetList(addrset) addrsetlist),addrset') = rm(addrsetlist,addrset')
    if (addrset' == addrset) .
ceq rm((sAddrSetList(addrset) addrsetlist),addrset') = (sAddrSetList(addrset) rm(addrsetlist,addrset'))
    if (addrset' =/= addrset) .

op subset : AddrSetList AddrSetList -> Bool .
eq subset(eAddrSetList,addrsetlist') = true .
eq subset((sAddrSetList(addrset) addrsetlist), addrsetlist') = 
    contains(addrsetlist',addrset) and subset(addrsetlist,addrsetlist') .

op ith : AddrSetList Nat -> AddrSet .
eq ith(sAddrSetList(addrset) addrsetlist, 0) = addrset .
eq ith(sAddrSetList(addrset) addrsetlist, (s n)) = ith(addrsetlist,n) .

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

sort Message .

--- plain ip packet

op ip : Addr      --- source
        Addr      --- destination
        Message   --- contents
     -> Message .

--- esp or ah header for ipsec

op sec :   Nat       --- sa spi
           Message 
        -> Message .

--- sectrace packets

op rreq : Addr      --- client
          Addr      --- server
       -> Message .

op rrep :  Addr     --- client (as above)
           Addr     --- server (as above)
           Addr     --- root ca of this node
           AddrSet  --- set of trusted ca roots
           Bool     --- done flag
        -> Message . 

op sareq : Addr     --- client (as above)
           Addr     --- server (as above)
           Addr     --- requested initiator
           Addr     --- requested responder
        -> Message .

op sarep : Addr     --- client (as above)
           Addr     --- server (as above)
           Addr     --- initiator (as above)
           Addr     --- responder (as above)
           Bool     --- done flag
        -> Message .

var message message' : Message .

var src src' dest dest' : Addr .

--- ip message projections 

op ip : Message ~> Bool .
eq ip(ip(src,dest,message)) = true .

op src : Message ~> Addr .
eq src(ip(src,dest,message)) = src .

op dest : Message ~> Addr .
eq dest(ip(src,dest,message)) = dest .

--- ipsec message projections

var sasrc sadest : Addr .
var saspi : Nat .

op ipsec : Message ~> Bool .
eq ipsec(ip(sasrc,sadest,sec(saspi,message))) = true .
eq ipsec(ip(sasrc,sadest,ip(src,dest,message))) = false .
eq ipsec(ip(sasrc,sadest,rreq(client,server))) = false .
eq ipsec(ip(sasrc,sadest,rrep(client,server,root,trustedroots,done))) = false .
eq ipsec(ip(sasrc,sadest,sareq(client,server,initiator,responder))) = false .
eq ipsec(ip(sasrc,sadest,sarep(client,server,initiator,responder,done))) = false .

op ipsecstrip : Message ~> Message .
eq ipsecstrip(ip(sasrc,sadest,sec(saspi,message))) = message .

op sasrc : Message ~> Addr .
eq sasrc(ip(sasrc,sadest,sec(saspi,message))) = sasrc .

op sadest : Message ~> Addr .
eq sadest(ip(sasrc,sadest,sec(saspi,message))) = sadest .

op saspi : Message ~> Nat .
eq saspi(ip(sasrc,sadest,sec(saspi,message))) = saspi .

--- sectrace message projections

var client server : Addr .
var root : Addr .
var trustedroots : AddrSet .
var done : Bool .
var initiator initiator' responder responder' : Addr .

op rreq : Message ~> Bool .
eq rreq(ip(src,dest,rreq(client,server))) = true .
eq rreq(ip(src,dest,rrep(client,server,root,trustedroots,done))) = false .
eq rreq(ip(src,dest,sareq(client,server,initiator,responder))) = false .
eq rreq(ip(src,dest,sarep(client,server,initiator,responder,done))) = false .

op rrep : Message ~> Bool .
eq rrep(ip(src,dest,rreq(client,server))) = false .
eq rrep(ip(src,dest,rrep(client,server,root,trustedroots,done))) = true .
eq rrep(ip(src,dest,sareq(client,server,initiator,responder))) = false .
eq rrep(ip(src,dest,sarep(client,server,initiator,responder,done))) = false .

op sareq : Message ~> Bool .
eq sareq(ip(src,dest,rreq(client,server))) = false .
eq sareq(ip(src,dest,rrep(client,server,root,trustedroots,done))) = false .
eq sareq(ip(src,dest,sareq(client,server,initiator,responder))) = true .
eq sareq(ip(src,dest,sarep(client,server,initiator,responder,done))) = false .

op sarep : Message ~> Bool .
eq sarep(ip(src,dest,rreq(client,server))) = false .
eq sarep(ip(src,dest,rrep(client,server,root,trustedroots,done))) = false .
eq sarep(ip(src,dest,sareq(client,server,initiator,responder))) = false .
eq sarep(ip(src,dest,sarep(client,server,initiator,responder,done))) = true .

op server : Message ~> Addr .
eq server(ip(src,dest,rreq(client,server))) = server .
eq server(ip(src,dest,sareq(client,server,initiator,responder))) = server .

op root : Message ~> Addr .
eq root(ip(src,dest,rrep(client,server,root,trustedroots,done))) = root .

op trustedroots : Message ~> AddrSet .
eq trustedroots(ip(src,dest,rrep(client,server,root,trustedroots,done))) = trustedroots .


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

sort MessageList .
op sMessageList : Message -> MessageList .
op eMessageList : -> MessageList .
op __ : MessageList MessageList -> MessageList [assoc id: eMessageList] .

var messagelist messagelist' : MessageList .

op contains : MessageList Message -> Bool .
eq contains(eMessageList, message') = false .
eq contains((sMessageList(message) messagelist), message') = 
     (message' == message) or contains(messagelist, message') .

op add : MessageList Message -> MessageList .
eq add(messagelist,message) = (messagelist sMessageList(message)) .

op  add' : MessageList Message -> MessageList .
ceq add'(messagelist,message) = messagelist 
    if contains(messagelist, message) .
ceq add'(messagelist,message) = (messagelist sMessageList(message)) 
    if not(contains(messagelist, message)) .

op  rm : MessageList Message -> MessageList .
eq  rm(eMessageList,message) = eMessageList .
ceq rm((sMessageList(message) messagelist),message') = rm(messagelist,message')
    if (message' == message) .
ceq rm((sMessageList(message) messagelist),message') = (sMessageList(message) rm(messagelist,message'))
    if (message' =/= message) .

op subset : MessageList MessageList -> Bool .
eq subset(eMessageList,messagelist') = true .
eq subset((sMessageList(message) messagelist), messagelist') = 
    contains(messagelist',message) and subset(messagelist,messagelist') .

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

sort MessageSet .
op sMessageSet : Message -> MessageSet .
op eMessageSet : -> MessageSet .
op __ : MessageSet MessageSet -> MessageSet [assoc comm id: eMessageSet] .

var messageset messageset' : MessageSet .
var received : MessageSet .

op contains : MessageSet Message -> Bool .
eq contains(eMessageSet, message') = false .
eq contains((sMessageSet(message) messageset), message') = 
     (message' == message) or contains(messageset, message') .

op add : MessageSet Message -> MessageSet .
eq add(messageset,message) = (messageset sMessageSet(message)) .

op  add' : MessageSet Message -> MessageSet .
ceq add'(messageset,message) = messageset 
    if contains(messageset, message) .
ceq add'(messageset,message) = (messageset sMessageSet(message)) 
    if not(contains(messageset, message)) .

op  rm : MessageSet Message -> MessageSet .
eq  rm(eMessageSet,message) = eMessageSet .
ceq rm((sMessageSet(message) messageset),message') = rm(messageset,message')
    if (message' == message) .
ceq rm((sMessageSet(message) messageset),message') = (sMessageSet(message) rm(messageset,message'))
    if (message' =/= message) .

op subset : MessageSet MessageSet -> Bool .
eq subset(eMessageSet,messageset') = true .
eq subset((sMessageSet(message) messageset), messageset') = 
    contains(messageset',message) and subset(messageset,messageset') .

-------------------- 
--- routing table entry

sort Route .

op route : Addr Addr Addr -> Route .

var route route' : Route .

op dest : Route -> Addr .
eq dest(route(dest,sinterface,nexthop)) = dest .

op sinterface : Route -> Addr .
eq sinterface(route(dest,sinterface,nexthop)) = sinterface .

op nexthop : Route -> Addr .
eq nexthop(route(dest,sinterface,nexthop)) = nexthop .

-------------------- 
--- routing table

sort RouteList .
op sRouteList : Route -> RouteList .
op eRouteList : -> RouteList .
op __ : RouteList RouteList -> RouteList [assoc id: eRouteList] .

var routelist routelist' : RouteList .

op contains : RouteList Route -> Bool .
eq contains(eRouteList, route') = false .
eq contains((sRouteList(route) routelist), route') = 
     (route' == route) or contains(routelist, route') .

op add : RouteList Route -> RouteList .
eq add(routelist,route) = (routelist sRouteList(route)) .

op  add' : RouteList Route -> RouteList .
ceq add'(routelist,route) = routelist 
    if contains(routelist, route) .
ceq add'(routelist,route) = (routelist sRouteList(route)) 
    if not(contains(routelist, route)) .

op  rm : RouteList Route -> RouteList .
eq  rm(eRouteList,route) = eRouteList .
ceq rm((sRouteList(route) routelist),route') = rm(routelist,route')
    if (route' == route) .
ceq rm((sRouteList(route) routelist),route') = (sRouteList(route) rm(routelist,route'))
    if (route' =/= route) .

op subset : RouteList RouteList -> Bool .
eq subset(eRouteList,routelist') = true .
eq subset((sRouteList(route) routelist), routelist') = 
    contains(routelist',route) and subset(routelist,routelist') .

op ith : RouteList Nat -> Route .
eq ith(sRouteList(route) routelist, 0) = route .
eq ith(sRouteList(route) routelist, (s n)) = ith(routelist,n) .

--- more specific functions

op  contains : RouteList Addr -> Bool .
eq  contains(eRouteList, addr') = false .
eq  contains((sRouteList(route) routelist), addr') = 
     (addr' == dest(route)) or contains(routelist, addr') .

op  sinterface : RouteList Addr -> Addr .
ceq sinterface((sRouteList(route) routelist), addr') =
    sinterface(route) if addr' == dest(route) .
ceq sinterface((sRouteList(route) routelist), addr') =
    sinterface(routelist,addr') if addr' =/= dest(route) .

op  nexthop : RouteList Addr -> Addr .
ceq nexthop((sRouteList(route) routelist), addr') =
    nexthop(route) if addr' == dest(route) .
ceq nexthop((sRouteList(route) routelist), addr') =
    nexthop(routelist,addr') if addr' =/= dest(route) .

--- lifted version of route

op route : AddrSet Addr Addr -> RouteList .
eq route(eAddrSet,sinterface,nexthop) = eRouteList .
eq route((sAddrSet(dest) addrset),sinterface,nexthop) =
   sRouteList(route(dest,sinterface,nexthop))
   route(addrset,sinterface,nexthop) .

--------------------
--- security association

sort SA .
op sa : Addr        --- source
        Addr        --- destination
        Nat         --- SPI
     -> SA .

var spi : Nat .

--- projections

op src : SA -> Addr .
eq src(sa(src,dest,spi)) = src .

op dest : SA -> Addr .
eq dest(sa(src,dest,spi)) = dest .

op spi : SA -> Nat .
eq spi(sa(src,dest,spi)) = spi .

var sa sa' : SA .

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

sort SAList .
op sSAList : SA -> SAList .
op eSAList : -> SAList .
op __ : SAList SAList -> SAList [assoc id: eSAList] .

var salist salist' : SAList .

op contains : SAList SA -> Bool .
eq contains(eSAList, sa') = false .
eq contains((sSAList(sa) salist), sa') = 
     (sa' == sa) or contains(salist, sa') .

op  add : SAList SA -> SAList .
eq  add(salist,sa) = (salist sSAList(sa)) .

op  add' : SAList SA -> SAList .
ceq add'(salist,sa) = salist 
    if contains(salist, sa) .
ceq add'(salist,sa) = (salist sSAList(sa)) 
    if not(contains(salist, sa)) .

op  rm : SAList SA -> SAList .
eq  rm(eSAList,sa) = eSAList .
ceq rm((sSAList(sa) salist),sa') = rm(salist,sa')
    if (sa' == sa) .
ceq rm((sSAList(sa) salist),sa') = (sSAList(sa) rm(salist,sa'))
    if (sa' =/= sa) .

op subset : SAList SAList -> Bool .
eq subset(eSAList,salist') = true .
eq subset((sSAList(sa) salist), salist') = 
    contains(salist',sa) and subset(salist,salist') .

op ith : SAList Nat -> SA .
eq ith(sSAList(sa) salist, 0) = sa .
eq ith(sSAList(sa) salist, (s n)) = ith(salist,n) .

---------------------
sort SASet .
op sSASet : SA -> SASet .
op eSASet : -> SASet .
op __ : SASet SASet -> SASet [assoc comm id: eSASet] .

var saset saset' : SASet .

op contains : SASet SA -> Bool .
eq contains(eSASet, sa') = false .
eq contains((sSASet(sa) saset), sa') = 
     (sa' == sa) or contains(saset, sa') .

op  add : SASet SA -> SASet .
eq  add(saset,sa) = (saset sSASet(sa)) .

op  add' : SASet SA -> SASet .
ceq add'(saset,sa) = saset 
    if contains(saset, sa) .
ceq add'(saset,sa) = (saset sSASet(sa)) 
    if not(contains(saset, sa)) .

op  rm : SASet SA -> SASet .
eq  rm(eSASet,sa) = eSASet .
ceq rm((sSASet(sa) saset),sa') = rm(saset,sa')
    if (sa' == sa) .
ceq rm((sSASet(sa) saset),sa') = (sSASet(sa) rm(saset,sa'))
    if (sa' =/= sa) .

op subset : SASet SASet -> Bool .
eq subset(eSASet,saset') = true .
eq subset((sSASet(sa) saset), saset') = 
    contains(saset',sa) and subset(saset,saset') .

--- more specific functions

op contains : SASet Addr Nat -> Bool .
eq contains(eSASet, dest,spi) = false .
eq contains((sSASet(sa) saset), dest,spi) = 
     ((dest(sa) == dest) and (spi(sa) == spi)) or 
     contains(saset, dest,spi) .

op contains : SASet SAList -> Bool .
eq contains(saset, eSAList) = true .
eq contains(saset, sSAList(sa') salist') = 
     contains(saset, dest(sa'),spi(sa')) and contains(saset,salist') .

op restrict : SASet Addr -> SASet . --- not used
eq restrict(eSASet,initiator) = eSASet .
ceq restrict(sSASet(sa) saset,initiator) = 
    (sSASet(sa) restrict(saset,initiator)) 
    if src(sa) == initiator .
ceq restrict(sSASet(sa) saset,initiator) = 
    restrict(saset,initiator) 
    if src(sa) =/= initiator .

---------------------
--- security policy

--- policy selection pattern

sort Pattern . 

op isinitiation : -> Pattern . --- sectrace initiation traffic
op isresponse : -> Pattern .   --- sectrace response traffic
op towards : Addr -> Pattern . --- sectrace traffic towards server

var pattern pattern' : Pattern .

--- security policy database entry

sort SP .
op sp :  Pattern    --- pattern for selection
         SAList     --- security association bundle
      -> SP .

var sp sp' : SP .
var sabundle sabundle' : SAList .

--- projections

op pattern : SP -> Pattern .
eq pattern(sp(pattern,sabundle)) = pattern .

op sabundle : SP -> SAList .
eq sabundle(sp(pattern,sabundle)) = sabundle .

--- access innermost message 
--- (e.g. to find ultimate destination (server) in case of rrep)

op  innermost : Message -> Message .
eq  innermost(ip(src,dest,sec(spi,message))) = message .
ceq innermost(message) = message 
    if rreq(message) or rrep(message) or sareq(message) or sarep(message) .

--- check if message matches pattern of security policy

op  match : SP Message ~> Bool .
eq  match(sp(isinitiation,sabundle),message) = 
    rreq(innermost(message)) or sareq(innermost(message)) .
eq  match(sp(isresponse,sabundle),message) = 
    rrep(innermost(message)) or sarep(innermost(message)) .
ceq match(sp(towards(server),sabundle),message) = 
    match(server,server(innermost(message)))
    if rreq(innermost(message)) or sareq(innermost(message)) .
ceq match(sp(towards(server),sabundle),message) = false
    if not(rreq(innermost(message)) or sareq(innermost(message))) .

--------------------
--- security policy database (unordered)

sort SPSet .
op sSPSet : SP -> SPSet .
op eSPSet : -> SPSet .
op __ : SPSet SPSet -> SPSet [assoc id: eSPSet] .

var spset spset' : SPSet .

op contains : SPSet SP -> Bool .
eq contains(eSPSet, sp') = false .
eq contains((sSPSet(sp) spset), sp') = 
     (sp' == sp) or contains(spset, sp') .

op  add : SPSet SP -> SPSet .
eq  add(spset,sp) = (spset sSPSet(sp)) .

op  add' : SPSet SP -> SPSet .
ceq add'(spset,sp) = spset 
    if contains(spset, sp) .
ceq add'(spset,sp) = (spset sSPSet(sp)) 
    if not(contains(spset, sp)) .

op  rm : SPSet SP -> SPSet .
eq  rm(eSPSet,sp) = eSPSet .
ceq rm((sSPSet(sp) spset),sp') = rm(spset,sp')
    if (sp' == sp) .
ceq rm((sSPSet(sp) spset),sp') = (sSPSet(sp) rm(spset,sp'))
    if (sp' =/= sp) .

op subset : SPSet SPSet -> Bool .
eq subset(eSPSet,spset') = true .
eq subset((sSPSet(sp) spset), spset') = 
    contains(spset',sp) and subset(spset,spset') .

***(
--- more specific functions

op contains : SPSet Pattern -> Bool .
eq contains(eSPSet, pattern') = false .
eq contains((sSPSet(sp) spset), pattern') = 
     (pattern(sp) == pattern') or contains(spset, pattern') .

op  contains : SPSet Message -> Bool .
eq  contains(eSPSet, message) = false .
eq  contains((sSPSet(sp) spset), message) = 
     match(sp,message) or contains(spset, message) .

op  sabundle : SPSet Message -> SASet .
ceq sabundle((sSPSet(sp) spset), message) = 
    sabundle(sp) if match(sp,message) .
ceq sabundle((sSPSet(sp) spset), message) = 
    sabundle(spset, message) if not(match(sp,message)) .

op  contains : SPSet Message SASet -> Bool .
eq  contains(eSPSet,message,sabundle) = false .
eq  contains((sSPSet(sp) spset), message, sabundle) = 
     (match(sp,message) and sabundle(sp) == sabundle) or 
     contains(spset,message,sabundle) .
)

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

sort SPSetList .
op sSPSetList : SPSet -> SPSetList .
op eSPSetList : -> SPSetList .
op __ : SPSetList SPSetList -> SPSetList [assoc id: eSPSetList] .

var spsetlist spsetlist' : SPSetList .

op contains : SPSetList SPSet -> Bool .
eq contains(eSPSetList, spset') = false .
eq contains((sSPSetList(spset) spsetlist), spset') = 
     (spset' == spset) or contains(spsetlist, spset') .

op  add : SPSetList SPSet -> SPSetList .
eq  add(spsetlist,spset) = (spsetlist sSPSetList(spset)) .

op  add' : SPSetList SPSet -> SPSetList .
ceq add'(spsetlist,spset) = spsetlist 
    if contains(spsetlist, spset) .
ceq add'(spsetlist,spset) = (spsetlist sSPSetList(spset)) 
    if not(contains(spsetlist, spset)) .

op  rm : SPSetList SPSet -> SPSetList .
eq  rm(eSPSetList,spset) = eSPSetList .
ceq rm((sSPSetList(spset) spsetlist),spset') = rm(spsetlist,spset')
    if (spset' == spset) .
ceq rm((sSPSetList(spset) spsetlist),spset') = (sSPSetList(spset) rm(spsetlist,spset'))
    if (spset' =/= spset) .

op subset : SPSetList SPSetList -> Bool .
eq subset(eSPSetList,spsetlist') = true .
eq subset((sSPSetList(spset) spsetlist), spsetlist') = 
    contains(spsetlist',spset) and subset(spsetlist,spsetlist') .

op ith : SPSetList Nat -> SPSet .
eq ith(sSPSetList(spset) spsetlist, 0) = spset .
eq ith(sSPSetList(spset) spsetlist, (s n)) = ith(spsetlist,n) .

***(
--- more specific functions

op contains : SPSetList Pattern -> Bool .
eq contains(eSPSetList, pattern') = false .
eq contains((sSPSetList(spset) spsetlist), pattern') = 
     (pattern(spset) == pattern') or contains(spsetlist, pattern') .

op  contains : SPSetList Message -> Bool .
eq  contains(eSPSetList, message) = false .
eq  contains((sSPSetList(spset) spsetlist), message) = 
     match(spset,message) or contains(spsetlist, message) .

op  sabundle : SPSetList Message -> SASetList .
ceq sabundle((sSPSetList(spset) spsetlist), message) = 
    sabundle(spset) if match(spset,message) .
ceq sabundle((sSPSetList(spset) spsetlist), message) = 
    sabundle(spsetlist, message) if not(match(spset,message)) .

op  contains : SPSetList Message SASetList -> Bool .
eq  contains(eSPSetList,message,sabundle) = false .
eq  contains((sSPSetList(spset) spsetlist), message, sabundle) = 
     (match(spset,message) and sabundle(spset) == sabundle) or 
     contains(spsetlist,message,sabundle) .
)

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

sort SPList .
op sSPList : SP -> SPList .
op eSPList : -> SPList .
op __ : SPList SPList -> SPList [assoc id: eSPList] .

var splist splist' : SPList .

op contains : SPList SP -> Bool .
eq contains(eSPList, sp') = false .
eq contains((sSPList(sp) splist), sp') = 
     (sp' == sp) or contains(splist, sp') .

op  add : SPList SP -> SPList .
eq  add(splist,sp) = (splist sSPList(sp)) .

op  add' : SPList SP -> SPList .
ceq add'(splist,sp) = splist 
    if contains(splist, sp) .
ceq add'(splist,sp) = (splist sSPList(sp)) 
    if not(contains(splist, sp)) .

op  rm : SPList SP -> SPList .
eq  rm(eSPList,sp) = eSPList .
ceq rm((sSPList(sp) splist),sp') = rm(splist,sp')
    if (sp' == sp) .
ceq rm((sSPList(sp) splist),sp') = (sSPList(sp) rm(splist,sp'))
    if (sp' =/= sp) .

op subset : SPList SPList -> Bool .
eq subset(eSPList,splist') = true .
eq subset((sSPList(sp) splist), splist') = 
    contains(splist',sp) and subset(splist,splist') .

op ith : SPList Nat -> SP .
eq ith(sSPList(sp) splist, 0) = sp .
eq ith(sSPList(sp) splist, (s n)) = ith(splist,n) .

--- more specific functions

op contains : SPList Pattern -> Bool .
eq contains(eSPList, pattern') = false .
eq contains((sSPList(sp) splist), pattern') = 
     (pattern(sp) == pattern') or contains(splist, pattern') .

op  contains : SPList Message -> Bool .
eq  contains(eSPList, message) = false .
eq  contains((sSPList(sp) splist), message) = 
     match(sp,message) or contains(splist, message) .

op  sabundle : SPList Message -> SAList .
ceq sabundle((sSPList(sp) splist), message) = 
    sabundle(sp) if match(sp,message) .
ceq sabundle((sSPList(sp) splist), message) = 
    sabundle(splist, message) if not(match(sp,message)) .

op  contains : SPList Message SAList -> Bool .
eq  contains(eSPList,message,sabundle) = false .
eq  contains((sSPList(sp) splist), message, sabundle) = 
     (match(sp,message) and sabundle(sp) == sabundle) or 
     contains(splist,message,sabundle) .

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

sort State .

--- physical network attributes
op interfaces : Node AddrSet -> State .
op subnet : AddrSet -> State .

var interfaces interfaces' : AddrSet .
var rinterface rinterface' sinterface : Addr .

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

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') .

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

--- ip interface

op ip-send : Node Message -> State .
op ip-received : Node Addr Message -> State .
op ip-delivered : Node Addr Message -> State .

--- ipsec interface 

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

--- ipsec layer attributes
op rootinfo : Node Addr AddrSet -> State .
op routetab : Node RouteList -> State . --- routing table
op sadb : Node SASet -> State . --- security association data base
op spdb : Node SPList SPList -> State . --- security association policy data base

var sadb : SASet .
var spdb spindb spoutdb : SPList .

--- sa/sp db management messages

op addsp-req : Node Addr Addr Addr Addr -> State .
op addsp-req' : Node Addr Addr Addr Addr -> State .
op addsp-ack : Node Addr Addr Addr Addr -> State .

-----

op eState : -> State .
op __ : State State -> State 
        [assoc comm id: eState format (d ni d)] .

------------------------------- IP -------------------------------------

--- node capabilities

op host : Node -> State .  --- node has ip host capabilities 
op gw : Node -> State .    --- node has additionally ip gateway capabilities

var subnet : AddrSet .
var routetab : RouteList .
var nexthop : Addr .

--- outgoing ip traffic 

crl [ip-receive]:
    subnet(subnet)
    ip-send(node, ip(src,dest,message))
    routetab(node,routetab)
    interfaces(node',interfaces') =>
    subnet(subnet)
    routetab(node,routetab)
    interfaces(node',interfaces') 
    ip-received(node',nexthop(routetab,dest),ip(src,dest,message))
    if contains(routetab,dest) and
       contains(interfaces',nexthop(routetab,dest)) and
       contains(subnet,sinterface(routetab,dest)) and 
       contains(subnet,nexthop(routetab,dest)) .

crl [ip-deliver]:
    host(node)
    ip-received(node, rinterface, ip(src,dest,message)) =>
    host(node)
    ip-delivered(node, rinterface, ip(src,dest,message))
    if dest == rinterface .

--- forwarding incoming ip traffic

crl [ip-forward]:
    gw(node)
    ip-received(node, rinterface, ip(src,dest,message)) =>
    gw(node)
    ip-send(node, ip(src,dest,message))
    if dest =/= rinterface .

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

--- 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(node, ip(src,dest,message))
    sadb(node,sadb)
    spdb(node,spindb,spoutdb) =>
    ip-send(node, ipsec(sabundle(spoutdb,ip(src,dest,message)),ip(src,dest,message)))
    sadb(node,sadb)
    spdb(node,spindb,spoutdb)
    if contains(spoutdb,ip(src,dest,message)) and 
       contains(sadb,sabundle(spoutdb,ip(src,dest,message))) .

--- 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

crl [ipsec-forward]:
    sgw(node)
    sadb(node,sadb)
    spdb(node,spindb,spoutdb)
    ipsec-received(node, rinterface, attrs, sabundle, message) =>
    sgw(node)
    sadb(node,sadb)
    spdb(node,spindb,spoutdb)
    ipsec-send(node, 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) .

--- 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)) .

------- security association and policy management

op  overwrite : SPList Pattern SAList -> SPList .
eq  overwrite(eSPList, pattern', sabundle') = 
    sSPList(sp(pattern',sabundle')) .
ceq overwrite((sSPList(sp(pattern,sabundle)) splist),pattern',sabundle') = 
    (sSPList(sp(pattern,sabundle')) splist)
    if pattern == pattern' .
ceq overwrite((sSPList(sp(pattern,sabundle)) splist),pattern',sabundle') = 
    (sSPList(sp(pattern,sabundle)) overwrite(splist,pattern',sabundle'))
    if pattern =/= pattern' .

op  extend' : SPList Pattern SA -> SPList .
eq  extend'(eSPList, pattern', sa') = eSPList .
ceq extend'((sSPList(sp(pattern,sabundle)) splist),pattern',sa') = 
    (sSPList(sp(pattern,(sSAList(sa') sabundle))) splist)
    if  pattern == pattern' and not(contains(sabundle,sa')) .
ceq extend'((sSPList(sp(pattern,sabundle)) splist),pattern',sa') = 
    (sSPList(sp(pattern,sabundle)) splist)
    if  pattern == pattern' and contains(sabundle,sa') .
ceq extend'((sSPList(sp(pattern,sabundle)) splist),pattern',sa') = 
    (sSPList(sp(pattern,sabundle)) extend(splist,pattern',sa'))
    if  pattern =/= pattern' .

op  extend : SPList Pattern SA -> SPList .
ceq extend(splist, pattern', sa') =
    extend'(splist, pattern', sa')
    if contains(splist,pattern') .
ceq extend(splist, pattern', sa') =
    (sSPList(sp(pattern',sSAList(sa'))) splist)
    if not(contains(splist,pattern')) .

crl [addsp-req-responder]:
    sadb(node,sadb)
    spdb(node,spindb,spoutdb)
    interfaces(node,interfaces)
    addsp-req(node', initiator, responder, client, server) =>
    sadb(node, add'(sadb,sa(initiator,responder,0)))
    spdb(node, add'(spindb,sp(towards(server),sSAList(sa(initiator,responder,0)))), spoutdb)
    interfaces(node,interfaces)
    addsp-req'(node', initiator, responder, client, server)
    if contains(interfaces,responder) .

crl [addsp-req-inititator]:
    sadb(node,sadb)
    spdb(node, spindb,spoutdb)
    interfaces(node,interfaces)
    addsp-req'(node', initiator, responder, client, server) =>
    sadb(node, add'(sadb,sa(initiator,responder,0)))
    spdb(node, spindb, extend(spoutdb,towards(server),sa(initiator,responder,0)))
    interfaces(node,interfaces)
    addsp-ack(node', initiator, responder, client, server) 
    if contains(interfaces,initiator) .


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

--- running sectrace application and its state

op sectrace-start : Node Addr Addr -> State .
op sectrace-rreq : Node Addr Addr MessageList MessageList -> State .
op sectrace-rrep1 : Node Addr Addr Addr Addr MessageList MessageList -> State .
op sectrace-rrep2 : Node Addr Addr Addr Addr MessageList MessageList -> State .
op sectrace-rrep3 : Node Addr Addr MessageList MessageList -> State .
op sectrace-sareq : Node Addr Addr MessageList MessageList -> State .
op sectrace-terminated : Node Addr Addr -> State .
op sectrace-failed : Node Addr Addr -> State .

--- running sectrace deamon and its states

op sectraced : Node -> State .
op sectraced-sareq : Node Addr Addr Addr Addr Addr -> State .

--- selection algorithm (selects sa initiator)

var myroot : Addr .
var mytrustedroots : AddrSet .
var fs fs' : AddrPairSet .
var path resplist resplist' : AddrList .

op  path : MessageList -> AddrList .
eq  path(eMessageList) = eAddrList .
ceq path(sMessageList(message) messagelist) = sAddrList(src(message)) path(messagelist) 
    if rrep(message) .
ceq path(sMessageList(message) messagelist) = path(messagelist)
    if not(rrep(message)) .

op  trustedroots : MessageList Addr -> AddrSet .
eq  trustedroots(eMessageList, addr) = eAddrSet .
ceq trustedroots(sMessageList(message) messagelist, addr) = trustedroots(message)
    if rrep(message) and src(message) == addr .
ceq trustedroots(sMessageList(message) messagelist, addr) = trustedroots(messagelist,addr)
    if rrep(message) and src(message) =/= addr .
ceq trustedroots(sMessageList(message) messagelist, addr) = trustedroots(messagelist,addr)
    if not(rrep(message)) .

op  root : Addr Addr MessageList Addr -> Addr .
ceq root(client,root,messagelist,addr) = root
    if addr == client .
ceq root(client,root,sMessageList(message) messagelist, addr) = root(message)
    if rrep(message) /\ addr =/= client /\ src(message) == addr .
ceq root(client,root,sMessageList(message) messagelist, addr) = root(client,root,messagelist,addr)
    if rrep(message) /\ addr =/= client /\ src(message) =/= addr .
ceq root(client,root,sMessageList(message) messagelist, addr) = root(client,root,messagelist,addr)
    if sarep(message) .

op  lt : AddrList Addr Addr -> Bool .
eq  lt(eAddrList,addr',addr'') = false .
ceq lt((sAddrList(addr) addrlist),addr',addr'') = lt(addrlist,addr',addr'') 
    if addr =/= addr' .
ceq lt((sAddrList(addr) addrlist),addr',addr'') = contains(addrlist,addr'')
    if addr == addr' .

op  trustedby : Addr Addr MessageList Addr Addr -> Bool .
eq  trustedby(client,root,rreplist,addr,addr') = 
    contains(trustedroots(rreplist,addr'),root(client,root,rreplist,addr)) .

op  trusted : Addr Addr MessageList AddrPairSet Addr -> Bool .
eq  trusted(client,root,rreplist,fs,responder) = 
    trustedby(client,root,rreplist,lookup(fs,responder),responder) .

op  trusted : Addr Addr MessageList AddrPairSet AddrList -> Bool .
eq  trusted(client,root,rreplist,fs, eAddrList) = true .
eq  trusted(client,root,rreplist,fs, (sAddrList(responder) addrlist')) =
    trusted(client,root,rreplist,fs,responder) and 
    trusted(client,root,rreplist,fs,addrlist') .

op  encapsulated : Addr Addr MessageList AddrPairSet Addr Addr -> Bool .
eq  encapsulated(client,root,rreplist,fs,responder,responder') = 
    lt(path(rreplist),responder,responder') implies
      (trustedby(client,root,rreplist,lookup(fs,responder),lookup(fs,responder')) or
       trustedby(client,root,rreplist,responder,lookup(fs,responder'))) .

op  encapsulated : Addr Addr MessageList AddrPairSet AddrList AddrList -> Bool .
eq  encapsulated(client,root,rreplist,fs,resplist,eAddrList) = true .
eq  encapsulated(client,root,rreplist,fs,eAddrList,resplist') = true .
eq  encapsulated(client,root,rreplist,fs,eAddrList,(sAddrList(responder') resplist')) = 
    encapsulated(client,root,rreplist,fs,path(rreplist),resplist') .
eq  encapsulated(client,root,rreplist,fs,(sAddrList(responder) resplist),(sAddrList(responder') resplist')) = 
    encapsulated(client,root,rreplist,fs,responder,responder') and
    encapsulated(client,root,rreplist,fs,resplist,(sAddrList(responder') resplist')) .

op  encapsulated : Addr Addr MessageList AddrPairSet AddrList -> Bool .
eq  encapsulated(client,root,rreplist,fs,addrlist) = 
    encapsulated(client,root,rreplist,fs,addrlist,addrlist) .

op  trustedencapsulation : Addr Addr MessageList AddrPairSet AddrList -> Bool .
eq  trustedencapsulation(client,root,rreplist,fs,addrlist) =
    trusted(client,root,rreplist,fs,addrlist) and 
    encapsulated(client,root,rreplist,fs,addrlist) .

op  fs : Addr Addr MessageList AddrList AddrList -> AddrPairSet .
eq  fs(client,root,rreplist,addrlist,eAddrList) = eAddrPairSet .
ceq fs(client,root,rreplist,(addrlist sAddrList(responder)),(addrlist' sAddrList(initiator))) =
      if trustedencapsulation(client,root,rreplist,fs',(addrlist sAddrList(responder))) then fs'
      else fs(client,root,rreplist,(addrlist sAddrList(responder)),addrlist') fi
    if fs' := (fs(client,root,rreplist,addrlist) sAddrPairSet((responder,initiator))) .

op  fs : Addr Addr MessageList AddrList -> AddrPairSet .
eq  fs(client,root,rreplist,eAddrList) = eAddrPairSet .
eq  fs(client,root,rreplist,(addrlist sAddrList(responder))) =
    fs(client,root,rreplist,(addrlist sAddrList(responder)),(sAddrList(client) addrlist)) .

op  select : Addr Addr MessageList Addr ~> Addr .
eq  select(client,root,rreplist,responder) =
    lookup(fs(client,root,rreplist,path(rreplist)),responder) .

--- client actions

--- client initiates protocol (sends rreq)

rl  [sectrace-start]:
    sectrace-start(node,client,server) =>
    sectrace-rreq(node,client,server,sMessageList(rreq(client,server)),eMessageList)
    ipsec-send(node,ip(client,server,rreq(client,server))) .

var rreplist newrreplist : MessageList .

--- client receives rrep (server is the responder and done = true)

crl [sectrace-rrep-0]:
    sectrace-rreq(node,client,server,sMessageList(rreq(client,server)),rreplist)
    rootinfo(node,myroot,mytrustedroots)
    ipsec-delivered(node,rinterface,attrs,sabundle,message) =>
    sectrace-terminated(node,client,server)
    rootinfo(node,myroot,mytrustedroots)
    if not(contains(rreplist,message)) /\
       ip(responder,dest,rrep(client,server,root,trustedroots,done)) := message /\
       done == true /\
       responder == server .

--- client receives rrep (selected initiator is client itself and server is the responder and done = false)

crl [sectrace-rrep-1]:
    sectrace-rreq(node,client,server,sMessageList(rreq(client,server)),rreplist)
    rootinfo(node,myroot,mytrustedroots)
    ipsec-delivered(node,rinterface,attrs,sabundle,message) =>
    sectrace-rrep1(node,initiator,responder,client,server,sMessageList(rreq(client,server)),(rreplist sMessageList(message)))
    rootinfo(node,myroot,mytrustedroots)
    addsp-req(node,initiator,responder,client,server)
    if not(contains(rreplist,message)) /\
       ip(responder,dest,rrep(client,server,root,trustedroots,done)) := message /\
       done == false /\
       initiator := select(client,myroot,(rreplist sMessageList(message)),responder) /\
       initiator == client and responder == server .

rl  [sectrace-rrep-1']:
    sectrace-rrep1(node,initiator,responder,client,server,sMessageList(rreq(client,server)),rreplist) 
    addsp-ack(node,initiator,responder,client,server) =>
    sectrace-terminated(node,client,server) .

--- client receives rrep (selected initiator is client itself and server is not the responder)

crl [sectrace-rrep-2]:
    sectrace-rreq(node,client,server,sMessageList(rreq(client,server)),rreplist)
    rootinfo(node,myroot,mytrustedroots)
    ipsec-delivered(node,rinterface,attrs,sabundle,message) =>
    sectrace-rrep2(node,initiator,responder,client,server,sMessageList(rreq(client,server)),(rreplist sMessageList(message)))
    rootinfo(node,myroot,mytrustedroots)
    addsp-req(node,initiator,responder,client,server)
    if not(contains(rreplist,message)) /\
       ip(responder,dest,rrep(client,server,root,trustedroots,done)) := message /\
       done == false /\
       initiator := select(client,myroot,(rreplist sMessageList(message)),responder) /\
       initiator == client /\ responder =/= server .
       
crl [sectrace-rrep-2']:
    sectrace-rrep2(node,initiator,responder,client,server,sMessageList(rreq(client,server)),(rreplist sMessageList(message)))
    addsp-ack(node,initiator,responder,client,server) =>
    sectrace-rreq(node,client,server,sMessageList(rreq(client,server)),(rreplist sMessageList(message)))
    ipsec-send(node,message')
    if message' := ip(client,server,rreq(client,server)) .

--- client receives rrep (selected initiator is not the client)

crl [sectrace-rrep-3]:
    sectrace-rreq(node,client,server,sMessageList(rreq(client,server)),rreplist)
    rootinfo(node,myroot,mytrustedroots)
    ipsec-delivered(node,rinterface,attrs,sabundle,message) =>
    sectrace-rrep3(node,client,server,sMessageList(sareq(client,server,initiator,responder)),(rreplist sMessageList(message)))
    rootinfo(node,myroot,mytrustedroots)
    if not(contains(rreplist,message)) /\
       ip(responder,dest,rrep(client,server,root,trustedroots,done)) := message /\
       done == false /\
       initiator := select(client,myroot,(rreplist sMessageList(message)),responder) /\
       initiator =/= client .

crl [sectrace-rrep-3']:
    sectrace-rrep3(node,client,server,sMessageList(sareq(client,server,initiator,responder)),(rreplist sMessageList(message)))
    rootinfo(node,myroot,mytrustedroots) =>
    sectrace-sareq(node,client,server,sMessageList(sareq(client,server,initiator,responder)),(rreplist sMessageList(message)))
    rootinfo(node,myroot,mytrustedroots)
    ipsec-send(node,message')
    if message' := ip(client,initiator,sareq(client,server,initiator,responder)) .

--- client receives sarep (with done = true and responder is the server)

crl [sectrace-sarep-0]:
    sectrace-sareq(node,client,server,sMessageList(sareq(client,server,initiator,responder)),rreplist)
    ipsec-delivered(node,rinterface,attrs,sabundle,message) =>
    sectrace-terminated(node,client,server)
    if not(contains(rreplist,message)) /\
       ip(src,dest,sarep(client,server,initiator,responder,done)) := message /\
       done == true and responder == server .

--- client receives sarep (with done = true and responder is not the server)

crl [sectrace-sarep-1]:
    sectrace-sareq(node,client,server,sMessageList(sareq(client,server,initiator,responder)),rreplist)
    ipsec-delivered(node,rinterface,attrs,sabundle,message) =>
    sectrace-rreq(node,client,server,sMessageList(rreq(client,server)),(rreplist sMessageList(message)))
    ipsec-send(node,ip(client,server,rreq(client,server)))
    if not(contains(rreplist,message)) /\
       ip(src,dest,sarep(client,server,initiator,responder,done)) := message /\
       done == true and responder =/= server .

--- client receives sarep (with done = false)

crl [sectrace-sarep-2]:
    sectrace-sareq(node,client,server,sMessageList(sareq(client,server,initiator,responder)),rreplist)
    ipsec-delivered(node,rinterface,attrs,sabundle,message) =>
    sectrace-failed(node,client,server)
    if not(contains(rreplist,message)) /\
       ip(src,dest,sarep(client,server,initiator,responder,done)) := message /\
       done == false .

--- security gateway actions (server acts as security gateway)

--- security gateway receives unauthenticated rreq (send rrep)

crl [sectraced-receive-unauth-rreq]:
    shost(node)
    sectraced(node)
    rootinfo(node,myroot,mytrustedroots)
    ipsec-delivered(node,rinterface,attrs,sabundle,message) =>
    shost(node)
    sectraced(node)
    rootinfo(node,myroot,mytrustedroots)
    ipsec-send(node,message')
    if contains(attrs,discard) /\
       ip(src,dest,rreq(client,server)) := message /\ 
       message' := ip(rinterface,src,rrep(client,server,myroot,mytrustedroots,false)) .


--- security gateway receives unauthenticated rrep (forward it)

crl [sectraced-forward-unauth-rrep]:
    sgw(node)
    sectraced(node)
    ipsec-delivered(node,rinterface,attrs,sabundle,message) =>
    sgw(node)
    sectraced(node)
    ipsec-send(node,message)
    if contains(attrs,discard) /\
       ip(src,dest,rrep(client,server,root,trustedroots,done)) := message /\
       dest =/= rinterface .

--- security gateway receives unauthenticated sarep (forward it)
				   
crl [sectraced-forward-unauth-sarep]:
    sgw(node)
    sectraced(node)
    ipsec-delivered(node,rinterface,attrs,sabundle,message) =>
    sgw(node)
    sectraced(node)
    ipsec-send(node,message)
    if ip(src,dest,sarep(client,server,initiator,responder,done)) := message /\
       dest =/= rinterface .

--- security gateway receives authenticated sareq for itself (process and send sarep)

crl [sectraced-receive-auth-sareq]:
    sgw(node)
    sectraced(node)
    ipsec-delivered(node,rinterface,attrs,sabundle,message) =>
    sgw(node)
    sectraced-sareq(node,rinterface,client,server,initiator,responder)
    addsp-req(node,initiator,responder,client,server)
    if not(contains(attrs,discard)) /\
       ip(src,dest,sareq(client,server,initiator,responder)) := message .

crl [sectraced-receive-sareq']:
    sectraced-sareq(node,rinterface,client,server,initiator,responder)
    addsp-ack(node,initiator,responder,client,server) =>
    sectraced(node)
    ipsec-send(node,message')
    if message' := ip(rinterface,client,sarep(client,server,initiator,responder,true)) .

--- server only actions

--- server receives authenticated rreq (as for sg)

crl [sectraced-receive-auth-rreq]:
    shost(node)
    sectraced(node)
    interfaces(node,interfaces)
    rootinfo(node,myroot,mytrustedroots)
    ipsec-delivered(node,rinterface,attrs,sabundle,message) =>
    shost(node)
    sectraced(node)
    interfaces(node,interfaces)
    rootinfo(node,myroot,mytrustedroots)
    ipsec-send(node,message')
    if not(contains(attrs,discard)) /\ 
       ip(src,dest,rreq(client,server)) := message /\
       contains(interfaces,server) /\
       message' := ip(rinterface,src,rrep(client,server,myroot,mytrustedroots,true)) .
              
endm