# 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.

## 6 Answers

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.

• Thanks Sadeq. In earlier years I covered Epistemic Logic in my introduction to Modal Logic for the course, but I dropped it this year. Student's often pick BAN logic for an essay topic. The other suggestions are very useful, especially the tools, which always suggest possible student assignments. Commented Nov 14, 2010 at 19:33
• @Dave: Glad to hear that! I once took part in an excellent crash course (~3 hrs) on "Epistemic Logic for Security Protocols" by Dr. Ramaznian. The presentation can be found here: ifile.it/xljn9s8/EpistemicLogic.rar. I suggest taking a look at that, before dropping the topic altogether. Commented Nov 14, 2010 at 20:15
• Thanks for the link. Epistemic Logic has not be dropped completely; it just didn't fit this year. Commented Nov 14, 2010 at 21:50

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.

• Thanks Rob. In fact I used these two pages when I designed the original course content. Commented Nov 15, 2010 at 11:13
• Aah. Well then I guess its additional utility to you is limited! Hopefully others will find it useful as well :). Commented Nov 15, 2010 at 14:59

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.

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).

• Interesting. Do you know of any security applications of PRISM or of these logics? Commented Nov 15, 2010 at 11:13
• in the case studies (prismmodelchecker.org/casestudies/index.php), there are some examples related to security. Most of them are MDP but it is more about the security of protocols rather than security of implementations. Commented Nov 15, 2010 at 11:24

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

• To speak French ... Commented Apr 12, 2011 at 14:48
• This link leads to an English version: mpri.master.univ-paris7.fr/C-2-30en.html Commented Apr 13, 2011 at 21:18

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.