First-Order Verification of CryptographicProtocolsErnie CohenMicrosoft ResearchAbstractWe describ e a verification method for cryptographic protocols, basedon first-order invariants. For typical protocols, a suitable invariant can begenerated mechanically from the program text, allowing safety propertiesto be proved by ordinary first-order reasoning.The metho d has been implemented in an automatic verifier, TAPS,that proves safety properties comparable to those in published Isabelleverifications, but does so much faster with little or no guidance from theuser. TAPS has verified properties of about 80 protocols, including allbut three protocols from the Clark & Jacob survey; on average, theseverifications require less than a second of CPU time and less than 4 bytesof hints from the user.1 IntroductionA cryptographic protocol is a program that uses cryptographic primitives (e.g.,ciphers and hash functions), typically to implement distributed computing prim-itives (e.g., reliable messaging, shared memory) in a hostile communication en-vironment. These protocols are notoriously tricky; for example, bugs have beenfound in a number of published authentication protocols. The brevity and sub-tlety of these protocols make them an attractive target for formal methods.Most modern methods for verifying these protocols model them as concur-rent systems, consisting of a collection of principals following the rules of theprotocol along with an active adversary who controls all message delivery andcan generate new messages from old ones using a limited set of operations (typ-ically tupling, untupling, encryption, decryption, and nonce/key generation).Protocol properties (e.g. authentication) are then checked using conventionalprogram verification techniques. This approach seems to strike a good balancebetween the complexity-based proofs favored by cryptographers [3, 4] (whichcannot be produced for most existing protocols) and proofs in special-purposeauthentication logics [7, 11] (which are insensitive to many flaws of interest).A variety of verification techniques have been applied to the resulting concur-rent s ystems ; we give only some examples here. Model checkers have been usedto find bugs [15, 9], but combinatorial explosion in the number of sessions/rolesforces the models to be severely constrained, which can lead to misse d attacks1.Bounded-session techniques using symbolic traces and constraints (e.g. [6])suffer from the same problem2. Symbolic search tools like Athena [23] andRankanalyser [13] are much faster, and can often prove protocols correct with-out bounding the number of se ss ions, but depend on bounded message size3and structural limitations on the protocol4. Finally, approaches that use classi-cal program invariants (e.g. [21, 22, 17, 10]) handle unbounded message depthand protocol instances, but require judiciously chosen recursively defined setsof messages [18], and require substantial effort and proof-checking expertise.We present a very different approach to verifying protocols in the unboundedmodel, based on first-order invariants. Unlike other approaches, our invariantsare constructed without regard for the properties being checked. Nevertheless,suitable invariants can be constructed automatically for most protocols, allowingsafety properties to be proved with first-order reasoning.Our method is impleme nted in an automatic verifier, TAPS, that provessafety properties roughly equivalent to those proved in published Isabelle ver-ifications. However, TAPS generates these proofs quickly (typically around asecond or less), with almost no user guidance (none for 90% of our examples,an average of about 40 bytes each for the remaining ones). TAPS has verifiedabout 80 protocols, including almost all of the Clark & Jacob Survey (see sec-tion 5). TAPS can perform sophisticated mathematical reasoning on functionsand predicates as part of a verification process, a feature important for our longterm goal of analyzing systems in which cryptography is used as part of a largersecurity infrastructure. It can also handle recursive protocols to a limited ex-tent, and has verified protocols that use chains of certificates and hashes. Themain downside compared to search-based systems is that TAPS does not gen-erate counterexamples (although the failure of a proof obligation can provideinformation useful in the construction of such counterexamples).Although TAPS can verify many protocols quickly and fully automatically,we emphasize that TAPS searches for proofs, not attacks. The utility of TAPSlies not in its ability to find attacks that search tools miss, but in its ability toquickly find proofs that make such searches unnecessary.1For example, overconstraint caused Murphi to miss a serious bug in a rationalized recon-struction of SSL [20], a bug we found by trying to prove the protocol correct.2They do, however, handle unbounded message size.3These bounds can often be justified by strong typing, which can be added to most to mostprotocols using the tagging scheme of [12]. However, this doesn’t work for protocols that re-quire unbounded encryption depth (e.g. SK EY and paywords), and the additional explicitnessof type tagging can open up new avenues of attack (e.g., offline guessing attacks). Moreover,our experience TAPS shows that strong typing is rarely needed for protocol correctness.4For example, protocols must be loop-free (so they can’t handle recursive protocols, re-peated authentication, or certificate chains) and can’t test messages for inequality (so theycan’t handle protocols that use such tests to prevent replay or reflection attacks). Similarlimitations apply to verifiers based on monadic Horn theories, e.g. [25, 5]21.1 RoadmapWe model protocols as transition systems , where the state of the system isgiven by the set of transitions that have been executed and the set of messagesthat have been published (i.e., sent in the clear). A typical transition generatessome fresh values (to be used as nonces or keys), checks that some preconditionholds, records that the transition has taken place, and publishes a new message.Several implicit transitions model the actions of the spy, and the states of thesystem can be further re stricted by user-supplied axioms.From the protocol description, we generate a number of invariants. All butone of these is invariant by construction. The one exception is the secrecy invari-ant, which says that if a message is published, then either we
View Full Document
Unlocking...