Workshop on
Foundations of Computer Security - FCS'03
Ottawa, Canada, 26-27 June 2003
Encryption as an abstract data-type: an extended abstract
Dale Miller (INRIA - France)
Abstract
At the Dolev-Yao level of abstraction, security protocols can be specified
using multisets rewriting. Such rewriting can be modeled naturally using
proof search in linear logic. The linear logic setting also provides a simple
mechanism for generating nonces and session and encryption keys via
eigenvariables. We illustrate several additional aspects of this direct
encoding of protocols into logic. In particular, encrypted data can be seen
naturally as an abstract data-type. Entailments between security protocols as
linear logic theories can be surprisingly strong. We also illustrate how the
well-known connection in linear logic between bipolar formulas and general
formulas can be used to show that the asynchronous model of communication
given by multiset rewriting rules can be understood, more naturally as
asynchronous process calculus (also represented directly as linear logic
formulas). The familiar proof theoretic notion of interpolants can also serve
to characterize communication between a role and its environment.