```module protocol

b : [1..L]; // counter for current bit to be send
n : [0..N-1]; // counter for which secret to send
phase : [1..4]; // phase of the protocol
// 1 - sending secrets using OT (step 1 of the protocol)
// 2 - send bits of the secrets 0,...,N-1 (step 2 of the protocol)
// 3 - send bits of the secrets N,...,2N-1 (step 2 of the protocol)
party : [1..2]; // which party sends next (1 - A and 2 - B)

// STEP 1
// A sends
[receiveB] phase=1 & party=1 -> (party'=2);
// B sends and we move onto the next secret
[receiveA] phase=1 & party=2 & n<N-1 -> (party'=1) & (n'=n+1);
// B sends and finished this step
[receiveA] phase=1 & party=2 & n=N-1 -> (party'=1) & (phase'=2) & (n'=0);
// STEP 2 (A sends)
// next secret
[receiveB] !kB & (phase=2 | phase=3) & party=1 & n<N-1-> (n'=n+1);
// move onto secrets N,...,2N-1
[receiveB] !kB & phase=2 & party=1 & n=N-1 -> (phase'=3) & (n'=0);
// move onto party B
[receiveB] !kB & phase=3 & party=1 & n=N-1 -> (phase'=2) & (party'=2) & (n'=0);
// STEP 2 (B sends)
// next secret
[receiveA] !kB & (phase=2 | phase=3) & party=2 & n<N-1 -> (n'=n+1);
// move onto secrets N,...,2N-1
[receiveA] !kB & phase=2 & party=2 & n=N-1 -> (phase'=3) & (n'=0);
// move onto next bit
[receiveA] !kB & phase=3 & party=2 & n=N-1 & b<L -> (phase'=2) & (party'=1) & (n'=0) & (b'=b+1);
// finished protocol
[receiveA] !kB & phase=3 & party=2 & n=N-1 & b=L -> (phase'=4);

// when B knows a pair we stop and compute the expected bits A requires
[finish] kB & phase<4 -> (phase'=4);
// FINISHED
[] phase=4 -> (phase'=4); // loop

endmodule

```