A Declarative Framework for Security: Secure Concurrent Constraint Programming

Motivation. Due to technological advances such as the Internet and mobile comput-ing, Security has become a serious challenge involving several disciplines of Computer Science. In recent years, there has been a growing interest in the analysis of security protocols and one promising approach is the development of formalisms that model communicating processes, in particular Process Calculi. The results are so far encour-aging although most remains to be done. Concurrent Constraint Programming (CCP) is a well-established formalism which generalizes Logic Programming [Sar93]. In CCP processes interact with each other by telling and asking information represented as constraints in a medium, a so-called store. One of the most appealing and distinct features of CCP is that it combines the traditional operational view of processes calculi with a declarative one of processes based upon logic. This combination allows CCP to benefit from the large body of techniques of both process calculi and logic. Over the last decade, several reasoning techniques and implementations for CCP have been developed: E.g., denotational models [SRP91], specification logics and proof systems [NPV02], Petri Net interpretations [RM94], an