This paper describes how the Automatic Authentication Protocol Analyzer (AAPA) works to formally analyze two large commercial protocols, the main- and coin-sequence protocols developed by CyberCash, Inc. The paper sketches the AAPA's simple Interface Specification Language (ISL) and gives and discusses ISL specifications of the two protocols, specifications which the AAPA automatically confirms have their stated authentication properties. The paper also notes the strengths and limitations of an AAPA analysis, listing the types of protocol failure that such an analysis will and will not find, and describes other benefits from performing such an analysis, particularly correcting errors, omissions, and inconsistencies in informal program specifications and providing high-level overview documentation.
Determining whether cryptographic protocols are vulnerable to attacks that involve stopping, replaying, modifying, or falsifying messages is notoriously difficult. The number of possible attacks grows exponentially with the number of messages in a protocol, the number of fields in these messages, the number of algebraic properties modeled of the encryption functions used, and the number of possible simultaneous protocol runs.
These complexities have led many protocol analysts to consider only short, simple protocols and to leave out much of their detail in modeling them. This makes the analysis tractable, but divorces it from the questions protocol developers really want to have answered.
The Automatic Authentication Protocol Analyzer (AAPA) takes a different approach. It addresses only parts of the protocol failure problem, but addresses these parts quickly and automatically. The time it takes to analyze a protocol is only quadratic in the size of the protocol, so it can analyze huge protocols in a high level of detail. By being able to include these details, AAPA analyses acquire many of the virtues of formal methods in general, virtues that have nothing to do with protocol failure; they give precise high-level design overviews, force designs to be complete and consistent, and find many common errors.
The AAPA produces its analyses by taking specifications in a simple Interface Specification Language (ISL) [4], translating them into Higher Order Logic (HOL) [8] theories over a belief logic [1] extending the Gong, Needham, Yahalom belief logic [6,7], automatically constructing proofs [3] in this belief logic that the specifications have their included authentication properties, and translating descriptions of the proved and unproved goals back into ISL [2].
Because it uses a belief logic, the AAPA addresses only authentication failures, not nondisclosure failures. It considers only single executions of protocols, and does not model potentially exploitable "accidental" algebraic properties of the encryption and decryption functions used - for example, RSA encryption has the property, roughly speaking, that the encryption of a product is the product of the encryptions. Even so, its analyses suffice to identify needed trust assumptions and to detect many common instances of protocol failure arising from attacks involving replays and legitimate principals' inability to determine whether data is fresh or of an expected form [2,9].
This paper describes using the AAPA to analyze two complicated commercial protocols, the main- and coin-sequence protocols developed and used by CyberCash, Inc. of Reston, VA, one of the leading providers of secure Internet commercial services (see, for example, [5][SW1]). The main-sequence protocol allows for secure credit card purchases between mutually suspicious customers and merchants. The coin-sequence protocol provides for inexpensive processing of large numbers of small purchases by customers using money they have allocated for this purpose, from merchants handling such purchases from large numbers of customers. CyberCash requested Arca Systems, Inc. perform an independent analysis of these protocols[SW2]. CyberCash provided informal protocol design documents that described the formats and functions of the different messages exchanged in the protocols, and answered technical questions.
[SW3]The rest of this paper is organized as follows: Section 1 introduces ISL, giving enough information to make the ISL specifications of the main- and coin-sequence protocols understandable. Section 2 provides an overview of these specifications, pointing out noteworthy properties of the various types of data used and instances in which the specifications had to be written in particular ways to avoid limitations in the current AAPA implementation. Section 3 details and discusses the Main-sequence protocol, and Section 4 gives and discusses the Coin-sequence protocol. Section 5 describes the benefits of performing AAPA analyses of these protocols, and Section 6 gives conclusions.
The AAPA's Interface Specification Language (ISL) [4] follows standard notation, uses intuitive terminology, and is largely self-explanatory. The following descriptions of ISL constructs will suffice for obtaining a reasonable understanding of the two protocols' ISL specifications:
In stating assumed initial conditions or desired protocol properties, ISL uses the following predicates with their indicated informal meanings:
This section describes basic attributes common to both ISL specifications. It describes the atomic pieces of data used in both specifications and the assumptions made about them. It also describes the simplifications, other adaptations, and other potential inaccuracies in the two specifications.
The three principals involved in both protocols, as they are specified in this paper, are Wallet, CashRegister, and Gateway. These are collections of programs representing a customer, a merchant, and CyberCash, respectively.
The main-sequence protocol uses both RSA public-key encryption/decryption and DES symmetric-key encryption/decryption. The coin-sequence protocol uses only DES encyrption/decryption, primarily because it is computationally much less expensive than RSA encryption/decryption. Both protocols use the MD5 hash algorithm.
The Date and MerchantDate fields give not only the date, but also the time. They are used as timestamps, and sometimes used to infer that a message is fresh.
In the main-sequence protocol, there are many public keys for sending messages to Gateway, one for each CashRegister and Wallet. In messages to Gateway, CashRegister and Wallet use the indexes MerchantCyberKey and CyberKey to tell Gateway which of its public keys is being used. In the ISL specification, PKMerchantCyberKey and PKCyberKey are the keys indexed by MerchantCyberKey and CyberKey, respectively. In the main-sequence protocol, CashRegister and Wallet have the public keys PKCashRegister and PKWallet, respectively, but these are used only by Gateway.
In both protocols, there are symmetric-key keys that are used as shared secrets between Gateway and CashRegister or Gateway and Wallet. In the main-sequence protocol, these keys are conveyed to Gateway by encrypting them with appropriately chosen Gateway public keys.
In both protocols, all secure communication is actually with Gateway, though encrypted messages from Gateway to Wallet are sent through CashRegister. Both CashRegister and Wallet trust Gateway, but neither trusts the other.
The other data items in the protocols, typically irrelevant to protocol failure, involve things such as credit card data, price and currency-exchange data, response codes, and error messages. Their names describe them as adequately as they need to be understood here.
The ISL models incorporate the following simplifications:
ISL does not have an "X is involved in the same transaction as Y and agrees with Y about its details" predicate. Both specifications use assertions that X conveyed particular messages it was expected to convey in lieu of assertions using such a predicate.
The coin-sequence specification defines transaction keys, and assumes that they are shared secrets, in the initial conditions. The belief logic underlying the AAPA has no notion of a key-generation function, and no rules for inferring that the result of applying a key-generation function to a shared-secret master key and other data is itself a shared-secret key. Adding these things involves nontrivial additions to the AAPA's belief logic and to its proof-construction algorithms.
The coin-sequence specification puts session IDs and session indexes together, in order, at the end of lists containing them so that the AAPA will be able to show the pair is fresh. The AAPA's belief logic is not complete enough to deduce that a list must be fresh if a pair containing two things in that list is fresh, regardless of where or in what order the two parts of the pair occur. This possibility extends to any tuple of elements of any list considered in any order. It would be expensive to check for these possibilities, since there are so many of them, and this case might not arise often enough to make doing so worthwhile.
The coin-sequence specification defines MerchantAmount as a single piece of data, and defines functions to extract the currency and numerical value. The AAPA is currently unable to define abbreviations for pairs or lists.
The main-sequence protocol handles credit card purchases by Wallet from CashRegister. The following steps give an informal description of the protocol. Note that although CashRegister and Wallet both need to trust Gateway, neither needs to trust the other.
/*======================================================================
Main-sequence ISL specification
Revision $Id: main.isl,v 1.5 1997/01/21 01:46:39 shb Exp $
======================================================================*/
DEFINITIONS:
/* Name and give the basic functions of all data items */
PRINCIPALS:
CashRegister, Gateway, Wallet;
SYMMETRIC KEYS:
CashRegisterSessionKey, WalletSessionKey;
PUBLIC KEYS:
PKCashRegister, PKCyberKey, PKMerchantCyberKey, PKWallet;
PRIVATE KEYS:
^PKCashRegister, ^PKCyberKey, ^PKMerchantCyberKey, ^PKWallet;
OTHER:
Accepts, AcquirerRefDataOptional, ActionCode,
AddnlResponseDataOptional, Amount, AuthorizationCode, AvsInfoOptional,
BeginTransaction, CardCIdOptional, CardCityOptional,
CardCountryOptional, CardExpirationDate, CardName, CardNumber,
CardOtherFieldsOptional, CardPostalCodeOptional, CardPrefixOptional,
CardSalt, CardStateOptional, CardStreetOptional, CardType, CyberKey,
Date, DebuggingInfoOptional, DescriptionListOptional, EndTransaction,
Id, MerchantAmount, MerchantAmount2Optional, MerchantCcId,
MerchantCyberKey, MerchantDate, MerchantDba, MerchantLocationOptional,
MerchantMessage, MerchantOrderId, MerchantResponseCode,
MerchantSwMessageOptional, MerchantSwSeverityOptional,
MerchantSwVersion, MerchantTransaction, MerchantUrlOptional, Message,
Note, OrderId, Payload, PayloadNote, ProcessorErrorCodeFuture,
ReportFeeOptional, ResponseCode, ResponseDetailCodeFuture,
RetrievalReferenceNumberOptional, ServerDate,
ServerDateMerchantOptional, ServiceCategory, SwMessageOptional,
SwSeverityOptional, SwVersion, TerminalIdFuture, Transaction,
TransactionDescriptionOptional, TransactionOriginal,
TransactionStatusOriginal, Type, TypeOriginalOptional, UrlCancel,
UrlFail, UrlPayTo, UrlSuccess;
ENCRYPT FUNCTIONS:
Des, Rsa;
HASH FUNCTIONS:
MD5;
/* Define the encrypt/decrypt relationships */
Des WITH ANYKEY HASINVERSE Des WITH ANYKEY;
Rsa WITH PKCashRegister HASINVERSE Rsa WITH ^PKCashRegister;
Rsa WITH ^PKCashRegister HASINVERSE Rsa WITH PKCashRegister;
Rsa WITH PKCyberKey HASINVERSE Rsa WITH ^PKCyberKey;
Rsa WITH ^PKCyberKey HASINVERSE Rsa WITH PKCyberKey;
Rsa WITH PKMerchantCyberKey HASINVERSE Rsa WITH ^PKMerchantCyberKey;
Rsa WITH ^PKMerchantCyberKey HASINVERSE Rsa WITH PKMerchantCyberKey;
Rsa WITH PKWallet HASINVERSE Rsa WITH ^PKWallet;
Rsa WITH ^PKWallet HASINVERSE Rsa WITH PKWallet;
/* Define the assumed conditions before the protocol starts */
INITIALCONDITIONS:
CashRegister Received Des,Rsa,MD5; /* CashRegister functions */
CashRegister Received /* CashRegister keys */
^PKCashRegister, PKCashRegister, PKMerchantCyberKey,
CashRegisterSessionKey;
CashRegister Believes /* CashRegister key beliefs */
(PrivateKey CashRegister Rsa ^PKCashRegister;
PublicKey CashRegister Rsa PKCashRegister;
PublicKey Gateway Rsa PKMerchantCyberKey;
SharedSecret CashRegister Gateway CashRegisterSessionKey);
CashRegister Received /* CashRegister other data */
Accepts, DescriptionListOptional, MerchantAmount,
MerchantAmount2Optional, MerchantCcId, MerchantCyberKey, MerchantDate,
MerchantDba, MerchantLocationOptional, MerchantMessage,
MerchantOrderId, MerchantSwMessageOptional, MerchantSwSeverityOptional,
MerchantSwVersion, MerchantTransaction, MerchantUrlOptional, Note,
Payload, PayloadNote, RetrievalReferenceNumberOptional,
ServerDateMerchantOptional, TerminalIdFuture,
TransactionDescriptionOptional, Type, UrlCancel, UrlFail, UrlPayTo,
UrlSuccess;
CashRegister Believes /* CashRegister other beliefs */
(Fresh MerchantDate;
CashRegister Recognizes MerchantDate;
Trustworthy Gateway);
Gateway Received Des,Rsa,MD5; /* Gateway functions */
Gateway Received /* Gateway keys */
^PKCyberKey, ^PKMerchantCyberKey, PKCashRegister, PKCyberKey,
PKMerchantCyberKey, PKWallet;
Gateway Believes /* Gateway key beliefs */
(PrivateKey Gateway Rsa ^PKCyberKey;
PrivateKey Gateway Rsa ^PKMerchantCyberKey;
PublicKey CashRegister Rsa PKCashRegister;
PublicKey Wallet Rsa PKWallet);
Gateway Received /* Gateway other data */
AcquirerRefDataOptional, ActionCode, AddnlResponseDataOptional,
AuthorizationCode, AvsInfoOptional, DebuggingInfoOptional,
MerchantResponseCode, Message, ProcessorErrorCodeFuture, ResponseCode,
ResponseDetailCodeFuture, ServerDate, SwMessageOptional,
SwSeverityOptional;
Gateway Believes /* Gateway other beliefs */
(Fresh Date;
Fresh MerchantDate;
Gateway Recognizes Date;
Gateway Recognizes MerchantDate);
Wallet Received Des,Rsa,MD5; /* Wallet functions */
Wallet Received /* Wallet keys */
^PKWallet, PKCyberKey, PKWallet, WalletSessionKey;
Wallet Believes /* Wallet key beliefs */
(PrivateKey Wallet Rsa ^PKWallet;
PublicKey Gateway Rsa PKCyberKey;
SharedSecret Wallet Gateway WalletSessionKey);
Wallet Received /* Wallet other data */
Amount, CardCIdOptional, CardCityOptional, CardCountryOptional,
CardExpirationDate, CardName, CardNumber, CardOtherFieldsOptional,
CardPostalCodeOptional, CardPrefixOptional, CardSalt,
CardStateOptional, CardStreetOptional, CardType, CyberKey, Date, Id,
OrderId, ServiceCategory, SwVersion, Transaction;
Wallet Believes /* Wallet other beliefs */
(Fresh Date;
Fresh ServerDate; /* Needed for final Conveyed goal */
Wallet Recognizes Date;
Wallet Recognizes ServerDate; /* Needed for final Conveyed goal */
Trustworthy Gateway);
/* Define the steps of the protocol */
PROTOCOL:
1. CashRegister -> Wallet: /* PR1 */
Accepts, MerchantAmount, MerchantAmount2Optional, MerchantCcId,
MerchantOrderId, MerchantDate, MerchantSwVersion, Note, Payload,
PayloadNote, Type, UrlCancel, UrlFail, UrlPayTo, UrlSuccess,
MerchantSignedHashKey_ = MD5(PKCashRegister),
PayloadHash_ = MD5(Payload),
MerchantSignedHash_ =
{MD5(Accepts,
DatePR1_ = MerchantDate,
MerchantAmount, MerchantCcId, MerchantOrderId,
MerchantSignedHashKey_, Note, Type, UrlCancel, UrlFail,
UrlPayTo, UrlSuccess)
}Rsa(^PKCashRegister);
2. Wallet -> CashRegister: /* CH1 */
CyberKey, Date, Id, MerchantCcId,
MerchantDateOptional_ = MerchantDate,
MerchantSignedHashKey_, OrderId,
ServiceCategoryOptional_ = ServiceCategory,
Transaction, Type,
PrHash_ =
MD5(Accepts, Date, MerchantAmount, MerchantCcId, MerchantOrderId,
MerchantSignedHashKey_, Note, Type, UrlCancel, UrlFail,
UrlPayTo, UrlSuccess),
PrSignedHash_ = MerchantSignedHash_,
OpaqPrefixCH1_ = {WalletSessionKey}Rsa(PKCyberKey),
OpaqueCH1_ =
{Amount, CardCIdOptional, CardCityOptional, CardCountryOptional,
CardExpirationDate, CardName, CardNumber, CardOtherFieldsOptional,
CardPostalCodeOptional, CardPrefixOptional, CardSalt,
CardStateOptional, CardStreetOptional, CardType, SwVersion,
KeyCH1_ = MD5(PKWallet),
SignatureCH1_ =
{MD5(Amount, CardCIdOptional, CardCityOptional,
CardCountryOptional, CardExpirationDate, CardName,
CardNumber, CardOtherFieldsOptional, CardPostalCodeOptional,
CardPrefixOptional, CardSalt, CardStateOptional,
CardStreetOptional, CardType, CyberKey, Date, Id,
MerchantCcId, MerchantSignedHashKey_, OrderId, PrHash_,
PrSignedHash_, SwVersion, Transaction, Type)
}Rsa(^PKWallet)
}Des(WalletSessionKey);
3. CashRegister -> Gateway: /* CM1 */
CyberKey, MerchantCcId, MerchantCyberKey, MerchantDate,
MerchantTransaction, ServiceCategory, OpaqPrefixCH1_, OpaqueCH1_,
MerchantOpaqPrefixCM1_ =
{CashRegisterSessionKey}Rsa(PKMerchantCyberKey),
MerchantOpaqueCM1_ =
{Date, DescriptionListOptional, Id, MerchantAmount, MerchantDba,
MerchantLocationOptional, MerchantMessage, MerchantSignedHashKey_,
MerchantSwMessageOptional, MerchantSwSeverityOptional,
MerchantSwVersion, MerchantUrlOptional, OrderId, PrHash__,
PrSignedHash_, RetrievalReferenceNumberOptional,
ServerDateMerchantOptional, TerminalIdFuture, Transaction,
TransactionDescriptionOptional, Type,
MerchantKey_ = MD5(PKMerchantCyberKey),
MerchantSignatureCM1_ =
{MD5(CyberKey, Date, Id, MerchantAmount, MerchantCcId,
MerchantCyberKey, MerchantDate, MerchantTransaction, OrderId,
PrHash_, PrSignedHash_, ServerDateMerchantOptional,
Transaction, Type)
}Rsa(^PKCashRegister)
}Des(CashRegisterSessionKey);
4. Gateway -> CashRegister: /* CM6 */
MerchantCcId, MerchantTransaction, MerchantDate,
ServiceCategoryOptional_,
MerchantOpaqueCM6_ =
{AcquirerRefDataOptional, ActionCode, AddnlResponseDataOptional,
AuthorizationCode, AvsInfoOptional, CardCIdOptional,
CardCityOptional, CardCountryOptional,
CardExpirationDateOptional_ = CardExpirationDate,
CardNameOptional_ = CardName,
CardNumberOptional_ = CardNumber,
CardPostalCodeOptional, CardPrefixOptional, CardStateOptional,
CardStreetOptional,
CardTypeOptional_ = CardType,
Date, DebuggingInfoOptional, Id, MerchantMessage,
MerchantSignedHashKey_, MerchantSwMessageOptional,
MerchantSwSeverityOptional, OrderId, ProcessorErrorCodeFuture,
PrHash_, PrSignedHash_, MerchantResponseCode,
ResponseDetailCodeFuture, RetrievalReferenceNumberOptional,
ServerDate, TerminalIdFuture, Transaction, Type
}Des(CashRegisterSessionKey)
||(Wallet Conveyed SignatureCH1_),
OpaqueCM6_ =
{Amount, AuthorizationCode, CardCIdOptional, CardCityOptional,
CardCountryOptional, CardExpirationDateOptional_,
CardNameOptional_, CardNumberOptional_, CardOtherFieldsOptional,
CardPostalCodeOptional, CardPrefixOptional,
CardSaltOptional_ = CardSalt,
CardStateOptional, CardStreetOptional, CardTypeOptional,
MerchantDba, MerchantLocationOptional, MerchantUrlOptional,
Message, OrderId, ResponseCode, ServerDate, SwMessageOptional,
SwSeverityOptional, TransactionDescriptionOptional
}Des(WalletSessionKey)
||(CashRegister Conveyed MerchantSignatureCM1_);
5. CashRegister -> Wallet: /* CH2 */
Date, MerchantCcId, MerchantDate, MerchantMessage,
MerchantResponseCode, MerchantSignedHashKey_, MerchantSwVersion, Id,
PrHash_, PrSignedHash_, ServiceCategoryOptional_, Transaction, Type,
OpaqueCM6_;
/* Define the conditions the protocol steps are expected to produce */
GOALS:
3. Gateway Believes Wallet Conveyed SignatureCH1_;
Gateway Believes CashRegister Conveyed MerchantSignatureCM1_;
4. CashRegister Believes Gateway Conveyed MerchantOpaqueCM6_;
CashRegister Believes Wallet Conveyed SignatureCH1_;
5. Wallet Believes Gateway Conveyed OpaqueCM6_;
Wallet Believes CashRegister Conveyed MerchantSignatureCM1_;
The AAPA confirms that this specification meets all of its goals. Note that after step 3, Gateway has adequate reason to believe that CashRegister and Wallet are involved in the same transaction and agree about its details, that after step 4, CashRegister has adequate reason to believe these things, and that after step 5, Wallet has adequate reason to believe these things.
As noted in Section 3.3, for simplicity, the ISL specification given here shows only the case of a single Wallet making purchases from a single CashRegister. The generalization to many Wallets making purchases from a single CashRegister is straightforward. The ISL specification also assumes that all optional fields are present.
The coin-sequence protocol is in many ways similar to the main-sequence protocol. In both protocols, Wallet sends information to CashRegister, which forwards it to Gateway. Gateway debits the Wallet's account and credits the CashRegister's account, then sends information back to CashRegister to be forwarded to Wallet. The following are the main differences between the two protocols:
/*===================================================================
Coin-sequence ISL specification
Stephen H. Brackin
Revision $Id: coin.isl,v 1.5 1997/02/14 09:29:19 shb Exp $
===================================================================*/
DEFINITIONS:
/* Name and give the basic functions of all data items */
PRINCIPALS:
CashRegister, Gateway, Wallet;
SYMMETRIC KEYS:
PayeeSessionMasterKey, PayeeSessionSalt, PayerSessionMasterKey,
PayerSessionSalt, PayloadKey;
OTHER:
Accepts, CollectedAmount, Fee, ForeignExchangeOptional, MerchantAmount,
MerchantAmount2Optional, MerchantCcId, MerchantDate,
MerchantMessageOptional, MerchantOrderId, MerchantResponseCodeOptional,
MerchantSwVersion, MessageOptional, Note, OrderIdOptional, PayeeIndex,
PayeeSessionId, PayerIndex, PayerSessionId, Payload, PayloadNote,
ProblemOptional, RequestVersion, ResponseCode, ServiceCategory,
SubType, SubVersion, TypeCA1, TypeCA2, TypeCA3, TypeCA4, TypePR1,
UrlCancel, UrlFail, UrlPayTo, UrlSuccess, VersionCA1, VersionCA2,
VersionCA3, VersionCA4;
ENCRYPT FUNCTIONS:
Des;
HASH FUNCTIONS:
MD5;
OTHER FUNCTIONS:
ExtractCurrency,GenerateKey;
/* Define the encrypt/decrypt relationships */
Des WITH ANYKEY HASINVERSE Des WITH ANYKEY;
/* Define the assumed conditions before the protocol starts */
INITIALCONDITIONS:
CashRegister Received /* CashRegister functions */
Des, GenerateKey, MD5;
CashRegister Received /* CashRegister keys */
PayeeSessionMasterKey, PayeeSessionSalt, PayloadKey;
CashRegister Believes /* CashRegister key beliefs */
(SharedSecret CashRegister Gateway PayeeSessionMasterKey;
SharedSecret CashRegister Gateway PayeeSessionSalt;
SharedSecret CashRegister Wallet PayloadKey);
CashRegister Received /* CashRegister other data */
Accepts, MerchantAmount, MerchantAmount2Optional, MerchantCcId,
MerchantDate, MerchantMessageOptional, MerchantOrderId,
MerchantResponseCodeOptional, MerchantSwVersion, Note, PayeeIndex,
PayeeSessionId, Payload, PayloadNote, SubType, SubVersion, TypeCA2,
TypeCA4, TypePR1, UrlCancel, UrlFail, UrlPayTo, UrlSuccess, VersionCA2,
VersionCA4;
CashRegister Believes
(Fresh PayeeSessionId,PayeeIndex;
CashRegister Recognizes Fee;
Trustworthy Gateway;
SharedSecret CashRegister Gateway /* See Section 3.4. */
PayeeTransactionKey_ =
GenerateKey(PayeeIndex,PayeeSessionMasterKey,TypeCA2,VersionCA2)
From CashRegister);
Wallet Received /* Wallet functions */
Des, ExtractCurrency, GenerateKey, MD5;
Wallet Received /* Wallet keys */
PayerSessionMasterKey, PayerSessionSalt;
Wallet Believes /* Wallet key beliefs */
(SharedSecret Wallet Gateway PayerSessionMasterKey;
SharedSecret Wallet Gateway PayerSessionSalt);
Wallet Received /* Wallet other data */
OrderIdOptional, PayerIndex, PayerSessionId, ServiceCategory, TypeCA1,
TypeCA3, VersionCA1, VersionCA3;
Wallet Believes /* Wallet other beliefs */
(Fresh PayerSessionId, PayerIndex;
Wallet Recognizes PayerIndex;
Trustworthy Gateway;
SharedSecret Wallet Gateway /* See Section 3.4. */
PayerTransactionKey_ =
GenerateKey(PayerIndex,PayerSessionMasterKey,TypeCA1,VersionCA1)
From Wallet);
Gateway Received /* Gateway functions */
Des, ExtractCurrency, GenerateKey, MD5;
Gateway Received /* Gateway keys */
PayeeSessionMasterKey, PayeeSessionSalt, PayerSessionMasterKey,
PayerSessionSalt;
Gateway Believes /* Gateway key beliefs */
(SharedSecret Gateway CashRegister PayeeSessionMasterKey;
SharedSecret Gateway CashRegister PayeeSessionSalt;
SharedSecret Gateway Wallet PayerSessionMasterKey;
SharedSecret Gateway Wallet PayerSessionSalt);
Gateway Received /* Gateway other data */
CollectedAmount, Fee, ForeignExchangeOptional,
MerchantCcId, /* Needed to check signature from Wallet */
MessageOptional, ProblemOptional, ResponseCode, RequestVersion,
TypeCA1, /* Needed; not forwarded as part of CA2 */
TypeCA3,
VersionCA1, /* Needed; not forwarded as part of CA2 */
VersionCA3;
Gateway Believes
(Fresh PayeeSessionId, PayeeIndex;
Fresh PayerSessionId, PayerIndex;
Gateway Recognizes PayeeIndex;
Gateway Recognizes PayerIndex;
SharedSecret Gateway CashRegister PayeeTransactionKey_;
SharedSecret Gateway Wallet PayerTransactionKey_);
/* Define the steps of the protocol */
PROTOCOL:
1. CashRegister -> Wallet: /* PR1 */
Accepts, MerchantAmount, MerchantAmount2Optional, MerchantCcId,
MerchantOrderId, MerchantDate, MerchantSwVersion, Note, PayloadNote,
TypePR1, UrlCancel, UrlFail, UrlPayTo, UrlSuccess,
PayloadHash_ = MD5(Payload),
{Payload}Des(PayloadKey);
2. Wallet -> CashRegister: /* CA1 */
NoteHash_ = MD5(Note),
OrderIdOptional,
PayeeCurrency_ = ExtractCurrency(MerchantAmount),
PayeeId_ = MerchantCcId,
PayerIndex, PayerSessionId,
PayloadHashOptional_ = PayloadHash_,
ServiceCategory, TypeCA1, VersionCA1,
OpaqueCA1_ =
{Amount_ = MerchantAmount,
SignatureCA1_ =
MD5(Amount_, NoteHash_, OrderIdOptional, PayeeCurrency_, PayeeId_,
PayerSessionSalt, PayloadHashOptional_, TypeCA1, VersionCA1,
PayerSessionId, /* See Section 3.4. */
PayerIndex)
}Des(PayerTransactionKey_);
3. CashRegister -> Gateway: /* CA2 */
PayeeIndex, ServiceCategory, PayeeSessionId, TypeCA2, VersionCA2,
OpaqueCA2_ =
{SubType, SubVersion, /* Non-lists */
MerchantAmountList_ = MerchantAmount, /* Lists */
NoteHashList_ = NoteHash_,
OrderIdOptionalList_ = OrderIdOptional,
PayerIndexList_ = PayerIndex,
PayerSessionIdList_ = PayerSessionId,
PayloadHashOptionalList_ = PayloadHashOptional_,
PayloadKeyOptionalList_ = PayloadKey,
SubTypeList_ = SubType,
SubVersionList_ = SubVersion,
SignatureCA2_ =
MD5(PayeeSessionSalt, ServiceCategory, /* Non-lists */
SubType, SubVersion, TypeCA2,VersionCA2,
MerchantAmountList_, NoteHashList_, /* Lists */
OrderIdOptionalList_, PayerIndexList_, PayerSessionIdList_,
PayloadHashOptionalList_, SubTypeList_, SubVersionList_,
PayeeSessionId, /* See Section 3.4. */
PayeeIndex)
}Des(PayeeTransactionKey_),
OpaqueListCA2_ = OpaqueCA1_;
4. Gateway -> CashRegister: /* CA3 */
PayeeIndex, ServiceCategory, PayeeSessionId, TypeCA3, VersionCA3,
OpaqueCA3_ =
{Fee, MessageOptional, ProblemOptional, /* Non-lists */
RequestVersion, ResponseCode, SubType, SubVersion,
CollectedAmountList_ = CollectedAmount, /* Lists */
OrderIdOptionalList_,
IndexList_ = PayeeIndex,
MessageOptionalList_ = MessageOptional,
ResponseCodeList_ = ResponseCode,
SessionIdList_= PayeeSessionId,
SubTypeList_, SubVersionList_,
ServerSignatureCA3_ =
MD5(Fee, MessageOptional, PayeeSessionSalt, /* Non-lists */
ProblemOptional, RequestVersion, ResponseCode,
ServiceCategory, SubType, SubVersion, TypeCA3, VersionCA3,
CollectedAmountList_, IndexList_, /* Lists */
MessageOptionalList_, OrderIdOptionalList_, ResponseCodeList_,
SessionIdList_, SubTypeList_, SubVersionList_,
PayeeSessionId, /* See Section 3.4. */
PayeeIndex)
}Des(PayeeTransactionKey_)
||(Wallet Conveyed SignatureCA1_),
OpaqueListCA3_ =
{Amount_, ForeignExchangeOptional, MessageOptional, OrderIdOptional,
PayloadHashOptional_,
PayloadKeyOptional_ = PayloadKey,
RequestVersion, ResponseCode,
ServerSignatureCA4_ =
MD5(Amount_, ForeignExchangeOptional, MessageOptional,
OrderIdOptional, PayloadHashOptional_, PayloadKeyOptional_,
PayerSessionSalt, RequestVersion, ResponseCode, TypeCA3,
VersionCA3,
PayerSessionId, /* See Section 3.4. */
PayerIndex)
}Des(PayerTransactionKey_)
||(CashRegister Conveyed SignatureCA2_);
5. CashRegister -> Wallet: /* CA4 */
MerchantMessageOptional, MerchantResponseCodeOptional,
OrderIdOptional, PayerIndex,
ServiceCategoryOptional_ = ServiceCategory,
PayerSessionId, TypeCA4, VersionCA4,
OpaqueCA4_ = OpaqueListCA3_;
/* Define the conditions the protocol steps are expected to produce */
GOALS:
3. Gateway Believes CashRegister Conveyed OpaqueCA2_;
Gateway Believes CashRegister Conveyed SignatureCA2_;
Gateway Believes Wallet Conveyed OpaqueCA1_;
Gateway Believes Wallet Conveyed SignatureCA1_;
4. CashRegister Believes Gateway Conveyed OpaqueCA3_;
CashRegister Believes Gateway Conveyed ServerSignatureCA3_;
CashRegister Believes Wallet Conveyed SignatureCA1_;
5. Wallet Believes Gateway Conveyed OpaqueListCA3_;
Wallet Believes Gateway Conveyed ServerSignatureCA4_;
Wallet Believes CashRegister Conveyed SignatureCA2_;
Wallet Possesses PayloadKey;
As before, the AAPA analysis confirms that the protocol meets its specified authentication goals.