@InCollection{	  accorsi.ea:modal:2002,
  abstract	= {We introduce a multi-modal logic that combines
		  complementary features of authentication logics and
		  trace-based approaches. Our logic contains two kinds of
		  modalities: implicit belief, which formalizes the view of
		  an external agent reasoning about interleaved protocol
		  executions, and explicit belief, which uses awareness to
		  model the resource-bounded reasoning of the agents involved
		  in the executions. We employ these modalities to formalize
		  extensional and intensional specifications of protocols and
		  their properties, and use these formalizations to
		  characterize and reason about attacks. As an example, we
		  consider the Needham-Schroeder Public Key protocol and use
		  our logic to demonstrate the existence of the well-known
		  man-in-the-middle attack, and also show the equivalence of
		  our modal specification to one based on an interleaved
		  trace semantics.},
  author	= {Rafael Accorsi and David Basin and Luca Vigan{\`o}},
  booktitle	= {Proceedings of the Second International Workshop on
		  Security of Mobile Multiagent Systems (SEMAS-2002)},
  editor	= {Klaus Fischer and Dieter Hutter},
  language	= {USenglish},
  month		= {July},
  pages		= {1--11},
  pdf		= {papers/2002/ABVSEMAS02.pdf},
  ps		= {papers/2002/ABVSEMAS02.ps.gz},
  publisher	= {University Saarbr{\"u}cken},
  series	= {Research Report},
  title		= {Modal Specifications of Trace-Based Security Properties},
  year		= 2002
}