Formal verification logic for hybrid security protocols

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 30 mobile systems. These include the ASPeCT and Boyd-Park security protocols. These protocols use a public key algorithm to exchange a secret session key for use with a 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 perform 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, which was designed to verify 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.