FCS'03 Preliminary Version

pages

English

Documents

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

pages

English

Ebook

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Publié par

chaeh

Nombre de lectures

Langue

English

Niveau: Supérieur
FCS'03 Preliminary Version Encryption as an abstract data-type: An extended abstract Dale Miller INRIA/Futurs & Ecole polytechnique, France Abstract At the Dolev-Yao level of abstraction, security protocols can be specified using mul- tisets rewriting. Such rewriting can be modeled naturally using proof search in linear logic. The linear logic setting also provides a simple mechanism for generat- ing nonces and session and encryption keys via eigenvariables. We illustrate several additional aspects of this direct encoding of protocols into logic. In particular, en- crypted data can be seen naturally as an abstract data-type. Entailments between security protocols as linear logic theories can be surprisingly strong. We also il- lustrate how the well-known connection in linear logic between bipolar formulas and general formulas can be used to show that the asynchronous model of com- munication 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. 1 Introduction When the topic of specifying and reasoning about security protocols attracts the attention of programming language researchers, it is common to find them turning to process calculi, such as CSP or the spi-calculus [27,18], automata, and even typed ?-calculus [29].

linear logic

security protocols

rewriting using

can easily

between roles

analyze security

proof theory comes

clause

rewriting

role clause

Voir

Publié par

chaeh

Nombre de lectures

Langue

English

FCS’03Preliminary Version

Encryption as an abstract datatype: An extended abstract

Dale Miller

INRIA/Futurs&Écolepolytechnique,France

Abstract At the Dolev-Yao level of abstraction, security protocols can be speciﬁed using mul-tisets rewriting. Such rewriting can be modeled naturally using proof search in linear logic. The linear logic setting also provides a simple mechanism for generat-ing nonces and session and encryption keys via eigenvariables. We illustrate several additional aspects of this direct encoding of protocols into logic. In particular, en-crypted data can be seen naturally as an abstract data-type. Entailments between security protocols as linear logic theories can be surprisingly strong. We also il-lustrate how the well-known connection in linear logic between bipolar formulas and general formulas can be used to show that the asynchronous model of com-munication 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.

Introduction

When the topic of specifying and reasoning about security protocols attracts the attention of programming language researchers, it is common to ﬁnd them turning to process calculi, such as CSP or the spi-calculus [27,18], automata, and even typedλProof search (that is, the foundations of logic-calculus [29]. programming), however, has a number of properties that are attractive when one attempts to specify and analyze security protocols. We list a few of these advantages here and devote the rest of this paper to develop these beneﬁts further. Formal analysis of security protocols is largely based on a set of assump-tions commonly referred to as the Dolev-Yao model [10], an abstraction that supports symbolic execution and reasoning. It has been observed in various places (for example, [9,4]) that this abstract can be realized well using mul-tiset rewriting. Given that it is well-known that proof search in linear logic provides a declarative framework for specifying multiset rewriting [12,15,4], a This is a preliminary version. The ﬁnal version will be published in Electronic Notes in Theoretical Computer Science URL:www.elsevier.nl/locate/entcs

Voir