Adventures with Computers
Before I can get back home and begin my Ph.D. I have to make some exams here at the [ETH][]… The plan is as follows:
| Course | Date | Time | Type |
|---|---|---|---|
| Formal Methods for Information Security | 7/2 | 15-17 | Written |
| Randomisierte Algorithmen | 13/2 | 9-12 | Written |
| Formal Verification | 17/2 | 10:00 | Oral |
| Verteilte Algorithmen | 20/2 | 14:15 | Oral |
| Decision Procedures for Logical Theories | 23/2 | 10:00 | Oral |
| Web Algorithms | 3/3 | ? | Oral |
I will then leave for Denmark at the very beginning of March.
Back in November I applied to become a Ph.D student at [DAIMI][], and today I finally got the answer: I am accepted!
This is just so cool! I plan to have my exams at the [ETH][] in the secod half of February, and I will return in the beginning of March — ready for work :-) I’m really looking forward to it.
After being away from Buchs for more than three weeks I’m finally coming back home today. My Christmas holidays started with my going to Denmark to visit my parents. I stayed there for Christmas but went back to Switzerland to get here in time for New Years Eve.
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.
So… December finally arrived. Now is the time to get together, light lots of candles, drink warm tea, gløg, or something else, eat lots of candy, and generally have a nice and cozy time.
And if you don’t celebrate Christmas, then I still wish you a good time with lots of candles and candy and hot beverages :-)
Stéphanie and I will have our Christmasses apart from each other, just like last year. But this time it will be me who travels back and forth, and I’ll be back in Switzerland for the New Year. I’m looking forward to really see Switzerland covered with snow — so far we have only gotten a [little bit of snow][1] a couple of days ago. The temperature has lingered just around the freezing point since, but we haven’t had any precipitation and thus no snow.