Probabilistic Contract Signing Protocol with PAT and Prism

View previous topic View next topic Go down

Probabilistic Contract Signing Protocol with PAT and Prism

Post  truongkhanh on Wed Feb 24, 2010 4:23 pm

Contract signing is when 2 or more parties want to sign a contract. We will consider a Contract Signing Protocol specified in [EGL85]. According to [EGL85], 2 parties A and B will exchange 2*n random secret a[1], a[2],..., a[2n]. A is considered committed to contract c if B can present both secrets from any one of A's pairs, that is, if B knows both a[i] and a[n+i] for some i. B is considered committed if A can present b[j] and b[n+j] for some j.

The protocol uses a 1-out-of-2 oblivious transfer (OT) subprotocol which allows one party to transfer exactly one secret, out of two secrets to his counterpart. Therefore when B sends the secrets b[i] and b[n+i] to A via OT, A will receive b[i] with the probability 1/2 and b[n+i] with the probability 1/2.

[EGL85] protocol specification:
EGL (A,B,{ (ai,an+i) },{ (bi,bn+i) })

(step 1)
for i=1 to n
OT(A,B,a[i],a[n+i])
(A sends a[i] and a[n+i] to B via OT)
OT(B,A,b[i],b[n+i])
(B sends b[i] and b[n+i] to A via OT)
end

(step 2)
for i=1 to L
(L is the length of each of the secrets)
for j=1 to 2n
A transmits bit i of the secret j
end
for j=1 to 2n
B transmits bit i of the secret j
end
end


The specification of the protocol is be modeled in PAT as below.


// number of pairs of secrets
#define N 5;
// number of bits in each secret
#define L 3;

// b[i] the number of bits of B's ith secret A knows
var b[2 * N + 1] : {0..L};
// a[i] the number of bits of A's ith secret B knows
var a[2 * N + 1] : {0..L};


Step1_A_Send(i) = [i < N]A_sends_via_OT -> pcase {
[0.5] : {a[i] = L} -> Step1_B_Send(i)
[0.5] : {a[i + N] = L} -> Step1_B_Send(i)

}
[]
[i == N] Step2_A_Send(0, 0);

Step1_B_Send(i) = B_sends_via_OT -> pcase {
[0.5] : {b[i] = L} -> Step1_A_Send(i + 1)
[0.5] : {b[i + N] = L} -> Step1_A_Send(i + 1)

};

//A transmits bit i of the secret j
Step2_A_Send(i, j) = [i < L && j < 2 * N && a[j] < L]A_sends_bit_i{a[j] = i + 1;} -> Step2_A_Send(i, j + 1)
[]
[i < L && j < 2 * N && a[j] == L]A_sends_bit_i -> Step2_A_Send(i, j + 1)
[]
[i < L && j == 2 * N]Step2_B_Send(i, 0)
[]
[i == L]Stop;


//B transmits bit i of the secret j
Step2_B_Send(i, j) = [j < 2 * N && b[j] < L]B_sends_bit_i{b[j] = i + 1;} -> Step2_B_Send(i, j + 1)
[]
[j < 2 * N && b[j] == L]B_sends_bit_i -> Step2_B_Send(i, j + 1)
[]
[j == 2 * N]Step2_A_Send(i + 1, 0);

System = Step1_A_Send(0);

#define knowA ((b[0] == L && b[0 + N] == L) ||(b[1] == L && b[1 + N] == L) ||(b[2] == L && b[2 + N] == L) ||(b[3] == L && b[3 + N] == L) ||(b[4] == L && b[4 + N] == L));
#define knowB ((a[0] == L && a[0 + N] == L) ||(a[1] == L && a[1 + N] == L) ||(a[2] == L && a[2 + N] == L) ||(a[3] == L && a[3 + N] == L) ||(a[4] == L && a[4 + N] == L));


#define unfairForA (!knowA && knowB);

#assert System reaches unfairForA;
#assert System |= (<>unfairForA)with pmax;
#assert System |= (<>unfairForA)with pmin;

The specification of the protocol in Prism can be found at http://www.prismmodelchecker.org/casestudies/contract_egl.php.

Compare the modeling languages, CSP language in PAT and PRISM language share most basic features for probabilistic model. However, one noticeable of PAT is that it supports the definition of process with process parameter which allows user to change the value of model parameter, the number of pairs of secrete and number of bits of each secret in this case. Although PRISM has "module renaming" which allows duplication of modules, it is difficult to adapt the variables for each new module accordingly and needs a lot of time to paste and adapt when there are a lot of modules.

You can copy this specification and run in PAT tool. Please remember when you change the number of pairs of secret N, you must change the unfairForA accordingly. The number of bits in each secret L is free to change.

truongkhanh

Posts : 1
Join date : 2010-02-15

View user profile

Back to top Go down

View previous topic View next topic Back to top

- Similar topics

 
Permissions in this forum:
You cannot reply to topics in this forum