Types for secure pattern matching with local knowledge in universal concurrent constraint programming

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Standard

Types for secure pattern matching with local knowledge in universal concurrent constraint programming. / Hildebrandt, Thomas; López, Hugo A.

Logic Programming - 25th International Conference, ICLP 2009, Proceedings. 2009. p. 417-431 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 5649 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Harvard

Hildebrandt, T & López, HA 2009, Types for secure pattern matching with local knowledge in universal concurrent constraint programming. in Logic Programming - 25th International Conference, ICLP 2009, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5649 LNCS, pp. 417-431, 25th International Conference on Logic Programming, ICLP 2009, Pasadena, CA, United States, 14/07/2009. https://doi.org/10.1007/978-3-642-02846-5_34

APA

Hildebrandt, T., & López, H. A. (2009). Types for secure pattern matching with local knowledge in universal concurrent constraint programming. In Logic Programming - 25th International Conference, ICLP 2009, Proceedings (pp. 417-431). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 5649 LNCS https://doi.org/10.1007/978-3-642-02846-5_34

Vancouver

Hildebrandt T, López HA. Types for secure pattern matching with local knowledge in universal concurrent constraint programming. In Logic Programming - 25th International Conference, ICLP 2009, Proceedings. 2009. p. 417-431. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 5649 LNCS). https://doi.org/10.1007/978-3-642-02846-5_34

Author

Hildebrandt, Thomas ; López, Hugo A. / Types for secure pattern matching with local knowledge in universal concurrent constraint programming. Logic Programming - 25th International Conference, ICLP 2009, Proceedings. 2009. pp. 417-431 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 5649 LNCS).

Bibtex

@inproceedings{ea5746979a19458aa8c120b2542ab9f6,
title = "Types for secure pattern matching with local knowledge in universal concurrent constraint programming",
abstract = "The fundamental primitives of Concurrent Constraint Programming (CCP), and , 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 (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.",
keywords = "Concurrent Constraint Programming, Mobility, Process Calculi, Security, Type systems",
author = "Thomas Hildebrandt and L{\'o}pez, {Hugo A.}",
year = "2009",
month = sep,
day = "14",
doi = "10.1007/978-3-642-02846-5_34",
language = "English",
isbn = "3642028454",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "417--431",
booktitle = "Logic Programming - 25th International Conference, ICLP 2009, Proceedings",
note = "25th International Conference on Logic Programming, ICLP 2009 ; Conference date: 14-07-2009 Through 17-07-2009",

}

RIS

TY - GEN

T1 - Types for secure pattern matching with local knowledge in universal concurrent constraint programming

AU - Hildebrandt, Thomas

AU - López, Hugo A.

PY - 2009/9/14

Y1 - 2009/9/14

N2 - The fundamental primitives of Concurrent Constraint Programming (CCP), and , 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 (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.

AB - The fundamental primitives of Concurrent Constraint Programming (CCP), and , 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 (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.

KW - Concurrent Constraint Programming

KW - Mobility

KW - Process Calculi

KW - Security

KW - Type systems

UR - http://www.scopus.com/inward/record.url?scp=69949138638&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-02846-5_34

DO - 10.1007/978-3-642-02846-5_34

M3 - Article in proceedings

AN - SCOPUS:69949138638

SN - 3642028454

SN - 9783642028458

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 417

EP - 431

BT - Logic Programming - 25th International Conference, ICLP 2009, Proceedings

T2 - 25th International Conference on Logic Programming, ICLP 2009

Y2 - 14 July 2009 through 17 July 2009

ER -

ID: 235144647