Curriculum: Logical/Formal Methods in Security At present I teach a small course (Four two hour lectures at the Masters level) on Logical Methods in Security, though the title Formal Methods in Security might be more apt. It covers briefly the following topics (with associated logical methods):


Digital Rights Management and Policy Enforcement (general formalisation, modal logic, enforcement via automata)
Proof-carrying code and proof-carrying authentication (proof theory, logical systems, Curry-Howard Isomorphism, verification)
Access Control (non-classical logics, proof theory)
Stack Inspection (programming language semantics, contextual equivalence, bisimulation)


Naturally, the course has multiple goals, where one of them is attracting potential graduate students.

In the coming years the course may be expanded to a regular course, which will need more content. Given that the background of people here is quite different from mine, I would like to know what content you would include in such a course.
I suggest familiarizing the students with the following logics:


Epistemic logic: Used to model the knowledge of various parties participating in the protocol, and prove that an adversary cannot gain knowledge of some secret.
BAN logic: An old logic for proving various properties of authentication protocols. (Other belief logics are appropriate as well.)
Logics for transition systems: This includes logics like LTL, CTL, and LTL*. (such logics act on Kripke-like models of the protocol.)
Process Algebras: Several process algebras, like Spi-calculus (or CSP, and its security-related tool, Casper) are useful for modeling security protocols.
Introducing tools like AVISPA of NuSMV are very useful.
I also suggest Formal Correctness of Security Protocols as one of the course textbooks.


A friend of mine, Morteza Amini, has recently got his Ph.D. on modeling access control with logic. He devised a new logic, named $MA(DL)^2$, which stands for "multi-authority deontic logic and description logic." As the name suggests, it combines two non-classical logics (deontic logic + description logic) to decide whether an entity has access to an object. If you like, I can encourage him to provide more information.