[Prev][Next][Index]
Re: Traits for BAN logic, TAOS auth, URI/IIIR stuff...
In message <9501112028.AA29708@grant.pa.dec.com>, ma@pa.dec.com writes:
>
>[...] There is something essentially wrong (or at
>least tricky) in mixing a modal logic (such as the BAN logic) with
>Larch. A traditional example goes: (the number of planets = 9) and
>(P believes (the number of planets = 7)) should not yield (P believes
>(9 = 7)). However, you may be able to hack something up.
My ban.lsl includes a "hack" that is supposed to account for this:
modal statements are of sort X, not sort Bool. There's a "projection"
operator [__] : X -> Bool for dealing with modal statements as Larch
formulas, and each of the conventional connectives has an analog in
X-space. The only connective used in the paper I read was conjunction,
which I modeled with \also.
There are postulates:
[ p \believes (x \also y) ] => [ p \believes x ]
[ p \believes x ] /\ [ p \believes y ] => [ p \believes (x \also y) ]
and such, but that's about it. The example would have to translate to:
numberOfPanets = 9 /\ [ p \believes (numberOfPlanets = 7) ]
=> [ p believes (9 = 7)]
but that's not a formula, because the term (numberOfPlantes = 7) is of
sort Bool, and __ \believes __ is X, X -> X, so the sorts wouldn't
match.
The bit about quantifiers looked like a stumper, but I never seemed
to need quantifiers inside the []'s, so I think I'm alright.
I'll feel better when I've sort-checked ban.lsl and worked few
a theorem or two with the Larch Prover, but for now... does that
look like a sound approach?
>- There have been other little automations of this and related logics.
>However, I have always found hand proofs perfectly satisfactory for
>my needs.
It's nice to have tools that assist me in building my intuition about
how all this works. For example, the business of abreviating "{X}k
from R" as just "{X}k" became much more clear to me when I worked
it out in Larch. Who knows if this will turn out to be a valuable
engineering technique... for know, I'm satisfied that it makes an
interesting intellectual excercise :-)
My hope is that larch traits, proofs, and interface specifications
will serve as engineering documentation for WWW/IIIR technology. But
who knows...
>- I don't expect the BAN logic will be suitable for everything you
>want. I am confident it can be used to explain some aspects of S-HTTP
>and SSL, for example, but not all. In fact, some of the techniques
>that Mike Burrows and I suggested for SSL (and which made it into
>the RFC) are hard to model in the BAN logic and in related logics.
Hmmm... now I'm curious. Care to elaborate?
Even so, I expect I'll learn quite a bit about all this before I get
to the parts of S-HTTP that can't be modeled by BAN logic, or by Larch
at all.
>- The simple protocol you suggest is insecure, as you say, and it
>would be seems a bit strange to modify the logic to get any conclusion
>stronger than the one you have. The conclusion you have simply means
>that the server believes that the client is alive at the moment and
>has recently said the nonce. (In the original BAN logic, there is
>a bit of an identification between beliefs and things recently said.)
OK. Good. Now I believe that you believe that I understand at least
this much :-) That's progress!
>I hope this helps.
Certainly! Thanks for the quick reply!
Dan
Reference(s):