Studying for FMIS
Today I’m at the [ETH][] to study for the exam in Formal Methods for Information Security, which will be next Tuesday.
I’m currently looking at BAN logic (see also Wikipedia), a nice system for proving (a limited set of) properties about security protocols. It deals with the beliefs of the participants in the protocol in a formal way. This allows you to verify that the goals of the protocol can be fulfilled based on the initial assumptions given. An example from BAN could be a rule that says:
If (P believes (Q controls X))
and (P believes (Q believes X))
then P believes X.
Here one should interpret the keyword controls as “has jurisdiction over”. An example could be a server S which has authority over the public keys for B:
If (A believes (S controls public key for B))
and (A believes (S believes public key for B = KB))
then A believes public key for B = KB.
So this rule expresses the trust of A in S. But for this rule to be applicable A needs to believe that S believes public key for B = KB. There’s a rule for introducing such beliefs about other participants beliefs:
If (P believes (X is fresh))
and (P believes (Q said X))
then P believes (Q believes X)
This rule is based on an assumption that you will not say something which you do not believe. There are then more rules stating when you can believe that someone said something (for example, when that something was signed, and you believe in the key used for the signature).
From this big set of rules, one can make more and more deductions and hopefully derive the goals of the protocol. A simple, but pretty cool concept.
Leave a comment