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