Security by typing |
| |
Authors: | Mourad Debbabi Nancy Durgin Mohamed Mejri John C. Mitchell |
| |
Affiliation: | (1) Département dInformatique, Université Laval, Sainte-Foy, Quebec, Canada;(2) Panasonic Information and Networking Technologies Laboratory, Princeton, New Jersey, USA;(3) Computer Science Department, Stanford University, Stanford, California, USA |
| |
Abstract: | We present an approach for analyzing cryptographic protocols that are subject to attack from an active intruder who takes advantage of knowledge of the protocol rules. The approach uses a form of type system in which types are communication steps and typing constraints characterize all the messages available to the intruder. This reduces verification of authentication and secrecy properties to a typing problem in our type system. We present the typing rules, prove soundness of a type inference algorithm, and establish the correctness of the typing rules with respect to the protocol execution and intruder actions. The protocol specifications used in the approach can be automatically extracted from the conventional, informal cryptographic protocol notation commonly found in the literature. To validate the approach, we implement our algorithm in a tool called DYMNA, which is a practical and efficient environment for the specification and analysis of cryptographic protocols. |
| |
Keywords: | Cryptographic Protocols Type System Intruder abilities Authentication Secrecy Integrity |
本文献已被 SpringerLink 等数据库收录! |
|