@InCollection{	  accorsi.ea:towards:2001,
  abstract	= {We report on work-in-progress on a new semantics for
		  analyzing securityprotocols that combines complementary
		  features of security logics andinductive methods. We use
		  awareness to model the agents' resource-boundedreasoning
		  and, in doing so, capture a more appropriate notion of
		  belief thanthose usually considered in security logics. We
		  also address the problem ofmodeling interleaved protocol
		  executions, adapting ideas from inductivemethods for
		  protocol verification. The result is an intuitive,
		  butexpressive, doxastic logic for formalizing and reasoning
		  about attacks. As acase study, we use awareness to
		  characterize, and demonstrate the existenceof, a
		  man-in-the-middle attack upon the Needham-Schroeder Public
		  Key protocol.This is, to our knowledge, not only the first
		  doxastic analysis of this attackbut also the first
		  practical application of an awareness logic. Even
		  thoughdefining the awareness sets of the agents, a task
		  that is left unspecified informal works on awareness
		  logics, turns out to be surprisingly subtle, initialresults
		  suggest that our approach is promising for modeling,
		  verifying andreasoning about security protocols and their
		  properties.},
  address	= {Amsterdam},
  author	= {Rafael Accorsi and David Basin and Luca Vigan{\`o}},
  booktitle	= {Post-CAV Workshop on Logical Aspects of Cryptographic
		  Protocol Verification},
  editor	= {Jean Goubault-Larrecq},
  language	= {USenglish},
  note		= {Electronic Notes in Theoretical Computer Science 55(1)},
  pdf		= {papers/2001/3_0_ABV01.pdf},
  ps		= {papers/2001/3_0_ABV01.ps.gz},
  publisher	= {Elsevier Science Publishers},
  num_pages	= 19,
  isbn		= 0444510699,
  title		= {Towards an awareness-based semantics for security protocol
		  analysis},
  year		= 2001
}