Steve Kremer: The P<span style="font-variant: small-caps;">rouvé</span> Manual: Specifications, Semantics, and Logics

The Prouvé Manual: Specifications, Semantics, and Logics

Steve Kremer, Yassine Lakhnech, and Ralf Treinen. The Prouvé Manual: Specifications, Semantics, and Logics. Technical Report 7, projet RNTL PROUVÉ, 2005. 49 pages.

Download

[PDF] [PS]

Abstract

In this report we describe the Prouvé specification language for cryptographic protocols. A main feature of the language is that it separates the roles of a protocol, which are defined in a simple imperative programming language, from the scenario which defines how instances of the roles are created.
We give a formal semantics of the protocol specification language, and define both an expressive logics for safety conditions of protocols and a more limited assertion language.
This version of the report (2.0.x) describes version 2.0 of the Prouvé language.

BibTeX

@techreport{Prouve:rap7,
  abstract =      {In this report we describe the {\scshape Prouv\'e}
                   specification language for cryptographic protocols. A
                   main feature of the language is that it separates the
                   roles of a protocol, which are defined in a simple
                   imperative programming language, from the scenario
                   which defines how instances of the roles are
                   created.\par We give a formal semantics of the
                   protocol specification language, and define both an
                   expressive logics for safety conditions of protocols
                   and a more limited assertion language.\par This
                   version of the report~(2.0.x) describes version~2.0
                   of the {\scshape Prouv\'e} language.},
  author =        {Kremer, Steve and Lakhnech, Yassine and
                   Treinen, Ralf},
  institution =   {projet RNTL PROUV{\'E}},
  month =         dec,
  note =          {49~pages},
  number =        {7},
  type =          {Technical Report},
  title =         {The {P}{\scshape rouv\'e} Manual: Specifications,
                   Semantics, and Logics},
  year =          {2005},
  nmonth =        {12},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Prouve-rap7.pdf},
}