Martin Geisler Online

If you search for “DAIMI” in Google, then you’ll find our nice little DAIMI Planet listed as result number seven. I think that’s pretty cool to become number seven out of 1,780,000 :-) And Google has been pretty fast too — the planet has only been 11 days online.

I’ve been messing around with the dates in Planet DAIMI this evening in an attempt to have the all outputted in our preferred timezone: European Standard Time, a.k.a. GMT+1. It finally worked, but I still managed to become mildly upset about the whole mess about timezones, local time, offsets, etc. :-)

But luckily I find [Python][] a mightly fine language to hack around in — the syntax is simply great and the way you can play with lists (called “list-comprehensions“) is too cool.

Using the very nice [Python][] script Planet Planet! I have now made one for myself and my friends: http://mgeisler.net/daimi/. As the name suggests, it aggregates the news feeds of my friends from [DAIMI][].

Simple and fun! :-)

Update: I’ve tweaked the [CSS][] a bit to produce margins for the post content — and thus to avoid having the faces collide with any right-aligned images you guys post yourself. Let me know of if you use any fancy CSS classes that you would like me to add…

I logged into [DAIMI][] today using the usual DNS alias fresh-horse.daimi.au.dk. This alias is points to the most “fresh” machine out of a number of machines named horse01 … and counting upwards.

Now the sys admins have apparently grown tired of the horses and have switched to camels, for I was logged into camel04 :-) I love this idea of such an alias!

At the [ETH][] things are much more chaotic — the two times I’ve had to log into the network from home I had to search for a long time to find the name of a suitable host! I couldn’t find it on any of the official ETH pages — in the end I found a working hostname somewhere in an exercise sheet for some course in distributed systems.

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 = K_B))
then A believes public key for B = K_B.

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 = K_B. 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.