[E-Lang] Re: there is no security without a threat model (was: Re: [p2p-hackers] Reputation System: "Dimensions of Trust")

[Dan Moniz]

At 09:05 PM 6/13/2001 -0700, Steve Jenson wrote:

>BTW, has anybody here have an opinion on CSP? It's a process algebra
>for modelling the security properties of communicating processes (as
>an abstract term). I'm currently reading a book out of the UK called
>"Modelling and Analysis of Security Protocols" (ISBN:0201674718), and so
>far it's been an interesting read. Here's a site devoted to the subject:
>http://www.afm.sbu.ac.uk/csp/

I'll admit up-front that I have a passing familiarity with CSP. I've looked 
at it and the underlying mathematics, but I haven't played with it much.

While CSP is a process algebra, formal specifications of security protocols 
is nothing terribly new (not that I'm implying that you're implying that it 
is). I have a lot of experience with formal logics for security protocols, 
particularly BAN and GNY, which deal with authentication. And I'm not 
counting all the standard model stuff like Bell-LaPadula (BLP), Biba, RBAC, 
etc.

Rather than commit to an opinion at this stage on CSP, I'll just make some 
statements that could be formed into an opinion with a little "client-side" 
extrapolation (i.e., make of this what you will):

CSP is really based around expressing the model flow of processes in 
sequence, although there's significant work regarding it and concurrent 
systems. It has a general applicability to software modelling and 
constitutes a first-order logic. All of this is good in specifying systems 
and providing material for proofs (indeed, CSP was invented by Hoare, who 
we all know from proof of program correctness research, among many other 
computing topics). I'm not sure where CSP fits in when trying to 
analytically attack security protocols, since it suffers from the same 
sorts of issues as BAN and GNY do -- it models an ideal system of 
communication, but just because your protocol matches with your CSP 
representation doesn't mean it necessarily follows it as strictly as you 
would perhaps like, and is still susceptible to subversion.

In general, I'd rate CSP as another general tool in the toolbox of software 
modelling, with BAN and GNY logics, and BLP, Biba, and RBAC, etc. models 
being similar tools, but more firmly oriented around security design 
concerns. Then again, I haven't read the book you mentioned, so I'm not 
sure how the author(s) is(/are) applying CSP to security protocols (but I 
can concoct some straightforward assumptions in my head pretty easily).


--
Dan Moniz <dnm@pobox.com> [http://www.pobox.com/~dnm/]