|
 |
|
|||||
|
|||||||
|
Verification of Cryptographic Protocols used in Fixed and Mobile Networksby Tom Coffey, Reiner Dojen and Tomas Flanagan The research undertaken by the Data Communications Security Laboratory at the University of Limerick includes: cryptographic algorithms and protocols for open hostile environments, non-repudiation protocols, global-wide identification, authentication and access control schemes, formal verification of security protocols using logical techniques and the developing area of steganography and information hiding. Network security encompasses cryptographic protocols and algorithms used to ensure secure communication in a hostile environment. Such secure communication is indispensable in areas such as Internet, e-commerce and mobile communications. Fixed and mobile networks are vulnerable to a variety of attacks, such as message replay, parallel session, data interception and/or manipulation, repudiation and impersonation. Before trusting security protocols, it is necessary to have some degree of assurance that they fulfil their intended objectives. Traditionally, general-purpose cryptographic protocols have been designed and verified using informal and intuitive techniques. However, the absence of formal verification of these protocols can lead to flaws and security errors remaining undetected. For example, the public-key authentication protocol of Needham and Schroeder was considered secure for over a decade. Verification of the Needham-Schroeder protocol using formal logics exposed vulnerability to replay attacks in this protocol. This highlights the fact that even comparably simple protocols are difficult to verify by intuitive techniques. Formal verification aims at providing a rigid and thorough means of evaluating the correctness of a cryptographic protocol so that even subtle defects can be uncovered. Protocol verification methods include state space searching, the use of process algebras and logic-based analysis. Unfortunately, these formal verification methods are highly complex and cannot be easily applied by protocol designers. The work undertaken by the Data Communications Security Laboratory at the University of Limerick includes the development of a logical technique, which can be used to reason about public-key cryptographic protocols. The technique combines the modal logics of knowledge and belief. Axioms are used to model the low-level properties of cryptographic communication systems such as: (i) data encryption and decryption, (ii) the transmission and reception of network data and (iii) the inability of a principal to decrypt a message without knowing the appropriate private key. These properties can be combined using inference rules to allow analysis of a wide range of public-key cryptographic protocols. The constructs of the logic are general purpose, enabling users deduce their own theorems, thus allowing for increased flexibility.
Protocol validation using this logic can be accomplished by deductive reasoning based on the application of valid rules of inference to sets of valid axioms. Once the logical syntax, rules of inference and axioms have been specified, the deduction process proceeds as follows:
It is important that the protocol goals be correctly formulated. If the desired goals have not been achieved, then this generally points to a missing hypothesis in the protocol assumptions or the presence of some protocol flaw. If a protocol goal is inaccurate or unaccounted for, then the verification cannot succeed. In this way, a formal analysis not only assesses the reliability of a protocol, but also compels a designer to formally and unambiguously state the protocol assumptions and desired goals. Future work is aimed at developing a tool-suite to simplify the formal verification process because current techniques are highly complex and their application is error prone. Major components in this work include:
Such a formal verification tool will offer communication security protocol designers, for both fixed and mobile networks, a significant advantage in the world ICT marketplace. It will enable them to prove the security and trustworthiness of the cryptographic communication protocol at an early stage of its design. Designers will then be able to prove, and improve, the security of the cryptographic protocols before the implementation phase begins, thereby reducing costs and increasing productivity. In addition this formal verification will significantly add user confidence to the end product. In the current economic climate, where security poses a most serious obstacle to the continued growth of e-commerce and m-commerce, the requirement that security protocols be formally verified cannot be overstated. Link: |
