[Prev][Next][Index]
Re: Traits for BAN logic, TAOS auth, URI/IIIR stuff...
Leslie Lamport forwarded your message. In answer to your questions:
- I don't know of any Larch trait for the BAN logic, although at
a very early stage Mike Burrows and Jim Horning may have thought
about defining one. 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.
- There have been other little automations of this and related logics.
However, I have always found hand proofs perfectly satisfactory for
my needs.
- 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.
- 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.)
I hope this helps.
Martin Abadi
Follow-Up(s):