CWI Cryptology Group

Abstract: We relate a Dolev Yao model with a realistic computational model. In particular, we extend the original work of Abadi and Rogaway by considering encryption with composed keys as opposed to atomic keys.

Abstract: Anonymizing protocols do not try to keep the contents of messages secure, but try to hide the mere fact that communication takes place. A sufficiently capable attacker could discover this mere fact by investigation relations between otherwise random looking messages. For instance, if A sends an encrypted message m and B sends the message h(m), an eavesdropper E could infer that A and B are communicating even if E cannot discover the meaning of the message m itself. Now, proving an anonymizing protocol correct from the formal method point of view is one thing, another thing is to analyze what this correctness means for a real implementation. In an Abadi-Rogaway / Micciancio-Warischi fashion, we analyze the relation between the world of algebraic messages and the world of bit string messages, taking care of possible relations between messages in both worlds, and prove soundness and completeness of an appropriate semantic interpretation of messages.

Abstract: This is an overview over simulatability in general, and certain pitfalls that arise with this security notion. Furthermore, some existing and potential relations to the formal methods community are sketched.

Abstract: I plan to talk about liveness issues in the formal verification of security protocols and a modified Dolev-Yao intruder suitable for checking them. I might also find some time to mention a couple of case studies.