[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):