BlanchetIPL05

Bruno Blanchet Back to publications

Bruno Blanchet. Security Protocols: From Linear to Classical Logic by Abstract Interpretation. Information Processing Letters, 95(5):473-479, September 2005.

Copyright

Links

An extended version is available, with an additional proof and some minor additions.

Information Processing Letters at Elsevier.

Abstract

We relate two models of security protocols, namely the linear logic or multiset rewriting model, and the classical logic, Horn clause representation of protocols. More specifically, we show that the latter model is an abstraction of the former, in which the number of repetitions of each fact is forgotten. This result formally characterizes the approximations made by the classical logic model.

Bibtex


@ARTICLE{BlanchetIPL05,
  AUTHOR = {Bruno Blanchet},
  TITLE = {Security {P}rotocols: {F}rom {L}inear to {C}lassical {L}ogic by {A}bstract {I}nterpretation},
  JOURNAL = {Information Processing Letters},
  YEAR = 2005,
  VOLUME = 95,
  NUMBER = 5,
  PAGES = {473--479},
  MONTH = SEP
}

E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)