Experiments for Protocols with Choice

Fan Yang¹, Santiago Escobar², Catherine Meadows³, José Meseguer¹, Sonia Santiago⁴

¹ University of Illinois at Urbana-Champaign, USA.
² VRAIN, Universitat Politècnica de València, Spain.
³ Naval Research Laboratory, Washington DC, USA.
⁴ ITI, Universitat Politècnica de València, Spain.

In this web page we present the experiments we have performed to validate our approach for specifying and analyzing protocols with choice, which is presented in our article "Strand Spaces with Choice via a Process Algebra Semantics". We provide here the source files of the protocol specifications and output of the analysis.

Choice of Encryption Mode

This protocol allows either public key encryption or shared key encryption to be used for Alice to communicate with Bob. Alice initiates the conversation by sending out a message containing the chosen encryption mode, then Bob replies by sending an encrypted message containing his session key. The encryption mode is chosen nondeterministically by Alice. In the case that a public key encryption (denoted by PubKey) is chosen, the protocol proceeds as follows:

1. A -> B: A ; B ; PubKey
2. B -> A: pk(A, B; SK)
3. A -> B: pk(B, A ; SK ; NA
4. B -> A: pk(A, B ; NA )

In the case that a shared key encryption (denoted by SharedKey) is chosen, the protocol proceeds as follows:

1. A -> B: A ; B ; SharedKey
2. B -> A: shk(key(A,B), B ; SK)
3. A -> B: shk(key(A,B), A ; SK ; NA)
4. B -> A: shk(key(A,B), B ; NA)

We checked that the intruder cannot learn the session key generated by Bob, when either the public key encryption or shared key encryption is chosen, assuming both Alice and Bob are honest principals. The protocol specification and the output of the analysis are listed below:

Rock Paper Scissors

This protocol simulates the famous Rock-paper-scissors game, in which Alice and Bob are the two players of the game. In one round of the game, Alice and Bob commit to each other their hand shapes, which are later on revealed to each other after both players committed their hand shapes. The result of the game is then agreed between the two players according to the rule: rock beats scissors, scissors beats paper and paper beats rock. The protocol proceeds as follows:

1. A -> B: pk(B, sign(A, commit(NA, XA) ) )
2. B -> A: pk(A, sign(B, commit(NB, XB ) ) )
3. A -> B: pk(B, sign(A, NA )
4. B -> A: pk(A, sign(B, NB)
5. if (XA beats XB) then R = Win
     else if (XB beats XA) then R = Lose
       else if (XB = XA) then R = Tie
6. A -> B : pk(B, sign(A, NA ; NB ; R ) )
7. if ( (R = Win & XA beats XB ) or (R = Lose & XB beats XA ) or (R = Tie & XA = XB) )
     then B -> A: pk(A, sign(B, NA ; NB ; finished )
     else B -> A: pk(A, sign(B, NA ; NB ; cheater )

We first tried to see whether the protocol can simulate the game successfully, so we asked for different scenarios in which the player Alice or Bob can win in a round of the game. Maude-NPA was able to generate the expected scenarios, and it did not generate any others. We then gave Maude-NPA a secrecy attack state, in which the intruder, playing the role of initiator against an honest responder, attempts to guess its nonce before the responder receives its commitment. Finally we specified an authentication attack state in which we asked if a responder could complete a session with an honest initiator with the conclusion that the initiator had carried out its rule faithfully, without that actually having happened. For both of these attack states Maude-NPA finished its search without finding any attacks. The protocol specification and the output of the analysis are listed below:

TLS Protocol

In our experiment, we used a simplified version of the handshake protocol in TLS 1.3, a proposed update to the TLS standard for client server authentication. We were able to execute the protocol and check the correctness of our specification by producing legal executions in Maude-NPA. The protocol specification and the output of the analysis are listed below:

We intentionally included a vulnerability in our version: unlike TLS 1.3, it is subject to a "downgrade attack" in which the attacker can trick the principals into using a weaker crypto system even when they are both capable of supporting stronger ones. We have not yet been able to produce the attack, because a very deep and wide analysis tree is produced because of the long messages and the different possible executions. The protocol specification and the output of the analysis are listed below: