Relating Process Algebras and Multiset Rewriting for Immediate Decryption Protocols - Computer Network Security - page 96

6 Conclusions
This paper shows how multiset rewriting theories (MSR P ) and process alge-
bras (PA P ) used to describe the large class of immediate decryption protocols
may be related. Indeed we show how to define transformations between MSR P
to PA P specifications of such a security protocol, whose semantics (based on
labeled transition systems) are proved to be related. The paper introduces a
correspondence relation based on what messages appear on the network and on
what messages the intruder knows. A direct consequence of this results is that
any confidentiality property established in one framework can automatically be
ported to the other. Moreover, since several forms of authentication among pro-
tocol participants may be formulated in terms of properties of what is sent to
the net or what is captured by the intruder, authentication results can also also
immediately transfered through our encodings.
Acknowledgments
We would like to thank the selection committee and attendees of the WITS'03
workshop where a preliminary version of this paper was presented [5]. Their
feedback gave us precious material for thought and led to the present revision,
which focuses on immediate decryption protocols, while the complications of the
general case are addressed in the technical report [4].
References
1. Abadi, M. and Blanchet, B.: Analyzing Security Protocols with Secrecy Types and
Logic Programs. ACM SIGPLAN Notices , 31(1):33-44, 2002. Proc. of the 29th
ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages
(POPL'02)
2. Abadi, M. and Gordon, A.D.: Reasoning about Cryptographic Protocols in the
Spi Calculus. In Proc. of CONCUR '97: Concurrency Theory, 8th International
Conference , volume 1243 of Lecture Notes in Computer Science . Springer-Verlag
(1997) 59-73
3. Abadi, M. and Gordon, A.D.: A Bisimulation Methods for Cryptographic Proto-
cols. In Proc. of ESOP'98 (1998)
4. Bistarelli, S., Cervesato, I., Lenzini, G., and Martinelli, F.: Relating multiset rewrit-
ing and process algebras for security protocol analysis. Technical report, ISTI-CNR,
2003. Available at http://matrix.iei.pi.cnr.it/˜lenzini/pub/msr.ps
5. Stefano Bistarelli, Iliano Cervesato, Gabriele Lenzini, and Fabio Martinelli: Re-
lating Process Algebras and Multiset Rewriting for Security Protocol Analysis.
In R. Gorrieri, editor, Third Workshop on Issues in the Theory of Security —
WITS'03 , Warsaw, Poland (2003)
6. Burrows, M., Abadi, M., and Needham, R.: A logic of authentication. In Proc. of
the Royal Society of London , volume 426 of Lecture Notes in Computer Science .
Springer-Verlag (1989) 233-271
7. Cervesato, I., Durgin, N.A., Lincoln, P.D., Mitchell, J.C., and Scedrov, A.: A Meta-
Notation for Protocol Analysis. In Proc. of the 12th IEEE Computer Security Foun-
dations Workshop (CSFW'99) . IEEE Computer Society Press (1999)