This talk will identify and explore some applications for proof-theoretic methods from logic to computer security, the branch of computer science concerned with the protection of computer systems and digital information. While cryptography is a well-developed area with a sound mathematical basis, many practical computer security problems involve failures of software design and implementation, not failures of cryptography. The areas of network security, access control, intrusion detection, and system security are full of informal practices waiting to be given precise definitions and analyzed. This talk will discuss a rigorous and precise framework, based on logic, for an analysis of network security protocols that are commonly used to protect access to computer systems and to protect transactions over the internet.