Loading...
Please wait, while we are loading the content...
Similar Documents
Analysis of cryptographic protocols using logics of belief: an overview
| Content Provider | Semantic Scholar |
|---|---|
| Author | Monniaux, David |
| Copyright Year | 2002 |
| Abstract | When designing a cryptographic protocol or explaining it, one often uses arguments such as “since this message was signed by machine B, machine A can be sure it came from B” in informal proofs justifying how the protocol works. Since it is, in such informal proofs, often easy to overlook an essential assumption, such as a trust relation or the belief that a message is not a replay from a previous session, it seems desirable to write such proofs in a formal system. While such logics do not replace the recent techniques of automatic proofs of safety properties, they help in pointing the weaknesses of the system. In this paper, we present briefly the BAN (Burrows – Abadi – Needham) formal system [9, 10] as well as some derivative. We show how to prove some properties of a simple protocol, as well as detecting undesirable assumptions. We then explain how the manual search for proofs can be made automatic. Finally, we explain how the lack of proper semantics can be a bit worrying. |
| Starting Page | 57 |
| Ending Page | 67 |
| Page Count | 11 |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.nit.eu/czasopisma/JTIT/2002/4/57.pdf |
| Alternate Webpage(s) | http://www.di.ens.fr/~monniaux/biblio/Monniaux_JTIT02.pdf |
| Alternate Webpage(s) | http://www.itl.waw.pl/czasopisma/JTIT/2002/4/57.pdf |
| Alternate Webpage(s) | http://www-verimag.imag.fr/~monniaux/biblio/Monniaux_JTIT02.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
