Curriculum: Logical/Formal Methods in Security

Question

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.

Answer 1

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.

Answer 2

There was a reading course at Carnegie Mellon a few years ago, Languages and Logics for Security, which tried to survey some of the literature in authentication, authorization, information flow, protocol calculi, protection, and trust management; the course web page has slides for the papers we discussed as well as a further list of references for each topic. Information flow in particular might be something worth taking a look at relative to the topics you listed.

The curriculum for Anupam Datta's course Foundations of Security and Privacy is also relevant.

Answer 3

Rob's answer reminded me of a similar Cornell reading group that Michael Clarkson organized for a few years: Cornell Security Discussion Group. Might be worth skimming through there for some papers.

Answer 4

I am not sure of what you hide under the word "verification" so I give a try. Maybe you can add something about quantitative verification of Markov Decision Processes and the use of probabilistic temporal logic (pLTL and PCTL). In this framework you have a pretty good way of modelling adversaries, of expressing properties and there exists easy to use verification tools (PRISM for instance).

Answer 5

You could also take a look at the following graduate course on security protocols in Paris (the text is mostly in French):

http://mpri.master.univ-paris7.fr/C-2-30.html

Answer 6

A lecture on Provable Security could be interesting, in particular using Game Theory. I think that the Chapters 8 and 25 of the Nisan et al book on Algorithmic Game Theory could provide a good basis.

I would also include a brief description of existing security/safety standards, such as ITSEC/TCSEC and the Common Criteria. It's always good to point out that in order to achieve the highest level of the Common Criteria, it is necessary to formally verify, design and test a system.