@Article{	  andova.ea:framework:2008,
  abstract	= {Automatic security protocol analysis is currently feasible
		  only forsmall protocols. Since larger protocols quite often
		  are composed ofmany small protocols, composi- tional
		  analysis is an attractive, butnon-trivial approach.We have
		  developed a framework for compositional analysis of a
		  largeclass of security protocols. The framework is intended
		  to facilitateautomatic as well as manual verification of
		  large structured securityprotocols. Our approach is to
		  verify properties of component protocolsin a multi-protocol
		  environment, then deduce properties about thecomposed
		  protocol. To reduce the complexity of
		  multi-protocolverification, we introduce a notion of
		  protocol independence and prove anumber of theorems that
		  enable analysis of independent componentprotocols in
		  isolation.To illustrate the applicability of our framework
		  to real-worldprotocols, we study a key establishment
		  sequence in WiMAX consisting ofthree subprotocols. Except
		  for a small amount of trivial reasoning, theanalysis is
		  done using automatic tools.},
  author	= {S. Andova and C.Cremers and K. Gjosteen and S. Mauw and S.
		  Mjolsnes and S. Radomirovic},
  journal	= {Information and Computation},
  language	= {USenglish},
  month		= 2,
  number	= {2-4},
  pages		= {425--459},
  title		= {A framework for compositional verification of security
		  protocols},
  volume	= 206,
  year		= 2008,
  user		= {cremersc}
}