Medium Access Control (MAC) protocols for Local Area Networks (LANs), yielding minimal delay and maximal throughput, have emerged as essential for supporting real-time applications. Design and performance analysis of these protocols have been informal and ad hoc. Such informal methods lead to ambiguities and result in time-consuming redesign should errors occur. This paper presents a formal method of modelling and performance evaluation for LAN protocols based on an Extended Finite State Machine (EFSM) model. Initially, this paper describes the EFSM model embodying the specification of delay, probability, and exclusive use of resources. From the EFSM representation of the protocol, a so-called timed-expanded tree is constructed. Based on the constructed tree, this paper presents the throughput evaluation upon having verified that the protocol preserves a particular property referred to as cyclicity. Consequently, LAN protocols can be formally and automatically modelled and analyzed.