Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Scientific Issues of Jan Długosz University in Częstochowa. Mathematics

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: protokoły uwierzytelniania kryptograficznego

Sortuj według:

Ogranicz wyniki do:

Verifying Untimed Version of the WMF Protocol Using networks of Autamata

Grondys K., Kurkowski M., Sowik A., Szczypior I.

Scientific Issues of Jan Długosz University in Częstochowa. Mathematics

2006

Vol. 11

51--58

In this paper we present some results of symbolic verification of untimed version of The Wide-Mouth Frog Protocol. This protocol is designed for achieving authentication between communicating sides in the computer network and exchange a new session cryptographic key. For our investigation we model executions of this protocol by a network of synchronized untimed automata. We investigate suitable protocols properties by testing reachablity of some distinguished states in the defined network. We use VerICS [5] - the symbolic model checker - for searching in our network.

A State Transition Model for Honest Executions of Authentication Protocols

Kurkowski M.

Scientific Issues of Jan Długosz University in Częstochowa. Mathematics

2005

Vol. 10

83-94

Cryptographic protocols are very good tools to achieve authentication in large distributed computer network. These protocols are precisely defined sequences of actions (communication and computation steps) which use some cryptographic mechanism such as encryption and decryption. It is well known that the design of authentication cryptographic protocols is error prone. Several protocols have been shown flawed in computer security literature. Due to this it is necessary to have some methods of analysis and properties verification of these protocols. It is obvious that in investigations of these properties a suitable formal model is needed. This model should express all important properties and ideas of protocols. Usually size of modeIs introduced by many people is very huge and searching of these modeIs is impossible. In this paper we propose a new formal model of honest executions of cryptographic authentication protocol. To decrease number of states in our model we propose some partial order reduction. We hope that this model is a good startpoint for further investigations and will be usefull in verification of real executions of cryptographic protocols.