@InCollection{	  vigneron:high:2004,
  abstract	= {This paper presents HLPSL, a high-level protocol
		  specification language for the modelling of
		  security-sensitive protocols. This language has a formal
		  semantics based on Lamport s Temporal Logic of Actions.
		  HLPSL is modular and allows for the specification of
		  control flow patterns, data-structures, alternative
		  intruder models, and complex security properties. It is
		  sufficiently highlevel to be accessible to protocol
		  engineers (themselves not necessarily formal methods
		  experts), yet easily translatable into a lower-level
		  term-rewriting based language well-suited to model-checking
		  tools. The accommodation of these contrasting features
		  makes HLPSL able to easily specify modern, industrial-scale
		  protocols on which existing specification languages only
		  partially succeed.},
  author	= { Yannick Chevalier \and Luca Compagna \and Jorge Cuellar
		  \and Paul Hankes Drielsma \and Jacopo Mantovani \and
		  Sebastian M\"odersheim \and Laurent Vigneron},
  booktitle	= {Workshop on Specification and Automated Processing of
		  Security Requirements (SAPS 2004)},
  language	= {USenglish},
  pdf		= {papers/2004/0_paper.pdf},
  ps		= {papers/2004/0_paper.ps.gz},
  title		= {A High Level Protocol Specification Language for
		  Industrial Security-Sensitive Protocols},
  year		= 2004,
  user		= {moederss}
}