The model follows the general simulatability approach of modern cryptography. A variety of network structures and trust models can be described, such as static and adaptive adversaries.
As an example of our specification methodology we provide the first abstract and complete specification for Secure Message Transmission, improving on recent results by Lynch, and verify one concrete implementation. Our proof is based on a general theorem on the security of encryption in a reactive multi-user setting, generalizing a recent result by Bellare et.al.
Category / Keywords: foundations / Publication Info: Full version of a paper accepted for the IEEE Symposium on Security and Privacy, Oakland, May 2001. Date: received 19 Dec 2000, revised 23 Feb 2001, revised 23 Feb 2001 Contact author: wmi at zurich ibm com Available format(s): Postscript (PS) | Compressed Postscript (PS.GZ) | BibTeX Citation Version: 20010223:142052 (All versions of this report) Short URL: ia.cr/2000/066 Discussion forum: Show discussion | Start new discussion