Provable Implementations of Security Protocols

10 years 7 months ago
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,...
Andrew D. Gordon
Added 12 Jun 2010
Updated 12 Jun 2010
Type Conference
Year 2006
Where LICS
Authors Andrew D. Gordon
Comments (0)