Verification of Battleship681 Protocol

Charles Smutz

12/4/2007

Abstract: 3

Background: 3

Protocol Requirements: 3

Protocol Design: 4

Protocol Specification: 4

Protocol Verification 5

Security Property 1 6

Security Property 2 6

Security Property 3 6

Security Property 4 6

Security Property 5 7

Security Property 6 7

Appendix 1: Battleship Program Flow 9

Appendix 2: Verification of TLS using AVISPA 11

Specification 11

Visualization: 14

Test Parameters: 16

Results 16

OFMC 16

ATSE 16

SATC 17

TA4SP 17

Summary 18

Appendix 3: Verification of Battleship681 using AVISPA 19

Specification 19

Visualization: 20

Test Parameters: 22

Results 22

OFMC 22

ATSE 22

SATC 23

TA4SP 23

Summary 24

Abstract:

This Battleship681 as defined herein is shown to satisify the requirements of strong mutual authentication of both players, secrecy and integrity of messages sent between players, secrecy of ship layout until discovered through gameplay or revealed at the end of a round, and non-repudiation of gameplay. These properties are verified using the AVISPA[1] tool.

Background:

The Battleship681 protocol was devised specifically to as a protocol over which to conduct online versions of the popular game Battleship[2]. Battleship is a strategy game based on a naval warfare theme. Battleship is played by two players at one time. Each player places their ships on a grid. Each ship usually occupies a few (2-5) grid points. The arrangement of each player’s ships is kept secret from their opponent. Alternating turns, each player guesses at or fires on a grid point. If a ship covering that grid point, the opponent declares a “hit”. Otherwise, the opponent declares a “miss”. When all grid points that are covered by a ship have been guessed, or in other words, when all compartments on a ship are hit, the ship is declared “sunk” by the opponent. Appendix 1 provides the program flow for a reference implementation of a battleship game using the Battleship681 protocol. The requirements and name of the Battleship681 protocol are derived from the requirements of the “Major Project” for the ISA681 course at GMU[3] and generally accepted rules for the Battleship game.

Protocol Requirements:

The high-level security requirements for the Battleship681 protocol are as follows:

Given the following environment:

□  Game players do not trust each other (they may try to cheat)

□  Attackers may try to monitor and/or tamper with the game and its results

And the requirements imposed by the game:

□  Each player’s ship layout, which is chosen at the start of a round, should be kept secret from the opponent until it is revealed at the end of the game or revealed incrementally through guesses

□  Players should not move their ships one the game begins.

The protocol should provide the following security properties:

1.  Mutual Authentication of Players

2.  Confidentiality (from attackers) of game play (Guesses and answers are not known to anyone but players.)

3.  Integrity (from attackers) of game player (Guesses and answers are only made by players and can not be modified or spoofed by attackers.)

4.  Confidentiality of ship layout (from opponent) during game play (Ship layout should not be revealed except through guesses and answers.)

5.  Non-repudiation of ship layout (Player should be able to verify that ship layout created by opponent before game play is the same as that claimed at end of game play.)

6.  Non-repudiation of game play (messages and message acknowledgments), including each move (Player should be able to prove the outcome of game to a third party. Opponent should not be able to deny game play.)

Protocol Design:

The Battleship681 protocol leverages other protocols such as SSL to provide a secure channel for communication. Therefore, security properties 1, 2, and 3 are met through the use of an external protocol. Battleship681 does requirement for the use of a specific protocol. Furthermore, Battleship681 does not provide any means of specifying the protocol to be used either before secure channel establishment or verification that the established channel is indeed secure. For example, on a trusted platform, the channel may well be a local IPC mechanism such as a UNIX socket. It is expected that most implementations of the protocol will be used on TCP/IP networks and will leverage SSL/TLS, SSH, IPSEC, or some other protocol that satisfies security properties 1, 2, and 3. For completeness’s sake and for demonstrative purposes, a formal verification of TLS is given in Appendix 2.

The remaining 3 security properties are addressed in the protocol natively. The Battleship681 protocol provides for security property 4 by encrypting a player’s ship layout with a randomly selected board encryption key and transmitting the encrypted ship layout to the opponent. Security property 5 is achieved by sending the signature of the board encryption key to the opponent before the round is started and sending the plaintext board encryption key at the end of the round. Property 6 is achieved by sending a signature of each message between the players (which are synchronous). Each message includes the signature of the previous message which creates a running signature providing for non-repudiation of not only each message, chains previous messages back to the encrypted ship layout and board key signature messages at the start of a round.

Protocol Specification:

The Battleship681 protocol is specified from one of the two participants’ view as follows (the other side is symmetric):

1.  Establish secure channel (TLS, SSH, etc)

2.  Send Intialization Message

3.  Receive Intialization Message from opponent

4.  Loop until Termination Message received
{
Send Message || Receive Message
}

5.  Optionally, Send Verifcation Message

6.  Optionally, Receive Verification Message

Each Message consists of 3 parts: the payload, the conversation signature, and the message signature. The payload is the data to be communicated. The conversation signature is the digital signature of from the previous message in the conversation. The message signature is a digital signature over other 2 parts of the message (payload and conversation signature).

The Intialization Message payload is an encrypted data item to kept secret during the length of the game. It is intended that this secret be the ship layout, but this is not enforced by the protocol. The Initialization Message conversation message contains the digital signature of the key used for the message payload encryption. This key is hereafter known as the game board key. The conversation signature of the first Message after the exchange of Initialization Messages must contain the concatenation of both the message signatures of the two Initialization Messages. Other message types include: Guess Message, Answer Message, and Game Abort Message. These other messages must not reveal anything about the game board key.

It should be noted that this specification leaves many details unspecified. The protocol provides no method for agreement of crucial details such as details of secure channel establishment; exchange and verification of public keys used for signatures; negotiation of cryptographic algorithms, encoding methods, or data representation; determination of party to send the first message following exchange of the Initialization Messages; rules for sending the optional messages; etc.

Protocol Verification

Security Properties 1, 2, and 3 are provided through the use of another protocol. In this verification, TLS is used as a representative protocol to verify completeness of the Battleship681 protocol using another protocol. In other words, the verification of security properties 1, 2, and 3 will be exactly the same as those for TLS and should be considered representative of the set of all external protocols that could ensure properties 1, 2, and 3. Security Properties 4, 5, and 6 are met internally to the protocol.

Security Property 1

Mutual Authentication of Players

Security Property 1 is met through mutual authentication in establishing the secure channel (client certificate authentication in TLS). Both parties present certificates signed by a trusted third party and perform signatures on session-specific data. A verification of TLS using AVISPA, including strong authentication of both parties, is provided in Appendix 2.

Security Property 2

Confidentiality (from attackers) of game play (Guesses and answers are not known to anyone but players.)

Security Property 2 is met by encryption of data through the secure channel (TLS). The TLS protocol[4] specifies that application data be encrypted. The verification of TLS in Appendix 2 proves the secrecy of session keys negotiated between the two players.

Security Property 3

Integrity (from attackers) of game player (Guesses and answers are only made by players and can not be modified or spoofed by attackers.)

Security Property is met by authentication of data through the secure channel (TLS). The TLS protocol specifies that application data be authenticated using Message Authentication Codes (MAC). The verification of TLS in Appendix 2 proves the secrecy of session keys negotiated between the two players.

Security Property 4

Confidentiality of ship layout (from opponent) during game play (Ship layout should not be revealed except through guesses and answers.)

Security Property 4 is achieved by encrypting the secret (ship layout) with a unique key per game (presumably randomly generated) and not revealing the key until the game is terminated.

It is recognized that the ship layout will be progressively revealed through game play. Since the game board is of a well known format, the confidentiality of the ship layout is susceptible to a known-plaintext attack regardless. The secrecy of the ship layout rests on the secrecy (randomness) of the game board key. No messages reveal or otherwise weaken this key, including the signature of this key which is included in the Initialization message.

Secrecy in AVISPA is forward secrecy, or secrecy through the end of the protocol. Since AVISPA does not provide adequate mechanisms for modeling the secrecy of data up until a certain point in the protocol, only the Initialization Message of the protocol is modeled in the verification of the Battleship681 protocol. The ship layout is not revealed except through game play after the Initialization Message exchange until game termination. This claim and simplification of the protocol specification rests on the intuitive argument that the game board key is not included in any form or derivative in any messages after the initialization phase until termination and that any revelations concerning the ship layout are made through game play.

The secrecy of the ship layout at the end of the Battleship681 initialization phase is given in Appendix 3. Portions of the ship layout are revealed until game termination through game play (Guess Messages and Answer Messages) but not through any other means.

Security Property 5

Non-repudiation of ship layout (Player should be able to verify that ship layout created by opponent before game play is the same as that claimed at end of game play.)

Security Property 5 is achieved by providing the opponent with the encrypted ship layout and the signature of the board encryption key during the initialization phase. The Initialization Messages are signed also. The game board key is revealed at the end of the game (also signed). If the opponent cheats, the player can prove the inconsistency through the aforementioned signatures.

AVISPA provides no reasonable mechanisms for verifying the claims of non-repudiation in this protocol. The argument for the association of the signatures at the start of the game and the end of the game is made by security property 6. The authentication of the public keys used for signatures is performed by the secure channel (see security property 1 and verification in Appendix 2).

Security Property 6

Non-repudiation of game play (messages and message acknowledgments), including each move (Player should be able to prove the outcome of game to a third party. Opponent should not be able to deny game play.)

Security Property 6 is achieved by chaining signatures: the signature of the previous message is included in the message and therefore covered in the signature of the current message. The inclusion of the previous signature in the current message signature serves as an acknowledgement of the previous message, and through induction, all message back to the first message in the chain. The first message after the Intialization Messages includes the concatenation of the signatures of both Intialization Messages. The protocol is not purely synchronous (a player can send more than one message before it is acknowledged by the opponent) so game play can only be proven back to the last message sent by the opponent which is adequate for this protocol.

AVISPA provides no reasonable mechanisms for verifying the claims of non-repudiation in this protocol. The authentication of the public keys used for signatures is performed by the secure channel (see security property 1 and verification in Appendix 2).

Conclusion

The AVISPA tool was used to aid in the verification of the security properties of the Battleship681 protocol. The Battleship681 protocol is shown to meet the security requirements of strong mutual authentication of players, confidentiality and integrity of game play (vice non-players), secrecy of the ship layout until revealed through game play, and non-repudiation of the ship layout and game play.

Appendix 1: Battleship Program Flow

The following describes the program flow for the reference implementation of a networked battleship game based on Battleship681 protocol.

  1. Before start-up:
  2. User obtains certificate from Battleship CA
  3. certificate is encrypted with password/phrase selected by user
  4. Program Statup-Up Phase:
  5. User presented with connection screen
  6. User chooses either server or client
  7. User sets connection settings
  8. IP
  9. If server, IP is displayed.
  10. If client, IP of server must be entered.
  11. Port
  12. Default: 6464
  13. Key Pair
  14. User specifies location of PKCS encode keypair
  15. User enters password to unlock private key
  16. User clicks connect (or cancel)
  17. SSL connection between client and server established
  18. server and client certs verified against hardcoded CA public key
  19. If errors occurs, display error to user
  20. Errors:
  21. Connection Timeout
  22. Certificate Verification Error
  23. Client and Server are notified of identity of other party
  24. Game Layout Phase:
  25. Each player places his ships using GUI
  26. Each player sends layout of board encrypted with randomly generated key and signature of the randomly generated key.
  27. Each player stores opponent’s encrypted board layout and signature of encryption key.
  28. Game Play Phase:
  29. Client and Server take turns going first
  30. Player sends signed guess to opponent
  31. Guess object grid positions
  32. Signature is over toString() of Guess object concatenated with the signature of the previous message
  33. This creates running signature for whole game. Creates long chain of non-repudiation.
  34. Opponent sends Answer signed answer object
  35. Answer object contains grid positions, impact (hit, sinking of ship (including which ship), or miss), and running signature.
  36. Players alternate until all of one player’s ships are sunk or a player quits
  37. Game Verification Phase:
  38. Both players send key to decrypt each other’s ship placement
  39. Both players verify that ships did not “move” throughout the game and that answers.
  40. Program notifies players of win/loss and asks them if they want to see verification details
  41. Verification details include:
  42. Player Identities (certificate)
  43. Players’ encrypted board layouts
  44. Signatures of keys used to encrypt ship layouts
  45. Guesses (including signatures)
  46. Answers (including signatures)
  47. Players’ board layout encryption keys
  48. Verification is always available on program exit even if connection to opponent times out (opponent flees) except that board layout will not be verified (layout encryption keys not available).
  49. Game End Phase:
  50. If Game finished normally, player can choose 3 options:
  51. Play another round with current opponent
  52. returns to Game Layout Phase
  53. Play round with a new opponent
  54. returns to Program Start-Up Phase
  55. Exit
  56. program exits

Appendix 2: Verification of TLS using AVISPA