Analysis of Real-World Security Protocols in a Universal Composability Framework

Max Tuengerthal

ISBN 978-3-8325-3468-4
339 pages, year of publication: 2013
price: 45.00 €
Analysis of Real-World Security Protocols in a Universal Composability Framework
Security protocols employed in practice are used in our everyday life and we heavily depend on their security. The complexity of these protocols still poses a big challenge on their comprehensive analysis. To cope with this complexity, a promising approach is modular security analysis based on universal composability frameworks, such as Canetti's UC model. This appealing approach has, however, only very rarely been applied to the analysis of (existing) real-world protocols. Either the analysis was not fully modular or it could only be applied to idealized variants of the protocols.

The main goal of this thesis therefore is to push modular protocol analysis as far as possible, but without giving up on accurate modeling. Our main contributions in a nutshell:

  • An ideal functionality for symmetric key cryptography that provides a solid foundation for faithful, composable cryptographic analysis of real-world security protocols.
  • A computational soundness result of formal analysis for key exchange protocols that use symmetric encryption.
  • Novel universal and joint state composition theorems that are applicable to the analysis of real-world security protocols.
  • Case studies on several security protocols: SSL/TLS, IEEE 802.11i (WPA2), SSH, IPsec, and EAP-PSK. We showed that our new composition theorems can be used for a faithful, modular analysis of these protocols. In addition, we proved composable security properties for two central protocols of the IEEE standard 802.11i, namely the 4-Way Handshake Protocol and the CCM Protocol. This constitutes the first rigorous cryptographic analysis of these protocols.

While our applications focus on real-world security protocols, our theorems, models, and techniques should be useful beyond this domain.

cover cover cover cover cover cover cover cover cover
Table of contents (PDF)


  • cryptographic protocols
  • universal composability
  • modular security analysis
  • composition theorems with joint state
  • computational soundness of formal analysis


45.00 €
in stock

42.00 €
55.00 €
61.50 €

(D) = Within Germany
(W) = Abroad

*You can purchase the eBook (PDF) alone or combined with the printed book (eBundle). In both cases we use the payment service of PayPal for charging you - nevertheless it is not necessary to have a PayPal-account. With purchasing the eBook or eBundle you accept our licence for eBooks.

For multi-user or campus licences (MyLibrary) please fill in the form or write an email to