article · 2003

Encryption as an abstract data-type: An extended abstract

Dale Miller

Cited by 0Abstract and details only

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 wellknown 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.

Cite this paper

APA 7

Miller, D. (2003). Encryption as an abstract data-type: An extended abstract.

MLA 9

Miller, Dale. “Encryption as an abstract data-type: An extended abstract.” 2003.

Chicago

Miller, Dale. 2003. “Encryption as an abstract data-type: An extended abstract.”

Harvard

Miller, D. (2003) ‘Encryption as an abstract data-type: An extended abstract’.

BibTeX

@article{miller2003encryption,
  title = {{Encryption as an abstract data-type: An extended abstract}},
  author = {Miller, Dale},
  year = {2003}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.