Provable Implementations of Security Protocols

for reasoning about abstract models of protocols. The work on informal methods attempts to discern common patterns in the extensive record of flawed protocols, and to formulate positive advice for avoiding each pattern [1, 2]. For example, Anderson and Needham propose an Explicitness Principle, that covers many classic errors: Robust security is about explicitness. A cryptographic protocol should make any necessary naming, typing and freshness information explicit in its messages; designers must also be explicit about their starting assumptions and goals, as well as any algorithm properties which could be used in an attack. [2] Much of the work on formal methods has depended on the powerful idea, introduced by Dolev and Yao [9], of idealizing cryptographic operations such as encryption and decryption as a symbolic algebra. After intense effort on symbolic reasoning, there are now several techniques [8, 7] for automatically proving properties of protocols represented within a symbolic,...

• Type: Conference
• Year: 2006
• Where: LICS
• Authors: Andrew D. Gordon
• Keywords: Computational Models, Computer Science, Informal Methods Attempts, LICS 2006, Symbolic Models