This paper presents an outline specification of the IP and TCP communication protocols in mixed intuitionistic linear logic and describes how this logic can be used to prove some properties of both protocols. We have previously presented a specification of IP in [8] using commutative linear logic; in this paper we extend this specification considerably to include TCP, which, in turn, necessitates the use of non-commutative operators. Linear logic is particularly suited to the description of state-based systems, and communication protocols in particular, since it keeps track of the resources used in each deduction step. Mixed intuitionistic linear logic is variant of linear logic that contains both commutative and non-commutative operators, and as such is useful where the order of the consumption of resources must be specified. In the following sections we brie y describe IP and TCP and linear logic. We then present an outline of our specification of the user interfaces for IP and TCP, demonstrating the role of the linear operators in the axioms. Finally, we outline the remainder of our work concerning the description of the TCP protocol itself and the verification process undertaken.