
The fundamental primitives of Concurrent Constraint Programming (CCP), ${\mathit{tell}}$ and ${\mathit {ask}}$, respectively adds knowledge to and infers knowledge from a shared constraint store. These features, and the elegant use of the constraint system to represent the abilities of attackers, make concurrent constraint programming and timed CCP ( tcc ) interesting candidates for modeling and reasoning about security protocols. However, they lack primitives for the communication of secrets (or local names as in the *** -calculus) between agents. The recently proposed ${\mathit{universal}} {\mathtt{tcc}}$ ( utcc ) introduces a universally quantified ask operation that makes it possible to infer knowledge which is local to other agents. However, it allows agents to guess knowledge even if it is encrypted or communicated on secret channels, simply by quantifying over both the encryption key (or channel) and the message simultaneously. We present a secure utcc ( utcc s ) based on: (i) a simple type system for constraints allowing to distinguish between restricted (secure) and non-restricted (universally quantifiable) variables in constraints, and (ii) a generalization of the universally quantified ask operation to allow the assumption of local knowledge. We illustrate the use of the utcc s calculus with examples on communication of local names (as in the *** -calculus) and for giving semantics to secure pattern matching in a prototypical security language.
Mobility, Security, Type systems, Concurrent Constraint Programming, Process Calculi
Mobility, Security, Type systems, Concurrent Constraint Programming, Process Calculi
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 4 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
