This course deals with computer security from a foundational perspective: aiming to make precise what security means and how we can justify a claim that a system is secure. Even very simple cryptographic protocols for basis security goals such as confidentiality, integrity, authentication, key agreement, and authorisation have often suffered from subtle but serious design flaws: we examine why, and study how we can verify that a protocol is secure. We also consider: advanced protocols for electronic commerce application level objectives (e.g. time stamping, digital cash, payment, contract signing and voting), formal models of access control and information flow (covert channels), programming language perspectives on security, and other topics drawn from recent developments and current research in computer security. The course is more concerned with applications of cryptography than with the mathematics underlying ciphers (which is treated in MATH3411). It takes a more theoretical approach than COMP3441 and TELE3119 and deals with some more advanced topics.