Cryptographically sound analysis of security protocols [Elektronische Ressource] / eingereicht von Michael Backes

SSAATRIASVRCryptographically Sound Analysis ofSecurity ProtocolsDissertation zur Erlangung des GradesDoktor der Ingenieurwissenschaften (Dr.-Ing.)der Naturwissenschaftlich-Technischen Fakultat¨ Ider Universitat¨ des SaarlandesEingereicht von Michael BackesGutachter:Prof. Dr. Birgit PfitzmannProf. Dr. Harald GanzingerDekan:Prof. Dr. Philipp SlusallekKolloquium:Saarbruck¨ en, April 2002IEEVNISNIUSiAbstractIn this thesis, we show how formal methods can be used for the cryptographicallysound verification of concrete implementations of security protocols in order to obtaintrustworthy and meaningful proofs, and to eliminate human inaccuracies.First, we show how to derive secure concrete implementations of a given abstractspecification. The security proofs are essentially based on the well-established ap-proach of bisimulation which can be formally verified yielding rigorous proofs. As anexample, we present both a specification and a secure implementation of secure mes-sage transmission with ordered channels. Moreover, the example comprises a generalmethodology how secure implementation of arbitrary specifications can be obtained.Thereafter, we concentrate on the actual goals the protocol should fulfill. Thus, wedefine integrity properties in our underlying model and we show that logic derivationsamong them carry over from the specification to the concrete implementation, whichmakes them accessible for tool-assisted verification.