Formal Analysis of the Kerberos Authentication System
| dc.creator | Bella,Giampaolo | |
| dc.creator | Riccobene,Elvinia | |
| dc.date | 1997 | |
| dc.date.accessioned | 2024-02-06T12:49:10Z | |
| dc.date.available | 2024-02-06T12:49:10Z | |
| dc.description | The Gurevich's Abstract State Machine formalism is used to specify the well known Kerberos Authentication System based on the Needham-Schroeder authentication protocol. A complete model of the system is reached through stepwise refinements of ASMs, and is used as a basis both to discover the minimum assumptions to guarantee the correctness of the system and to analyse its security weaknesses. Each refined model comes together with a correctness refinement theorem. | |
| dc.format | text/html | |
| dc.identifier | https://doi.org/10.3217/jucs-003-12-1337 | |
| dc.identifier | https://lib.jucs.org/article/27445/ | |
| dc.identifier.uri | https://openrepository.mephi.ru/handle/123456789/7273 | |
| dc.language | en | |
| dc.publisher | Journal of Universal Computer Science | |
| dc.relation | info:eu-repo/semantics/altIdentifier/eissn/0948-6968 | |
| dc.relation | info:eu-repo/semantics/altIdentifier/pissn/0948-695X | |
| dc.rights | info:eu-repo/semantics/openAccess | |
| dc.rights | J.UCS License | |
| dc.source | JUCS - Journal of Universal Computer Science 3(12): 1337-1381 | |
| dc.subject | Formal Methods | |
| dc.subject | Security | |
| dc.subject | Protocol specification | |
| dc.subject | Refinement | |
| dc.subject | Protocol verification | |
| dc.subject | Key distribution protocol | |
| dc.subject | Gurevich's Abstract State Machine | |
| dc.subject | Kerberos. | |
| dc.title | Formal Analysis of the Kerberos Authentication System | |
| dc.type | Research Article |