Loading...
Please wait, while we are loading the content...
Similar Documents
Verifying Secrecy by Abstract Interpretation
| Content Provider | Semantic Scholar |
|---|---|
| Author | Bozga, Liana Lakhnech, Yassine |
| Copyright Year | 2002 |
| Abstract | At the heart of almost every computer security architecture is a set of cryptographic protocols that use cryptography to encrypt and sign data. They are used to exchange confidential data such as pin numbers and passwords, to authentify users or to guarantee anonymity of participants. It is well known that even under the idealized assumption of perfect cryptography, logical flaws in the protocol design may lead to incorrect behavior with undesired consequences. Maybe the most prominent example showing that cryptographic protocols are notoriously difficult to design and test is the Needham-Schroeder protocol for authentification. It has been introduced in 1978 [19]. An attack on this protocol has been found by G. Lowe using the CSP modelchecker FDR in 1995 [13]; and this led to a corrected version of the protocol [14]. Consequently there has been a growing interest in developing and applying formal methods for validating cryptographic protocols [15, 7]. Most of this work adopts the so-called Dolev and Yao model of intruders. This model assumes idealized cryptographic primitives and a nondeterministic intruder that has total control of the communication network and capacity to forge new messages. It is known that reachability is undecidable for cryptographic protocols in the general case [10], even when a bound is put on the size of messages [9]. Because of these negative results, from the point of view of verification, the best we can hope for is either to identify decidable sub-classes as in [1, 21, 16] or to develop correct but incomplete verification algorithms as in [18, 12, 11]. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.lsv.ens-cachan.fr/~goubault/SECI-02/Final/actes-seci02/pdf/012-yassine.pdf |
| Alternate Webpage(s) | http://www.lsv.fr/~goubault/SECI-02/Final/actes-seci02/pdf/012-yassine.pdf |
| Alternate Webpage(s) | http://www.lsv.ens-cachan.fr/~goubault/SECI-02/Final/actes-seci02/ps/012-yassine.ps |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
