Our specification language defines the security properties, including authentication, secrecy and other properties related to electronic commerce. The system requirements are specified as a metric function and a specification of the initial setup. The initial system configuration defines which cryptographic primitives are available to the principals and what keys each principal possesses. For example, in a PKI environment, all protocol parties know their own private key and the public keys of the other principals, whereas in a symmetric-key environment the principals have shared secret keys. Hybrid systems are also possible.
The metric function corresponds to the cost or overhead of the protocol. An example for metric design is to make the metric correspond to the time overhead of the protocol. In a system such as a smart-card, encryption can be fast while the bandwidth between the card and the card reader may be low, in which case the metric function specifies a low cost for encryption, whereas the cost of sending and receiving messages is high.
The metric function is required to be monotonically increasing as the protocol complexity is increasing. This requirement is necessary during the protocol generation phase, where all the protocols up to a maximum cost threshold are generated.
The metric function defines an ordering among the protocols generated. The
screener analyzes the protocols in the order of increasing cost,
hence the first correct
protocol has a minimal cost-value with respect to the metric function. Given a
specification of security properties and system requirements, we say
that a protocol
is optimal if it has the lowest cost-value with respect to
the metric function among protocols that satisfy the security properties and the
system requirements.