Antti Huima (antti.huima@hut.fi) -
Tuomas Aura (tuomas.aura@hut.fi)
Helsinki University of Technology, Finland(note)
A log of cryptographic protocols are designed to work in situations where the participants of the protocols have different, or even conflicting, interests. These conflicts must be taken into account when the protocols are developed in order to avoid pitfalls. More generally, it must be ensured that the rights of the different parties can be protected. Usually, the rights and protecting them are included in the underlying goals of a protocol. However, no formal method of examining them do exist. In this paper we propose a formal method that can be used to analyse situations involving conflicting interests and rights to be protected. The method is based on a standard multimodal logic S4n. With the logic, we formalize and validate reasoning done in protocol design. As an example we analyse a secret election protocol appeared in the literature.
A lot of cryptographic protocols hare designed to work in situations where the participants of the protocols have different, or even conflicting, interests. Various specialized cryptographic protocols put extra emphasis on ensuring fairness to all involved parties in such situations. For example, designers of electronic payment schemes have to consider the interests of banks, customers, merchants, national banks and economies and law-enforcement agencies. Similarly, specialized digital signature systems must guarantee different properties to signers, verifiers and law-enforcement. Nevertheless, there is no general framework for representing and analysing the conflicting interests.
When systematic proof techniques and automatic verification tools for cryptographic protocols are reaching the level where the actually will be used by protocol developers, it is especially important that the verified properties correspond to the application requirements. That is why we believe that more insight into the derivation of the design goals and the relationships between the formal requirements is needed.
In this paper we present a formal method that can be used to express conflicting interests and to analyse situations that involve them. With the logic, we formalize and validate reasoning done in protocol design. The method that we use is based on a standard multimodal logic known S4n, applied to the current problem domain. We use both propositional and first-order versions of the logic.
This paper is structured as follows.
A propositional modal logic with only one modality is obtained from standard propositional calculus by adding to the language a unary operator 1 (pronounced ``box''); it is the modality operator . Different axioms can be given. Often these axioms reflect the interpretation of the modality. For example, if is read as ``necessarily '' then the following axiom:
makes sense. It says that if something is necessarily true, then it is true. On the other hand, interpreting as ``it is believed that '', the axiom above is questionable. For it is possible to believe something that is not true.
Different sets of axioms create different modal logics. Some of the logics are given standard names. For example, the logic that obeys the three modal axioms
is given the standard name S4.
Both Hilbert-style and tableaux-style proof methods exist for modal logics.
Multimodal logics are modal logics that have more than one modality. Relevant to us is the multimodal logic S4n where every modality independently obeys (1)-(3).
Cryptographic protocols are often used in situations where the protocol is meant to ensure protection of the rights of the participating entities. For instance,
These issues have been addressed, at least partially, in existing protocols--but on a per case basis. Although formal proofs have been presented about the workings of protocols, the discussion of high-level properties pertaining to the protection of rights have been informal and not well studied.
This is a problem, because the ultimate goals of the protocol are unclearly stated. Technical results of what a protocol achieves can be given and proven using existing methods. However, there is no apparatus for interpreting these results in a standard way. We want to present one here.
This is because by being able to demonstrate the real situation to anyone else she can claim justice for her.
We use to denote that ``A can demonstrate [to a third party]'' (from now on we shall drop ``[to a third party]'' out). In fact, we shall make a modality for every entity p in the system.
Definition 2676
Let be a set of participants. We are interested in the following multimodal logic:
This definition, though lacking rigor, defines a standard multimodal logic called S4n. Because the binding we make to the set of participants , we denote any specific instanse of the logic by .
We assume that the set is finite. For this reason we may use the notations and in the apparent sense (i.e. quantify over participants or modalities). We will also use n-ary predicates, computable functions and equality operator where necessary.
We need to make proofs in our logic. The example proofs in this paper will be Hilbert-style. We will use short hand markings in our proofs and use well-established deduction rules in addition to the two basic deduction rules, Modus Ponens(note) and Necessitation(note).(note) S4n is shown to be decidable in [HM92]. Tableaux-based proof methods are quite complicated to systematize, but exist however.
We must, of course, give some justification to the axioms we have just presented, remembering the interpretation that we just gave for the modalities--demonstrability. We will first consider the three modal axiom schemas and then discuss a problem that inavoidably appears.
.
This
is the basic axiom of all frame based modal logics, to which S4
belongs. When we interpret the modality in this axiom in the way
suggested above, we read: ``If p can demonstrate that Y is
necessarily true when X is, then if p can additionaly demonstrate
X, he can demonstrate Y also.'' If I can prove that Y
follows from X and that X is true, then I have just shown that Y
must be true also, despite of the interpretation of the subclauses X
and Y. For this reason we see that this axiom captures an essential
aspect of demonstrability.
.
We claim that X cannot be false if someone
is able to prove X, which is what this axiom captures. This
implication is inherent in our choice of the interpretation of the
modality. Namely, you cannot prove a thing that does not hold!
For this reason we see that this notion is also a part of the concept
of demonstrability.
If the assumptions we make about a system are not consistent this axiom has especially great potential to be the cause of contradictory derivations. We assume that our notion of provability has the property captured by this axiom. Thus we must ensure ourselves that the assumptions we make do not enable anyone to prove anything that should be false. In our examples this consisteness requirement is quite easily seen to hold.
.
The last axiom claims,
that everyone who is able to prove X, despite of the interpretation
of X, is also able prove that he/she is able to prove that. This
makes sense because by giving the proof of X, the ability to
prove X is undeniably demonstrated.
The problem of logical omniscience. This wording is used to refer to a difficulty that appears inevitably in logics like the one we use due to the Necessitation rule, though originally it refers to logics of knowledge [FHMV95]. Namely, if X is always true (it is, for example, a tautology), then we get using Necessitation . In essence, all participants must be able to prove all universally true clauses to a third party, despite of the possible complexity of the proofs. This however, turns out not to be a problem in our practical applications.
In modal logics there are two kinds of true formulas: those that are locally and those that are globally true. In our application the locally true formulas will represent facts that hold but that cannot be necessarily proven by anyone. The globally true formulas are facts that can be necessarily proven by everyone.
Our proposed analysis process goes as follows:
Having referred to critical situations above we now define them.
Definition 2722 (Critical situation)
A certain situation is critical for A if, when in the situation, A needs to be able to know that the situation holds and to prove that. In particular, critical situations include situations where
For example, assume that you have bought a new car and find after two weeks that there is no gear box in the vehicle. This is a critical situation for you, as the seller has cheated. It does not help you much to only know that the gear box is missing, you must also be able to show that it is missing and that you paid for it in order to get justice.
On the other hand, assume that you paid only for the car, but suddenly you find that there are is also a brand new stereo rack mounted in the car which you didn't paid for. This is not a critical situation for you per se because your rights are not being deprived by you receiving a free rack. You do not need to be able to prove that you have a free rack.(note)
The main point of critical situations is that when in one, an entity must be able to prove that the situation really holds. This the subject of the next subsections.
Definition 2726 (Critical Pair)
Let denote a situation that is critical for p. Then the pair is a critical pair.
Definition 2734 (Mapping)
Let denote all clauses of an logic. We define the mapping as
For we use to denote
maps critical pairs into clauses that, when true, guarantee that when ever in a critical situation, the participants concerned can demonstrate it. This is exactly what we discussed in the previous section.
We can now define our method more formally.
Let , a set of critical pairs, and , containing rules describing the system at hand, be given.
Definition 2742 (Solution)
Let . is a solution of iff
Thus, if a set of clauses is a solution for , then the following holds: if is true in addition to , then all participants' rights can be protected in the sense defined previously (they can demonstrate, giving a proof, that their rights are being dishonored if that is the case). We want to separate from for clarity; can contain different assumptions about the behaviour of the participants etc. that cannot be taken directly to be properties of a protocol being examined. However, no theoretical difference between the two types of premises exists.
It appears that such deductions as ``if A has payed the bill, she must have a receipt'' occur often in applications. However, this kind of thinking suffers of some inconsistency when stated formally. We would like to translate the clause above to the form
This has the contraposition
But this appears to lead to inconsistent results, if A has paid the bill but for some reason has lost the bill. Namely, she has indeed paid the bill, although the logic claims otherwise. For this reason we need sometimes to assume that such situations do not take place. Another solution would be to model these exceptions also, but it would lead to unnecessary complications. The same assumptions must be made in any traditional paper-based system: lost certificates may lead to contradictory results.
The crucial assumption is (5), and it must be discussed. Namely, it formalizes the argument that if B is able to prove and it is beneficial for him to do so, then he will exhibit a proof. Or, when B is asked to give a proof but he does not, it is concluded that B cannot give a proof. This is quite commonsense in everyday life. For example, a contract may contain wording such as: ``A receipt must be presented in two weeks of the request. In the case of failure to do that, the receipt is assumed not to exist.'' For this reason we will use this rule when necessary, though giving a comment when it is used.
In this example we consider a situation that takes place between a phone user U and a phone company C. The user subscribes to telecommunication services provided by the company. We have three predicates:
Note that we are just talking about ``a call'' and not making any distinction between different calls. That is, we assume that every call is independently charged.
Naturally .
We assume that there exists the following relationship between the predicates: the user does not pay a call before he has dialled it. We assume also that both the user and the company are able to prove when the user is being charged. This is reasonable, because otherwise the bill has not much legal force. (Other relationships will later be added in the solution set .) We thus get
We proceed to define the critical pairs. From the user's point of view, the company should charge him only if he has made a call that is not yet paid. From the company's point of view, it should be able to charge the user always when this is the situation. From these two observations we get the set of critical pairs
From these we get the set of requirements :
We should then try to prove . This turns out to be impossible, however. The reason is that the parties cannot prove anything about the predicates and .(note)
We will now show that
is a solution of , i.e. that . Indeed,
(30) is equal with the first requirement. The second requirement is proved using a similar argument. Note that actually (15) (item of ) was not used at all.
The solution set can be interpreted as resulting from a contract of the form: ``the company must be able to demonstrate dialled call when requested. Otherwise all requests of charge will be declared void'', and similarly for the customer's paid bills. This is exactly the situation discussed in Sec. 4.8.
We analyse a modified version [Sal96,Sch96] of the Two-Agency Secret Election Protocol, proposed originally by Salomaa et al. [NSS91,Sal91].
The protocol goes as follows. There are two agencies: one for legitimizating the voters (L) and another for computing the votes (C). We have also a voter (A).
In the following we assume that L works honestly and correctly. Of course, if L were cheating voters could, for instance, get many identification numbers. This would break the whole system immediately. (L can be replaced by running an all-or-nothing-disclosure-of-secrets protocol with C [NSS91].)
Our analysis will concentrate on the rights of A, an individual voter.
We also make the following minor modification to the protocol. If somebody tries to vote multiple times with the same identification number the first vote sent is the one registered by C in Step 5. We change this to let C choose the vote to use from the many votes sent by the party instead.
At this point we will begin to use first-order modal logic, i.e. add predicates and quantifiers to the previously propositionally based logic we have used. (We use rigid designators [Fit93].) Incorporating predicate calculus into modal logics contains some subtleties due to the amount of choices available regarding to the interpretation of the semantics of the quantifiers.
We will use the following sets: is the set of possible identification numbers, is the set of possible secret identifications, is the set of possible voting strategies and is the set of voters.
The predicates that we have chosen to model the protocol are presented in Figure 5.2.3.
When we state these observations formally we get the following clauses :
We let .
We use also the derived predicates:
Here is true for a voter and an identification number if the voter has sent at least one triple using the identification number and the identification number is valid, i.e. granted by L. is true for an identification number if there exists no -pair that the voter had sent with the identification number and C had published in the protocol step 6. is true for a voter if there exists an identification number that the voter has used when sending at least one vote to C but none of the votes sent with the identification number do appear in the list.
is true for two -pairs when they have been sent using the same identification number. denotes the situation that two pairs are published that are . is true for a similar pair if nobody has sent it with a valid identification number. Finally, is true for a pair if it has been published but either does not have a legal sender or another published pair exists that has been sent with the same identification number.
Critical pairs for A are then
In essence, the situations where A's rights are in danger are those where her vote is ignored or modified (45) and those where illegal votes are counted (46).
We get then the requirements
Trying to prove , we get stuck. Starting from (45) and looking at the definition of , the first problem seems to be that A cannot prove that she has sent anything. Indeed, this is a problem in the protocol. Because A cannot prove that she sent a vote to C, C can claim that he never received it.
Another problem is that A cannot prove for any i.
Problems are encountered when examining (46) also. A has no way to prove -clauses, for example.
We thus see that the protocol as formalized above does not fulfil the requirements we stated as the critical pairs (45)-(46). This reflects real world problems and/or bad formalization.
We will now begin to revise the formalization and the assumptions concerning the system until we find a result that fulfils (45) and (46). We do this trying to get a better voting protocol.
We start from (45) and work top-down. We make first the assumptions (their interpretations will be discussed below)
(48) and (49) together ensure that (45) is handled:
Similarly we take care of (46) by assuming
Thus (48), (49), (57) and (58) together form a solution set of the system. What has been assumed? (48) states that A can demonstrate when appropriate that she has sent a triple with a legal identification number. (49) formalizes that A can show that none of the pairs sent by her in triples with an identification number are published in the public list. (57) claims that A can prove that a pair has no legal sender when that is the case, and (58) that she can always demonstrate, when appropriate, that the same identification number was used to make two counted votes.
We now see how the protocol can be modified to satisfy the first two of the four necessary assumptions, i.e. (48) and (49).
The straightforward (48) has actually a problem. Namely, if A does prove that she has sent a triple with i, then she reveals the connection between i and herself and the anonymousness of her vote is lost. We assume that a trusted third party can be used to mediate without disclosing A's identity. This is just a design choice we make; we could try to remove his problem by making another assumptions instead of (48). Similar problems appear with (49).
We must now examine how to implement (48) and (49).
(48) is clearly a consequence of
In order to be able to implement (59) we assume that the identification numbers granted to voters have certificates that include the intended user's name. (60) can be implemented by requiring C to send a signed certificate (receipt) of all the received messages to the senders.
Thus making these two changes to the protocol we can ensure (48). (49) is a bit more complicated as a non-existence must be proved. We accomplish this using an indirect proof, assuming:
Here (61) says that whenever something has been sent using a legal identification number, C is able to prove that; and A is able to prove that this holds. This can be implemented so that i's itself are public keys and every voter is sent a private key corresponding to the public one. The private keys are used to sign the triples. C receives the public keys in the list N, and L certifies this list. (62) is an instance of the situation presented in Sec. 4.8. A is able to demonstrate that C cannot prove when this is the case.
We will give a sketch of a proof that with these assumpions, (49) follows. It is straightforward to prove that whenever ,. This is based on (61). As this is commonly provable by all participants, we can let in particular A be able to prove that. From that the conclusion follows via a contraposition argument using (62).
We sum up what we have done at this point:
We find that the method we used was easy and intuitive to use and it helped us to find problems and examine solutions to them.
The main contribution of our work to the area of trustworthy security engineering is giving a language to formally argue about conflicting interests and protection of rights; and proposing an applicable method that forces one to examine the underlying assumptions of a protocol to a great detail.
It may be possible to use the logic here in conjunction with existing authentication logics such as BAN [BAN90]. This is an area that should be examined. More case studies are needed in order to weight the usefulness of the method. Making proofs by hand is currently very cumbersome. Lemmas and more intuitive notation for certain commonly occurring clauses should be developed. The details of using a first-order multimodal logic still needs more attention. The case studies show this to be a promising direction. However, research on this subject is still in a very preliminary phase. Finally, other methods for examining conflicting interests could be developed.