<p>There was a reading course at Carnegie Mellon a few years ago, <a href="http://www.cs.cmu.edu/~rwh/courses/llsec/" rel="nofollow">Languages and Logics for Security</a>, 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. </p>

<p>The curriculum for Anupam Datta's course <a href="http://www.ece.cmu.edu/~ece739/" rel="nofollow">Foundations of Security and Privacy</a> is also relevant.</p>

CC BY-SA 2.5
2010-11-15T11:13:58.317Z
Thanks Rob. In fact I used these two pages when I designed the original course content.
Dave Clarke
CC BY-SA 2.5
2010-11-15T14:59:52.430Z
Aah. Well then I guess its additional utility to you is limited! Hopefully others will find it useful as well :).
Rob Simmons
CC BY-SA 2.5
2010-11-15T02:15:40.710Z
2010-11-15T02:15:40.710Z
Rob Simmons
<p>Rob's answer reminded me of a similar Cornell reading group that Michael Clarkson organized for a few years: <a href="http://www.cs.cornell.edu/people/clarkson/secdg/" rel="nofollow">Cornell Security Discussion Group</a>. Might be worth skimming through there for some papers.</p>

CC BY-SA 2.5
2010-11-15T03:12:04.630Z
2010-11-15T03:12:04.630Z
Mark Reitblatt
<p>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 (<a href="http://www.prismmodelchecker.org/" rel="nofollow">PRISM</a> for instance).</p>

CC BY-SA 2.5
2010-11-15T11:13:06.417Z
Interesting. Do you know of any security applications of PRISM or of these logics?
Dave Clarke
CC BY-SA 2.5
2010-11-15T11:24:52.257Z
in the case studies (http://www.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.
Sylvain Peyronnet
CC BY-SA 2.5
2010-11-15T11:08:18.667Z
2010-11-15T11:08:18.667Z
Sylvain Peyronnet
<p>You could also take a look at the following graduate course on security protocols in Paris (the text is mostly in French):</p>

<p><a href="http://mpri.master.univ-paris7.fr/C-2-30.html" rel="nofollow">http://mpri.master.univ-paris7.fr/C-2-30.html</a></p>

CC BY-SA 3.0
2011-04-12T14:48:36.113Z
To speak French ...
Dave Clarke
CC BY-SA 3.0
2011-04-13T21:18:34.957Z
This link leads to an English version: http://mpri.master.univ-paris7.fr/C-2-30en.html
Sylvain
CC BY-SA 3.0
2011-04-12T14:44:32.603Z
2011-04-12T14:44:32.603Z
Stefan Ciobaca
<p>A lecture on Provable Security could be interesting, in particular using Game Theory. I think that the Chapters 8 and 25 of the <a href="http://www.cambridge.org/journals/nisan/downloads/Nisan_Non-printable.pdf" rel="nofollow">Nisan et al book</a> on Algorithmic Game Theory could provide a good basis. </p>

<p>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 <strong>formally</strong> verify, design and test a system. </p>

CC BY-SA 3.0
2012-01-20T01:16:31.487Z
2012-01-20T01:16:31.487Z
Charles
<p>I suggest familiarizing the students with the following logics:</p>

<ul>
<li><strong>Epistemic logic:</strong> Used to model the knowledge of various parties participating in the protocol, and prove that an adversary cannot gain knowledge of some secret.</li>
<li><strong>BAN logic:</strong> An old logic for proving various properties of authentication protocols. (Other <em>belief logics</em> are appropriate as well.)</li>
<li><strong>Logics for transition systems:</strong> This includes logics like LTL, CTL, and LTL*. (such logics act on Kripke-like models of the protocol.)</li>
<li><strong>Process Algebras:</strong> Several process algebras, like <em>Spi-calculus</em> (or <em>CSP</em>, and its security-related tool, <a href="http://www.comlab.ox.ac.uk/gavin.lowe/Security/Casper/" rel="nofollow noreferrer">Casper</a>) are useful for modeling security protocols.</li>
<li>Introducing tools like <a href="http://www.avispa-project.org/" rel="nofollow noreferrer">AVISPA</a> of <a href="http://nusmv.fbk.eu/" rel="nofollow noreferrer">NuSMV</a> are very useful.</li>
<li>I also suggest <a href="http://www.springer.com/computer/theoretical+computer+science/book/978-3-540-68134-2" rel="nofollow noreferrer">Formal Correctness of Security Protocols</a> as one of the course textbooks.</li>
</ul>

<p>A friend of mine, <a href="https://cstheory.stackexchange.com/users/994/morteza-amini">Morteza Amini</a>, 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.</p>

CC BY-SA 2.5
2010-11-14T19:33:39.460Z
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.
Dave Clarke
CC BY-SA 2.5
2010-11-14T20:15:46.540Z
@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: http://ifile.it/xljn9s8/EpistemicLogic.rar. I suggest taking a look at that, before dropping the topic altogether.
Sadeq Dousti
CC BY-SA 2.5
2010-11-14T21:50:06.893Z
Thanks for the link. Epistemic Logic has not be dropped completely; it just didn't fit this year.
Dave Clarke
CC BY-SA 2.5
2010-11-14T16:35:21.057Z
2010-11-14T16:44:56.363Z
2017-04-13T12:32:28.077Z
Sadeq Dousti
<p>At present I teach a small course (Four two hour lectures at the Masters level) on <em>Logical Methods in Security</em>, though the title <em>Formal Methods in Security</em> might be more apt. It covers briefly the following topics (with associated logical methods):</p>

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

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

<p>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.</p>

<lo.logic><cr.crypto-security><teaching><security><formal-methods>
Curriculum: Logical/Formal Methods in Security
Dave Clarke
# Curriculum: Logical/Formal Methods in Security

(Asked by: username_0 on 2010-11-14)

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.

**Tags:** lo.logic, cr.crypto-security, teaching, security, formal-methods

---

## 6 answers

### Answer by username_7 on 2010-11-14. Score: 15 | Accepted answer

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](http://www.comlab.ox.ac.uk/gavin.lowe/Security/Casper/)) are useful for modeling security protocols.
* Introducing tools like [AVISPA](http://www.avispa-project.org/) of [NuSMV](http://nusmv.fbk.eu/) are very useful.
* I also suggest [Formal Correctness of Security Protocols](http://www.springer.com/computer/theoretical+computer+science/book/978-3-540-68134-2) as one of the course textbooks.

A friend of mine, [Morteza Amini](https://cstheory.stackexchange.com/users/994/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.

> **Comments:**
> **username_0**: 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.  
> **username_7**: @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: http://ifile.it/xljn9s8/EpistemicLogic.rar. I suggest taking a look at that, before dropping the topic altogether.  
> **username_0**: Thanks for the link. Epistemic Logic has not be dropped completely; it just didn't fit this year.  

---

### Answer by username_1 on 2010-11-15. Score: 12

There was a reading course at Carnegie Mellon a few years ago, [Languages and Logics for Security](http://www.cs.cmu.edu/~rwh/courses/llsec/), 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](http://www.ece.cmu.edu/~ece739/) is also relevant.

> **Comments:**
> **username_0**: Thanks Rob. In fact I used these two pages when I designed the original course content.  
> **username_1**: Aah. Well then I guess its additional utility to you is limited! Hopefully others will find it useful as well :).  

---

### Answer by username_2 on 2010-11-15. Score: 10

Rob's answer reminded me of a similar Cornell reading group that Michael Clarkson organized for a few years: [Cornell Security Discussion Group](http://www.cs.cornell.edu/people/clarkson/secdg/). Might be worth skimming through there for some papers.


---

### Answer by username_3 on 2010-11-15. Score: 6

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](http://www.prismmodelchecker.org/) for instance).

> **Comments:**
> **username_0**: Interesting. Do you know of any security applications of PRISM or of these logics?  
> **username_3**: in the case studies (http://www.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.  

---

### Answer by username_4 on 2011-04-12. Score: 3

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>

> **Comments:**
> **username_0**: To speak French ...  
> **username_5**: This link leads to an English version: http://mpri.master.univ-paris7.fr/C-2-30en.html  

---

### Answer by username_6 on 2012-01-20. Score: 1

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](http://www.cambridge.org/journals/nisan/downloads/Nisan_Non-printable.pdf) 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.


---

