Peer-Reviewed Journal Details
Mandatory Fields
Newe, T; Coffey, T
2003
January
Computer Systems Science And Engineering
Formal verification logic for hybrid security protocols
Published
()
Optional Fields
formal methods verification logic hybrid security protocol 3G mobile
18
1
17
25
Hybrid cryptographic security protocols find applications in many areas of communications, none more demanding than in the mobile Security sector. In recent years a number of hybrid cryptographic security protocols have been proposed for Use with 3G mobile systems. These include the ASPeCT [1] and Boyd-Park [2] security protocols. These protocols use a public key algorithm to exchange a secret session key for use with it symmetric algorithm. thereby removing the need for ultra reliable key servers. In order to provide assurance that these protocols are verifiably secure and trustworthy it is necessary to perforin a formal verification on their design specifications. In this paper a formal modal logic is presented to enable hybrid cryptographic security protocols to be formally verified. This logic is based on the Coffey-Saidha logic [3], which was designed to verily public key based protocols only. The logic presented here is a substantial extension to the original. The new extended logic is used to formally verify the well-documented Needham-Schroeder key-distribution protocol in order to demonstrate the effectiveness and usefulness of the logic in the protocol verification arena. The Boyd-Park hybrid mobile security protocol is then formally specified and verified using this logic, and as a result of this verification a modification to the original protocol is suggested.
0267-6192
Grant Details