English Russian
Journal Title
Scientific journal of the
theoretical and applied
researches
 The News of Altai State University
Print ISSN 1561-9443
On-line ISSN 1561-9451
Issues list
Content of 1-2(73) 2012
Management, Computer Facilities and Computer Science
Mathematics and Mechanics
Physics
 
1-2(73)2012
Management, Computer Facilities and Computer Science

Previous | Next
 
A.A. Lependin, A.V. Ubert

The Model Checking Method for the Authentication Protocols Analysis

The research shows some capabilities to use model checking method for cryptographic protocol verification. An approach to modeling interacting agents as an asynchronous parallel processes was illustrated on an example of Needham-Schr?eder protocol.
An example of formalization and properties verification by means of using linear temporal logic was given. The well-known vulnerability of Needham-Schr?eder protocol - Lowe attack - was found.
Key words: cryptographic protocol, authentication, model checking, linear temporal logic, automatic verification.

Full text at PDF, 157Kb. Language: russian.

Print Edition of "The News of Altai State University" copyright 1996-2012 Altai State University.
All rights reserved. Any of parts of a journal or edition as a whole cannot be reprinted without the written sanction of the authors or publisher. On purchase of a journal to address to ASU publishing house:
Altai State University. 656039, 66 Dimitrova street, Barnaul, Russia. Telephone + 7 (3852) 366351.