Set-pi: Set Membership Pi-calculus

Add to your list(s) Download to your calendar using vCal

• Alessandro Bruni (Technical University of Denmark)
• Thursday 16 April 2015, 11:00-12:00
• Room 245, School of Computer Science.

If you have a question about this talk, please contact Gurchetan Grewal.

Communication protocols often rely on stateful mechanisms to ensure certain security properties. For example, counters and timestamps can be used to ensure authentication, or the security of communication can depend on whether a particular key is registered to a server or it has been revoked. ProVerif, like other state of the art tools for protocol analysis, achieves good performance by converting a formal protocol specification into a set of Horn clauses, that represent a monotonically growing set of facts that a Dolev-Yao attacker can derive from the system. Since this set of facts is not state-dependent, the category of protocols of our interest cannot be precisely analysed by such tools, as they would report false attacks due to the over-approximation.

We present Set-pi, an extension of the Applied Pi-calculus that includes primitives for handling databases of objects, and propose a translation from Set-pi into Horn clauses that employs the set-membership abstraction to capture the non-monotonicity of the state. Furthermore, we give a characterisation of authentication properties in terms of the set properties in the language, and showcase our method with two examples, a simple authentication protocol based on counters, and key registration protocol.

This talk is part of the Computer Security Seminars series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Computer Security Seminars
• Room 245, School of Computer Science
• computer sience

Note that ex-directory lists are not shown.