next up previous
Next: Formalizing Security Services Up: Background Previous: Managing Security Associations and

Mechanized Belief Logics

Belief logics[3] are designed to consider what conclusions individual parties (principals) in a communication dialogue can deduce based on messages received and a set of initial assumptions or beliefs. Logics devised to reason about cryptographic protocols generally consider only idealized protocols; there are no bit streams, but rather typed messages. Thus, all parties are presumed to recognize varying message formats, despite the lack of this information in the bit stream. Belief analysis attempts to show that only desired properties are guaranteed by the communication (data security, non-repudiation, no replayed transactions, etc).

Note that proofs about idealized protocols are not a guarantee that the concrete protocols are correct. There are many implementation assumptions that if invalid, would cause a secure, idealized protocol to actually be insecure. For example, these logics all assume that the cryptoalgorithm is secure.

Using the HOL system's type definition mechanisms, we define a number of application specific data types. HOL's recursive type definition facility [9] automates the process of defining new data types in terms of already existing types. Both new type constants and type constructors (operators) can be defined. Additional (recursive) functions can be defined to operate on the concrete data representation of the type. The properties of new types must be derived by formal proof. This guarantees that the type does not introduce inconsistency into the logic.

The SVO logic[13] defines a number of property predicates to describe the set of beliefs present in a system. This set may also include ``facts'' that may not be believed by all principals. Informally, a message can be received, but it may be encrypted. If a principal has the key, then the plaintext may be obtained. However, the principal has no assurance who the plaintext came from unless the message is signed. If a message is signed, then a principal can assume that the signing principal said the plaintext. But we don't know when the message was said, unless it is fresh, in which case, the principal can assume the signer effectively, says the message at the same time it is received (the message is timely, and thus not a replay). Still, the message may not come from an authority (e.g. ``Simon says'') unless the signer controls the message. If so, then whatever the message asserts is considered accurate.

Since performing proofs using only the above axioms is exceedingly tedious, we developed a collection of semi-automated tactics to simplify proof manipulations.


next up previous
Next: Formalizing Security Services Up: Background Previous: Managing Security Associations and