begin_problem(Unknown). list_of_descriptions. name({* Network Infrastructure *}). author({*Carsten Karl*}). status(satisfiable). description({* Layer 2/3 Networking plus Statefull Firewall CNF generated by FLOTTER V 3.1 *}). end_of_list. list_of_symbols. functions[(0, 0), (1, 0), (ip, 32), (land, 2), (ipand, 2), (null, 0), (one, 0), (tcp, 0), (udp, 0), (syn, 0), (synack, 0), (no_syn, 0), (fin, 0), (finack, 0), (ack, 0), (epacket, 5), (ippacket, 4), (tcppacket, 4), (udppacket, 3), (interface, 5), (recv_ip_packet, 3), (send_ip_packet, 3), (route_ip_packet, 2), (recv_udp_packet, 5), (send_udp_packet, 5), (broadcastmac, 0), (broadcastip, 0), (networkip, 0), (mask32, 0), (mask24, 0), (mask16, 0), (mask8, 0), (mask0, 0), (forwarded, 10), (udp_incoming, 4), (e_ip, 0), (tcp_clientsynsent, 5), (tcp_serversynacksent, 5), (tcp_clientacksent, 5), (tcp_connection_open, 5), (tcp_connection_halfclosed, 5), (tcp_connection_closed, 5), (permit, 0), (deny, 0), (first_rule, 0), (next_rule, 1), (any, 0), (tcp_not_matched, 19), (udp_matched, 18), (denied, 10), (tcp_fwrule, 9), (udp_fwrule, 9), (udp_connection_open, 5), (firewall, 3), (route, 5), (first_route, 0), (next_route, 1), (not_forwarded, 2), (nomatch, 0), (related_conn, 4), (ftp_start_state, 5), (ftp_active_port_request, 6), (ftp_active_port, 6), (ftp_passive_mode_request, 5), (ftp_passive_mode, 5), (ftpServerPort, 3), (ftp_port_cmd, 2), (ftp_cmd_pasv, 0), (ftp_control_data, 1), (code200, 0), (ftp_reply, 1), (ftp_error, 0), (ftp_quit, 0), (ftp_closed, 5), (ftp_pasv_ok, 2), (dataport, 0), (arpEntry, 3), (local, 0), (port67, 0), (port68, 0), (c1port, 0), (s1port, 0), (c1_mac, 0), (rl1_mac, 0), (s1_mac, 0), (r1_mac, 0), (c2_mac, 0), (net1, 0), (net2, 0), (net3, 0), (con1, 0), (fw1, 0), (s1, 0), (c1, 0), (c2, 0), (rl1, 0), (r1, 0), (c1_ip, 0), (s1_ip, 0), (rl1_ip, 0), (r1_ip, 0), (c2_ip, 0), (c1_id, 0), (c2_id, 0), (net1_addr, 0), (net2_addr, 0), (net3_addr, 0), (c_class, 0), (r1_ip_net1, 0), (r1_mac_net1, 0), (r1_ip_net2, 0), (r1_mac_net2, 0), (r2_ip_net2, 0), (r2_mac_net2, 0), (r2_ip_net3, 0), (r2_mac_net3, 0), (deniedport, 0), (dns, 0)]. predicates[(ArpTable, 1), (Sent, 1), (Network, 1), (Router, 1), (Firewall, 1), (Interface, 1), (RouteEntry, 1), (Relayagententry, 1), (Hostentry, 1), (DhcpServer, 1), (DhcpClient, 1), (Relayagent, 1), (Bit, 1), (ReceivedIPPacket, 1), (SendIPPacket, 1), (RouteIPPacket, 1), (Forwarded, 1), (NotForwarded, 1), (SendUDPPacket, 1), (ReceivedUDPPacket, 1), (TCP_FirewallRule, 1), (TCP_ClientSynSent, 1), (TCP_ServerSynAckSent, 1), (TCP_ClientAckSent, 1), (TCP_Connection_Open, 1), (TCP_Connection_HalfClosed, 1), (TCP_Connection_Closed, 1), (TCP_NotMatched, 1), (Denied, 1), (UDP_FirewallRule, 1), (UDP_ConnectionOpen, 1), (UDP_NotMatched, 1), (FtpServerPort, 1), (Ftp_Start, 1), (FtpActivePortRequest, 1), (FtpActivePort, 1), (FtpClosed, 1), (FtpPassiveModeRequest, 1), (FtpPassiveMode, 1)]. end_of_list. list_of_clauses(axioms, cnf). clause( || -> Router(r1),1). clause( || -> Network(net2),2). clause( || -> Network(con1),3). clause( || -> Network(net1),4). clause( || -> Bit(0),5). clause( || -> Bit(1),6). clause( || equal(broadcastip,local) -> ,7). clause( || equal(broadcastip,any) -> ,8). clause( || equal(networkip,broadcastip) -> ,9). clause( || equal(0,1) -> ,10). clause( || -> Firewall(firewall(fw1,net1,con1)),11). clause( || -> Firewall(firewall(fw1,con1,net1)),12). clause( || -> ArpTable(arpEntry(s1,s1_mac,s1_ip)),13). clause( || -> ArpTable(arpEntry(c2,r1_mac_net2,r1_ip_net2)),14). clause( || -> ArpTable(arpEntry(c1,rl1_mac,rl1_ip)),15). clause( || -> ArpTable(arpEntry(c1,r1_mac_net1,r1_ip_net1)),16). clause( || -> ArpTable(arpEntry(rl1,c1_mac,c1_ip)),17). clause( || -> ArpTable(arpEntry(rl1,r1_mac_net1,r1_ip_net1)),18). clause( || -> ArpTable(arpEntry(s1,c2_mac,c2_ip)),19). clause( || -> ArpTable(arpEntry(s1,r1_mac_net2,r1_ip_net2)),20). clause( || -> ArpTable(arpEntry(r1,rl1_mac,rl1_ip)),21). clause( || -> ArpTable(arpEntry(r1,c1_mac,c1_ip)),22). clause( || -> ArpTable(arpEntry(r1,s1_mac,s1_ip)),23). clause( || -> RouteEntry(route(c2,c_class,net2_addr,local,first_route)),24). clause( || -> RouteEntry(route(c1,c_class,net1_addr,local,first_route)),25). clause( || -> RouteEntry(route(s1,c_class,net2_addr,local,first_route)),26). clause( || -> RouteEntry(route(rl1,c_class,net1_addr,local,first_route)),27). clause( || -> RouteEntry(route(r1,c_class,net1_addr,local,first_route)),28). clause( || -> Interface(interface(r1,r1_ip_net2,c_class,r1_mac_net2,net2)),29). clause( || -> Interface(interface(r1,r1_ip_net1,c_class,r1_mac_net1,con1)),30). clause( || -> RouteEntry(route(c2,mask0,mask0,r1_ip_net2,next_route(first_route))),31). clause( || -> RouteEntry(route(c1,mask0,mask0,r1_ip_net1,next_route(first_route))),32). clause( || -> RouteEntry(route(s1,mask0,mask0,r1_ip_net2,next_route(first_route))),33). clause( || -> RouteEntry(route(rl1,mask0,mask0,r1_ip_net1,next_route(first_route))),34). clause( || -> RouteEntry(route(r1,c_class,net2_addr,local,next_route(first_route))),35). clause( || Bit(U) -> equal(land(U,1),U),36). clause( || Bit(U) -> equal(land(1,U),U),37). clause( || Bit(U) -> equal(land(U,0),0),38). clause( || Bit(U) -> equal(land(0,U),0),39). clause( || -> UDP_FirewallRule(udp_fwrule(fw1,first_rule,permit,any,any,any,any,port67,port67)),40). clause( || -> TCP_FirewallRule(tcp_fwrule(fw1,first_rule,deny,net2_addr,c_class,net2_addr,c_class,c1port,s1port)),41). clause( || -> UDP_FirewallRule(udp_fwrule(fw1,next_rule(first_rule),permit,any,any,any,any,port67,port68)),42). clause( || -> TCP_FirewallRule(tcp_fwrule(fw1,next_rule(first_rule),permit,any,any,any,any,c1port,s1port)),43). clause( || -> UDP_FirewallRule(udp_fwrule(fw1,next_rule(next_rule(first_rule)),permit,any,any,any,any,port68,port67)),44). clause( || Bit(U) equal(land(V,U),1) Bit(V) -> equal(V,1),45). clause( || Bit(U) equal(land(V,U),1) Bit(V) -> equal(U,1),46). clause( || Bit(U) Bit(V) -> equal(land(V,U),0) equal(land(V,U),1),47). clause( || Bit(U) equal(land(V,U),0) Bit(V) -> equal(U,0) equal(V,0),48). clause( || Relayagent(U) SendUDPPacket(send_udp_packet(V,U,W,X,Y)) -> RouteIPPacket(route_ip_packet(U,ippacket(W,X,udp,Y))),49). clause( || DhcpClient(U) SendUDPPacket(send_udp_packet(V,U,W,X,Y)) -> RouteIPPacket(route_ip_packet(U,ippacket(W,X,udp,Y))),50). clause( || DhcpServer(U) SendUDPPacket(send_udp_packet(V,U,W,X,Y)) -> RouteIPPacket(route_ip_packet(U,ippacket(W,X,udp,Y))),51). clause( || Router(U) ReceivedIPPacket(recv_ip_packet(V,U,ippacket(W,X,Y,Z))) -> RouteIPPacket(route_ip_packet(U,ippacket(W,X,Y,Z))),52). clause( || Network(U) Interface(interface(V,W,X,Y,U)) Sent(epacket(U,Y,Z,e_ip,X1)) -> ReceivedIPPacket(recv_ip_packet(U,V,X1)),53). clause( || Network(U) Sent(epacket(U,broadcastmac,V,e_ip,W)) Interface(interface(X,Y,Z,X1,U)) -> ReceivedIPPacket(recv_ip_packet(U,X,W)),54). clause( || DhcpServer(U) Interface(interface(U,V,W,X,Y)) ReceivedIPPacket(recv_ip_packet(Y,U,ippacket(Z,V,udp,X1))) -> ReceivedUDPPacket(recv_udp_packet(Y,U,Z,V,X1)),55). clause( || DhcpClient(U) Interface(interface(U,V,W,X,Y)) ReceivedIPPacket(recv_ip_packet(Y,U,ippacket(Z,V,udp,X1))) -> ReceivedUDPPacket(recv_udp_packet(Y,U,Z,V,X1)),56). clause( || Relayagent(U) Interface(interface(U,V,W,X,Y)) ReceivedIPPacket(recv_ip_packet(Y,U,ippacket(Z,V,udp,X1))) -> ReceivedUDPPacket(recv_udp_packet(Y,U,Z,V,X1)),57). clause( || DhcpServer(U) ReceivedIPPacket(recv_ip_packet(V,U,ippacket(W,broadcastip,udp,X))) Interface(interface(U,Y,Z,X1,V)) -> ReceivedUDPPacket(recv_udp_packet(V,U,W,broadcastip,X)),58). clause( || DhcpClient(U) ReceivedIPPacket(recv_ip_packet(V,U,ippacket(W,broadcastip,udp,X))) Interface(interface(U,Y,Z,X1,V)) -> ReceivedUDPPacket(recv_udp_packet(V,U,W,broadcastip,X)),59). clause( || Relayagent(U) ReceivedIPPacket(recv_ip_packet(V,U,ippacket(W,broadcastip,udp,X))) Interface(interface(U,Y,Z,X1,V)) -> ReceivedUDPPacket(recv_udp_packet(V,U,W,broadcastip,X)),60). clause( || RouteIPPacket(route_ip_packet(U,ippacket(V,broadcastip,udp,W))) DhcpServer(U) Interface(interface(U,V,X,Y,Z)) -> Sent(epacket(Z,broadcastmac,Y,e_ip,ippacket(V,broadcastip,udp,W))),61). clause( || RouteIPPacket(route_ip_packet(U,ippacket(V,broadcastip,udp,W))) DhcpClient(U) Interface(interface(U,V,X,Y,Z)) -> Sent(epacket(Z,broadcastmac,Y,e_ip,ippacket(V,broadcastip,udp,W))),62). clause( || RouteIPPacket(route_ip_packet(U,ippacket(V,broadcastip,udp,W))) Relayagent(U) Interface(interface(U,V,X,Y,Z)) -> Sent(epacket(Z,broadcastmac,Y,e_ip,ippacket(V,broadcastip,udp,W))),63). clause( || Relayagent(U) RouteIPPacket(route_ip_packet(U,ippacket(networkip,broadcastip,udp,V))) Interface(interface(U,W,X,Y,Z)) -> Sent(epacket(Z,broadcastmac,Y,e_ip,ippacket(networkip,broadcastip,udp,V))),64). clause( || DhcpClient(U) RouteIPPacket(route_ip_packet(U,ippacket(networkip,broadcastip,udp,V))) Interface(interface(U,W,X,Y,Z)) -> Sent(epacket(Z,broadcastmac,Y,e_ip,ippacket(networkip,broadcastip,udp,V))),65). clause( || DhcpServer(U) RouteIPPacket(route_ip_packet(U,ippacket(networkip,broadcastip,udp,V))) Interface(interface(U,W,X,Y,Z)) -> Sent(epacket(Z,broadcastmac,Y,e_ip,ippacket(networkip,broadcastip,udp,V))),66). clause( || -> equal(ip(0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0),any),67). clause( || -> equal(ip(0,0,0,0,1,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0),net1_addr),68). clause( || -> equal(ip(0,0,0,0,1,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0),net2_addr),69). clause( || -> equal(ip(0,0,0,0,1,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,1,0),s1_ip),70). clause( || -> equal(ip(0,0,0,0,1,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,1,0),rl1_ip),71). clause( || -> equal(ip(0,0,0,0,1,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,1),c1_ip),72). clause( || -> equal(ip(0,0,0,0,1,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,1),c2_ip),73). clause( || -> equal(ip(0,0,0,0,1,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,1,1,0),r1_ip_net1),74). clause( || -> equal(ip(0,0,0,0,1,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,1,1,1,1,1,1,1,0),r1_ip_net2),75). clause( || -> equal(ip(1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,0,0,0,0),c_class),76). clause( || -> equal(ip(1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1),mask32),77). clause( || -> equal(ip(1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1),broadcastip),78). clause( || -> equal(ip(1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,0,0,0,0),mask24),79). clause( || -> equal(ip(1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0),mask16),80). clause( || -> equal(ip(1,1,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0),mask8),81). clause( || -> equal(ip(0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0),mask0),82). clause( || -> equal(ip(0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0),local),83). clause( || -> equal(ip(0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0),networkip),84). clause( || equal(ipand(U,V),ipand(W,V)) Network(X) ArpTable(arpEntry(Y,Z,W)) Interface(interface(Y,U,V,X1,X)) SendIPPacket(send_ip_packet(Y,W,X2)) -> Sent(epacket(X,Z,X1,e_ip,X2)),85). clause( || Interface(interface(U,V,W,X,Y)) RouteIPPacket(route_ip_packet(U,ippacket(Z,X1,X2,X3))) RouteEntry(route(U,X4,X5,X6,first_rule)) -> equal(ipand(X1,X4),X5) NotForwarded(not_forwarded(ippacket(Z,X1,X2,X3),first_rule)),86). clause( || Network(U) Network(V) Sent(epacket(V,W,X,e_ip,ippacket(Y,Z,tcp,tcppacket(X1,X2,synack,X3)))) Firewall(firewall(X4,V,U)) TCP_ClientSynSent(tcp_clientsynsent(X4,Z,Y,X2,X1)) -> TCP_ServerSynAckSent(tcp_connection_open(X4,Z,Y,X2,X1)),87). clause( || Network(U) Network(V) Sent(epacket(V,W,X,e_ip,ippacket(Y,Z,tcp,tcppacket(X1,X2,ack,X3)))) TCP_ClientSynSent(tcp_clientsynsent(X4,Z,Y,X2,X1)) Firewall(firewall(X4,V,U)) -> TCP_Connection_Open(tcp_connection_open(X4,Z,Y,X2,X1)),88). clause( || Network(U) Network(V) Sent(epacket(V,W,X,e_ip,ippacket(Y,Z,tcp,tcppacket(X1,X2,fin,X3)))) TCP_Connection_Open(tcp_connection_open(X4,Y,Z,X1,X2)) Firewall(firewall(X4,V,U)) -> TCP_Connection_HalfClosed(tcp_connection_halfclosed(X4,Y,Z,X1,X2)),89). clause( || Network(U) Network(V) Sent(epacket(V,W,X,e_ip,ippacket(Y,Z,tcp,tcppacket(X1,X2,fin,X3)))) TCP_Connection_Open(tcp_connection_open(X4,Z,Y,X1,X2)) Firewall(firewall(X4,V,U)) -> TCP_Connection_HalfClosed(tcp_connection_halfclosed(X4,Z,Y,X1,X2)),90). clause( || Network(U) Network(V) Sent(epacket(V,W,X,e_ip,ippacket(Y,Z,tcp,tcppacket(X1,X2,finack,X3)))) TCP_Connection_HalfClosed(tcp_connection_halfclosed(X4,Y,Z,X1,X2)) Firewall(firewall(X4,V,U)) -> TCP_Connection_Closed(tcp_connection_closed(X4,Y,Z,X1,X2)),91). clause( || equal(ipand(U,V),W) equal(ipand(X,Y),ipand(Z,Y)) RouteEntry(route(X1,V,W,Z,first_route)) RouteIPPacket(route_ip_packet(X1,ippacket(X2,U,X3,X4))) Interface(interface(X1,X,Y,X5,X6)) -> SendIPPacket(send_ip_packet(X1,Z,ippacket(X2,U,X3,X4))),92). clause( || equal(ipand(U,V),W) equal(ipand(X,Y),ipand(U,Y)) Interface(interface(Z,X,Y,X1,X2)) RouteEntry(route(Z,V,W,local,first_route)) RouteIPPacket(route_ip_packet(Z,ippacket(X3,U,X4,X5))) -> SendIPPacket(send_ip_packet(Z,U,ippacket(X3,U,X4,X5))),93). clause( || NotForwarded(not_forwarded(ippacket(U,V,W,X),Y)) Interface(interface(Z,X1,X2,X3,X4)) RouteIPPacket(route_ip_packet(Z,ippacket(U,V,W,X))) RouteEntry(route(Z,X5,X6,X7,next_rule(Y))) -> equal(ipand(V,X5),X6) NotForwarded(not_forwarded(ippacket(U,V,W,X),next_rule(Y))),94). clause( || Network(U) Network(V) FtpServerPort(ftpServerPort(W,X,Y)) TCP_ClientAckSent(tcp_clientacksent(W,Z,X,X1,Y)) Firewall(firewall(W,V,U)) Sent(epacket(V,X2,X3,e_ip,ippacket(X,Z,tcp,tcppacket(Y,X1,ack,X4)))) -> Ftp_Start(ftp_start_state(W,Z,X,X1,Y)),95). clause( || Network(U) Sent(epacket(V,W,X,e_ip,ippacket(Y,Z,udp,udppacket(X1,X2,X3)))) Network(V) UDP_ConnectionOpen(udp_connection_open(X4,Z,Y,X2,X1)) Firewall(firewall(X4,V,U)) -> Sent(epacket(U,W,X,e_ip,ippacket(Y,Z,udp,udppacket(X1,X2,X3)))),96). clause( || Network(U) Network(V) Sent(epacket(V,W,X,e_ip,ippacket(Y,Z,tcp,tcppacket(X1,X2,synack,X3)))) Firewall(firewall(X4,V,U)) TCP_ClientSynSent(tcp_clientsynsent(X4,Z,Y,X2,X1)) -> Sent(epacket(U,W,X,e_ip,ippacket(Y,Z,tcp,tcppacket(X1,X2,X5,X3)))),97). clause( || Network(U) Network(V) Sent(epacket(V,W,X,e_ip,ippacket(Y,Z,tcp,tcppacket(X1,X2,ack,X3)))) TCP_ClientSynSent(tcp_clientsynsent(X4,Z,Y,X2,X1)) Firewall(firewall(X4,V,U)) -> Sent(epacket(U,W,X,e_ip,ippacket(Y,Z,tcp,tcppacket(X1,X2,ack,X3)))),98). clause( || Network(U) Sent(epacket(V,W,X,e_ip,ippacket(Y,Z,tcp,tcppacket(X1,X2,no_syn,X3)))) Network(V) TCP_Connection_Open(tcp_connection_open(X4,Y,Z,X1,X2)) Firewall(firewall(X4,V,U)) -> Sent(epacket(U,W,X,e_ip,ippacket(Y,Z,tcp,tcppacket(X1,X2,X5,X3)))),99). clause( || Network(U) Sent(epacket(V,W,X,e_ip,ippacket(Y,Z,tcp,tcppacket(X1,X2,no_syn,X3)))) Network(V) TCP_Connection_Open(tcp_connection_open(X4,Z,Y,X2,X1)) Firewall(firewall(X4,V,U)) -> Sent(epacket(U,W,X,e_ip,ippacket(Y,Z,tcp,tcppacket(X1,X2,X5,X3)))),100). clause( || Network(U) Network(V) Sent(epacket(V,W,X,e_ip,ippacket(Y,Z,tcp,tcppacket(X1,X2,fin,X3)))) TCP_Connection_Open(tcp_connection_open(X4,Y,Z,X1,X2)) Firewall(firewall(X4,V,U)) -> Sent(epacket(U,W,X,e_ip,ippacket(Y,Z,tcp,tcppacket(X1,X2,fin,X3)))),101). clause( || Network(U) Network(V) Sent(epacket(V,W,X,e_ip,ippacket(Y,Z,tcp,tcppacket(X1,X2,fin,X3)))) TCP_Connection_Open(tcp_connection_open(X4,Z,Y,X1,X2)) Firewall(firewall(X4,V,U)) -> Sent(epacket(U,W,X,e_ip,ippacket(Y,Z,tcp,tcppacket(X1,X2,fin,X3)))),102). clause( || Network(U) Network(V) Sent(epacket(V,W,X,e_ip,ippacket(Y,Z,tcp,tcppacket(X1,X2,finack,X3)))) TCP_Connection_HalfClosed(tcp_connection_halfclosed(X4,Y,Z,X1,X2)) Firewall(firewall(X4,V,U)) -> Sent(epacket(U,W,X,e_ip,ippacket(Y,Z,tcp,tcppacket(X1,X2,finack,X3)))),103). clause( || equal(ipand(U,V),W) NotForwarded(not_forwarded(ippacket(X,U,Y,Z),X1)) equal(ipand(X2,X3),ipand(X4,X3)) RouteEntry(route(X5,V,W,X4,next_route(X1))) RouteIPPacket(route_ip_packet(X5,ippacket(X,U,Y,Z))) Interface(interface(X5,X2,X3,X6,X7)) -> SendIPPacket(send_ip_packet(X5,X4,ippacket(X,U,Y,Z))),104). clause( || equal(ipand(U,V),W) equal(ipand(X,Y),ipand(U,Y)) NotForwarded(not_forwarded(ippacket(Z,U,X1,X2),X3)) RouteEntry(route(X4,V,W,local,next_route(X3))) RouteIPPacket(route_ip_packet(X4,ippacket(Z,U,X1,X2))) Interface(interface(X4,X,Y,X5,X6)) -> SendIPPacket(send_ip_packet(X4,U,ippacket(Z,U,X1,X2))),105). clause( || equal(ipand(U,V),W) equal(ipand(X,Y),Z) Network(X1) Network(X2) Sent(epacket(X2,X3,X4,e_ip,ippacket(X,U,udp,udppacket(X5,X6,X7)))) UDP_FirewallRule(udp_fwrule(X8,first_rule,permit,Z,Y,W,V,X5,X6)) Firewall(firewall(X8,X2,X1)) -> UDP_ConnectionOpen(udp_connection_open(X8,X,U,X5,X6)),106). clause( || equal(ipand(U,V),W) equal(ipand(X,Y),Z) Network(X1) Network(X2) Sent(epacket(X2,X3,X4,e_ip,ippacket(X,U,tcp,tcppacket(X5,X6,syn,X7)))) TCP_FirewallRule(tcp_fwrule(X8,first_rule,permit,Z,Y,W,V,X5,X6)) Firewall(firewall(X8,X2,X1)) -> TCP_ClientSynSent(tcp_clientsynsent(X8,X,U,X5,X6)),107). clause( || Network(U) Network(V) Firewall(firewall(W,V,U)) UDP_FirewallRule(udp_fwrule(W,X,Y,Z,X1,X2,X3,X4,X5)) Sent(epacket(V,X6,X7,e_ip,ippacket(X8,X9,udp,udppacket(X10,X11,X12)))) -> equal(X10,X4) UDP_NotMatched(udp_matched(W,V,U,X6,X7,X8,X9,udp,X10,X11,X,Y,Z,X1,X2,X3,X4,X5)),108). clause( || Network(U) Network(V) Firewall(firewall(W,V,U)) UDP_FirewallRule(udp_fwrule(W,X,Y,Z,X1,X2,X3,X4,X5)) Sent(epacket(V,X6,X7,e_ip,ippacket(X8,X9,udp,udppacket(X10,X11,X12)))) -> equal(X11,X5) UDP_NotMatched(udp_matched(W,V,U,X6,X7,X8,X9,udp,X10,X11,X,Y,Z,X1,X2,X3,X4,X5)),109). clause( || Network(U) Network(V) Firewall(firewall(W,V,U)) TCP_FirewallRule(tcp_fwrule(W,X,Y,Z,X1,X2,X3,X4,X5)) Sent(epacket(V,X6,X7,e_ip,ippacket(X8,X9,tcp,tcppacket(X10,X11,syn,X12)))) -> equal(X10,X4) TCP_NotMatched(tcp_not_matched(W,V,U,X6,X7,X8,X9,tcp,X10,X11,syn,X,Y,Z,X1,X2,X3,X4,X5)),110). clause( || Network(U) Network(V) Firewall(firewall(W,V,U)) TCP_FirewallRule(tcp_fwrule(W,X,Y,Z,X1,X2,X3,X4,X5)) Sent(epacket(V,X6,X7,e_ip,ippacket(X8,X9,tcp,tcppacket(X10,X11,syn,X12)))) -> equal(X11,X5) TCP_NotMatched(tcp_not_matched(W,V,U,X6,X7,X8,X9,tcp,X10,X11,syn,X,Y,Z,X1,X2,X3,X4,X5)),111). clause( || Network(U) Network(V) Firewall(firewall(W,V,U)) UDP_FirewallRule(udp_fwrule(W,X,Y,Z,X1,X2,X3,X4,X5)) Sent(epacket(V,X6,X7,e_ip,ippacket(X8,X9,udp,udppacket(X10,X11,X12)))) -> equal(ipand(X8,X1),Z) UDP_NotMatched(udp_matched(W,V,U,X6,X7,X8,X9,udp,X10,X11,X,Y,Z,X1,X2,X3,X4,X5)),112). clause( || Network(U) Network(V) Firewall(firewall(W,V,U)) UDP_FirewallRule(udp_fwrule(W,X,Y,Z,X1,X2,X3,X4,X5)) Sent(epacket(V,X6,X7,e_ip,ippacket(X8,X9,udp,udppacket(X10,X11,X12)))) -> equal(ipand(X9,X3),X2) UDP_NotMatched(udp_matched(W,V,U,X6,X7,X8,X9,udp,X10,X11,X,Y,Z,X1,X2,X3,X4,X5)),113). clause( || equal(ipand(U,V),W) equal(ipand(X,Y),Z) Network(X1) Network(X2) Sent(epacket(X2,X3,X4,e_ip,ippacket(X,U,udp,udppacket(X5,X6,X7)))) UDP_FirewallRule(udp_fwrule(X8,first_rule,permit,Z,Y,W,V,X5,X6)) Firewall(firewall(X8,X2,X1)) -> Sent(epacket(X1,X3,X4,e_ip,ippacket(X,U,udp,udppacket(X5,X6,X7)))),114). clause( || Network(U) Network(V) Firewall(firewall(W,V,U)) TCP_FirewallRule(tcp_fwrule(W,X,Y,Z,X1,X2,X3,X4,X5)) Sent(epacket(V,X6,X7,e_ip,ippacket(X8,X9,tcp,tcppacket(X10,X11,syn,X12)))) -> equal(ipand(X8,X1),Z) TCP_NotMatched(tcp_not_matched(W,V,U,X6,X7,X8,X9,tcp,X10,X11,syn,X,Y,Z,X1,X2,X3,X4,X5)),115). clause( || Network(U) Network(V) Firewall(firewall(W,V,U)) TCP_FirewallRule(tcp_fwrule(W,X,Y,Z,X1,X2,X3,X4,X5)) Sent(epacket(V,X6,X7,e_ip,ippacket(X8,X9,tcp,tcppacket(X10,X11,syn,X12)))) -> equal(ipand(X9,X3),X2) TCP_NotMatched(tcp_not_matched(W,V,U,X6,X7,X8,X9,tcp,X10,X11,syn,X,Y,Z,X1,X2,X3,X4,X5)),116). clause( || equal(ipand(U,V),W) equal(ipand(X,Y),Z) Network(X1) Network(X2) Sent(epacket(X2,X3,X4,e_ip,ippacket(X,U,udp,udppacket(X5,X6,X7)))) UDP_FirewallRule(udp_fwrule(X8,first_rule,deny,Z,Y,W,V,X5,X6)) Firewall(firewall(X8,X2,X1)) -> Denied(denied(X8,X2,X1,first_rule,X3,X4,X,U,udp,udppacket(X5,X6,X7))),117). clause( || equal(ipand(U,V),W) equal(ipand(X,Y),Z) Network(X1) Network(X2) Sent(epacket(X2,X3,X4,e_ip,ippacket(X,U,tcp,tcppacket(X5,X6,syn,X7)))) TCP_FirewallRule(tcp_fwrule(X8,first_rule,permit,Z,Y,W,V,X5,X6)) Firewall(firewall(X8,X2,X1)) -> Sent(epacket(X1,X3,X4,e_ip,ippacket(X,U,tcp,tcppacket(X5,X6,syn,X7)))),118). clause( || equal(ip(0,U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25),ip(1,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,119). clause( || equal(ip(U,0,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25),ip(X26,1,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,120). clause( || equal(ip(U,V,0,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25),ip(X26,X27,1,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,121). clause( || equal(ip(U,V,W,0,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25),ip(X26,X27,X28,1,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,122). clause( || equal(ip(U,V,W,X,0,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25),ip(X26,X27,X28,X29,1,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,123). clause( || equal(ip(U,V,W,X,Y,0,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25),ip(X26,X27,X28,X29,X30,1,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,124). clause( || equal(ip(U,V,W,X,Y,Z,0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25),ip(X26,X27,X28,X29,X30,X31,1,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,125). clause( || equal(ip(U,V,W,X,Y,Z,X1,0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25),ip(X26,X27,X28,X29,X30,X31,X32,1,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,126). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,0,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,1,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,127). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,0,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,1,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,128). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,0,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,1,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,129). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,0,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,1,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,130). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,0,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,1,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,131). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,0,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,1,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,132). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,0,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,1,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,133). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,0,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,1,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,134). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,0,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,1,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,135). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,0,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,1,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,136). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,0,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,1,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,137). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,0,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,1,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,138). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,0,X17,X18,X19,X20,X21,X22,X23,X24,X25),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,1,X48,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,139). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,0,X18,X19,X20,X21,X22,X23,X24,X25),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,1,X49,X50,X51,X52,X53,X54,X55,X56)) -> ,140). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,0,X19,X20,X21,X22,X23,X24,X25),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,1,X50,X51,X52,X53,X54,X55,X56)) -> ,141). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,0,X20,X21,X22,X23,X24,X25),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,1,X51,X52,X53,X54,X55,X56)) -> ,142). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,0,X21,X22,X23,X24,X25),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,1,X52,X53,X54,X55,X56)) -> ,143). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,0,X22,X23,X24,X25),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,1,X53,X54,X55,X56)) -> ,144). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,0,X23,X24,X25),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,1,X54,X55,X56)) -> ,145). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,0,X24,X25),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,1,X55,X56)) -> ,146). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,0,X25),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,1,X56)) -> ,147). clause( || equal(ip(U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,0),ip(X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56,1)) -> ,148). clause( || equal(ipand(U,V),W) equal(ipand(X,Y),Z) Network(X1) Network(X2) Sent(epacket(X2,X3,X4,e_ip,ippacket(X,U,tcp,tcppacket(X5,X6,syn,X7)))) TCP_FirewallRule(tcp_fwrule(X8,first_rule,deny,Z,Y,W,V,X5,X6)) Firewall(firewall(X8,X2,X1)) -> Denied(denied(X8,X2,X1,first_rule,X3,X4,X,U,tcp,tcppacket(X5,X6,syn,X7))),149). clause( || equal(ipand(U,V),W) equal(ipand(X,Y),Z) Network(X1) Network(X2) Sent(epacket(X2,X3,X4,e_ip,ippacket(X,U,udp,udppacket(X5,X6,X7)))) Firewall(firewall(X8,X2,X1)) UDP_FirewallRule(udp_fwrule(X8,next_rule(X9),permit,Z,Y,W,V,X5,X6)) UDP_NotMatched(udp_matched(X8,X2,X1,X3,X4,X,U,udp,X5,X6,X9,X10,X11,X12,X13,X14,X15,X16)) -> UDP_ConnectionOpen(udp_connection_open(X8,X,U,X5,X6)),150). clause( || equal(ipand(U,V),W) equal(ipand(X,Y),Z) Network(X1) Network(X2) Sent(epacket(X2,X3,X4,e_ip,ippacket(X,U,tcp,tcppacket(X5,X6,syn,X7)))) Firewall(firewall(X8,X2,X1)) TCP_FirewallRule(tcp_fwrule(X8,next_rule(X9),permit,Z,Y,W,V,X5,X6)) TCP_NotMatched(tcp_not_matched(X8,X2,X1,X3,X4,X,U,tcp,X5,X6,syn,X9,X10,X11,X12,X13,X14,X15,X16)) -> TCP_ClientSynSent(tcp_clientsynsent(X8,X,U,X5,X6)),151). clause( || equal(ipand(U,V),W) equal(ipand(X,Y),Z) Network(X1) Network(X2) Sent(epacket(X2,X3,X4,e_ip,ippacket(X,U,udp,udppacket(X5,X6,X7)))) Firewall(firewall(X8,X2,X1)) UDP_FirewallRule(udp_fwrule(X8,next_rule(X9),permit,Z,Y,W,V,X5,X6)) UDP_NotMatched(udp_matched(X8,X2,X1,X3,X4,X,U,udp,X5,X6,X9,X10,X11,X12,X13,X14,X15,X16)) -> Sent(epacket(X1,X3,X4,e_ip,ippacket(X,U,udp,udppacket(X5,X6,X7)))),152). clause( || equal(ipand(U,V),W) equal(ipand(X,Y),Z) Network(X1) Network(X2) Sent(epacket(X2,X3,X4,e_ip,ippacket(X,U,udp,udppacket(X5,X6,X7)))) Firewall(firewall(X8,X2,X1)) UDP_FirewallRule(udp_fwrule(X8,next_rule(X9),deny,Z,Y,W,V,X5,X6)) UDP_NotMatched(udp_matched(X8,X2,X1,X3,X4,X,U,udp,X5,X6,X9,X10,X11,X12,X13,X14,X15,X16)) -> Denied(denied(X8,X2,X1,next_rule(X9),X3,X4,X,U,udp,udppacket(X5,X6,X7))),153). clause( || equal(ipand(U,V),W) equal(ipand(X,Y),Z) Network(X1) Network(X2) Sent(epacket(X2,X3,X4,e_ip,ippacket(X,U,tcp,tcppacket(X5,X6,syn,X7)))) Firewall(firewall(X8,X2,X1)) TCP_FirewallRule(tcp_fwrule(X8,next_rule(X9),permit,Z,Y,W,V,X5,X6)) TCP_NotMatched(tcp_not_matched(X8,X2,X1,X3,X4,X,U,tcp,X5,X6,syn,X9,X10,X11,X12,X13,X14,X15,X16)) -> Sent(epacket(X1,X3,X4,e_ip,ippacket(X,U,tcp,tcppacket(X5,X6,syn,X7)))),154). clause( || equal(ipand(U,V),W) equal(ipand(X,Y),Z) Network(X1) Network(X2) Sent(epacket(X2,X3,X4,e_ip,ippacket(X,U,tcp,tcppacket(X5,X6,syn,X7)))) Firewall(firewall(X8,X2,X1)) TCP_FirewallRule(tcp_fwrule(X8,next_rule(X9),deny,Z,Y,W,V,X5,X6)) TCP_NotMatched(tcp_not_matched(X8,X2,X1,X3,X4,X,U,tcp,X5,X6,syn,X9,X10,X11,X12,X13,X14,X15,X16)) -> Denied(denied(X8,X2,X1,next_rule(X9),X3,X4,X,U,tcp,tcppacket(X5,X6,syn,X7))),155). clause( || -> equal(ip(land(U,V),land(W,X),land(Y,Z),land(X1,X2),land(X3,X4),land(X5,X6),land(X7,X8),land(X9,X10),land(X11,X12),land(X13,X14),land(X15,X16),land(X17,X18),land(X19,X20),land(X21,X22),land(X23,X24),land(X25,X26),land(X27,X28),land(X29,X30),land(X31,X32),land(X33,X34),land(X35,X36),land(X37,X38),land(X39,X40),land(X41,X42),land(X43,X44),land(X45,X46),land(X47,X48),land(X49,X50),land(X51,X52),land(X53,X54),land(X55,X56),land(X57,X58)),ipand(ip(U,W,Y,X1,X3,X5,X7,X9,X11,X13,X15,X17,X19,X21,X23,X25,X27,X29,X31,X33,X35,X37,X39,X41,X43,X45,X47,X49,X51,X53,X55,X57),ip(V,X,Z,X2,X4,X6,X8,X10,X12,X14,X16,X18,X20,X22,X24,X26,X28,X30,X32,X34,X36,X38,X40,X42,X44,X46,X48,X50,X52,X54,X56,X58))),156). end_of_list. list_of_clauses(conjectures, cnf). end_of_list. list_of_settings(SPASS). {* set_flag(Ordering,1). set_flag(CNFFEqR,0). set_flag(RInput,0). set_flag(Splits,0). set_precedence(net1_addr,net2_addr,net3_addr,networkip,broadcastip,mask32,mask24,mask16,mask8,mask0,c_class,any,local,c1_ip,c2_ip,rl1_ip,s1_ip,r1_ip_net1,r1_ip_net2,r2_ip_net2,r2_ip_net3,ipand,land,ip,ippacket). set_selection(Sent, TCP_FirewallRule, UDP_FirewallRule,RouteIPPacket,ReceivedIPPacket,SendIPPacket,ArpTable,Interface). set_ClauseFormulaRelation((1,axiom80), (2,axiom79), (3,axiom78), (4,axiom77), (5,axiom40), (6,axiom40), (7,axiom3), (8,axiom2), (9,axiom1), (10,axiom0), (11,axiom105), (12,axiom104), (13,axiom93), (14,axiom92), (15,axiom91), (16,axiom90), (17,axiom89), (18,axiom88), (19,axiom87), (20,axiom86), (21,axiom85), (22,axiom84), (23,axiom83), (24,axiom102), (25,axiom100), (26,axiom98), (27,axiom96), (28,axiom94), (29,axiom82), (30,axiom81), (31,axiom103), (32,axiom101), (33,axiom99), (34,axiom97), (35,axiom95), (36,axiom39), (37,axiom38), (38,axiom37), (39,axiom36), (40,axiom108), (41,axiom106), (42,axiom109), (43,axiom107), (44,axiom110), (45,axiom35), (46,axiom35), (47,axiom41), (48,axiom34), (49,axiom57), (50,axiom57), (51,axiom57), (52,axiom54), (53,axiom43), (54,axiom44), (55,axiom55), (56,axiom55), (57,axiom55), (58,axiom56), (59,axiom56), (60,axiom56), (61,axiom50), (62,axiom50), (63,axiom50), (64,axiom51), (65,axiom51), (66,axiom51), (67,axiom111), (68,axiom112), (69,axiom113), (70,axiom114), (71,axiom115), (72,axiom116), (73,axiom117), (74,axiom118), (75,axiom119), (76,axiom120), (77,axiom121), (78,axiom122), (79,axiom123), (80,axiom124), (81,axiom125), (82,axiom126), (83,axiom127), (84,axiom128), (85,axiom45), (86,axiom46), (87,axiom63), (88,axiom64), (89,axiom68), (90,axiom69), (91,axiom70), (92,axiom48), (93,axiom49), (94,axiom47), (95,axiom65), (96,axiom76), (97,axiom63), (98,axiom64), (99,axiom66), (100,axiom67), (101,axiom68), (102,axiom69), (103,axiom70), (104,axiom52), (105,axiom53), (106,axiom72), (107,axiom59), (108,axiom71), (109,axiom71), (110,axiom58), (111,axiom58), (112,axiom71), (113,axiom71), (114,axiom72), (115,axiom58), (116,axiom58), (117,axiom74), (118,axiom59), (119,axiom4), (120,axiom5), (121,axiom6), (122,axiom7), (123,axiom8), (124,axiom9), (125,axiom10), (126,axiom11), (127,axiom12), (128,axiom13), (129,axiom14), (130,axiom15), (131,axiom16), (132,axiom17), (133,axiom18), (134,axiom19), (135,axiom20), (136,axiom21), (137,axiom22), (138,axiom23), (139,axiom24), (140,axiom25), (141,axiom26), (142,axiom27), (143,axiom28), (144,axiom29), (145,axiom30), (146,axiom31), (147,axiom32), (148,axiom33), (149,axiom61), (150,axiom73), (151,axiom60), (152,axiom73), (153,axiom75), (154,axiom60), (155,axiom62), (156,axiom42)). *} end_of_list. end_problem.