Important guarantees for LAN infrastructures include connectivity, error
detection/recovery, robust changes and security.  In the talk I will develop
a LAN infrastructure model in first-order logic enabling automatic analysis 
of such properties. The model starts at the ethernet layer of the TCP/IP
stack and ranges up to application protocols such as DHCP.