Abstract:


A framework for compositional verification of 
security protocols

S. Andova and C.Cremers and K. Gjosteen and 
S. Mauw and S. Mjolsnes and S. Radomirovic

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.