- Protocol Verification - Light Scheme

Multi-party Coin Toss

We implement a protocol where N + 2 parties labeled 0, ..., N + 1 reach a Boolean consensus. We prove the protocol secure against a malicious attacker in the case when party N is corrupt, party N + 1 is honest, and any other party is arbitrarily honest or corrupt.

Protocol Real
newfamily Commit[i < N + 2] : bool in
newfamily Committed[i < N + 2] : unit in
newfamily Open[i < N + 2] : unit in
newfamily Opened[i < N + 2] : bool in
(
(family Committed[i < N + 2] ::= 
  x : bool <- read Commit[i] ; 
  return () )
||
(family Opened[i < N + 2] ::=  
  commit : bool <- read Commit[i] ; 
  x : unit <- read Open[i] ; 
  return commit )
||
(family LeakCommittedCommAdv[i < N + 2] ::= 
  committed : unit <- read Committed[i] ; 
  return committed )
|| 
(family LeakOpenedCommAdv[i < N + 2] ::= 
  opened : bool <- read Opened[i] ; 
  return opened )
||
(family Party[i < N + 2] ::= 
  (when (honest(i)) --> (
    newfamily AllCommitted[i < N + 2, j < N + 3] : unit in
    newfamily SumOpened[i < N + 2, j < N + 3] : bool in
    (
      (family SumOpened[i < N + 2, j < N + 3] ::= 
        ( (when (0 = j) --> return False ) ;;
          (when (not (0 = j)) --> 
            x : bool <- read SumOpened[i, j - 1] ; 
            y : bool <- read Opened[j - 1] ; 
            return xor((x, y)) ) ) )
      ||
      (family AllCommitted[i < N + 2, j < N + 3] ::= 
        ( (when (0 = j) --> return () ) ;;
          (when (not (0 = j)) --> 
            x : unit <- read AllCommitted[i, j - 1] ; 
            y : unit <- read Committed[j - 1] ; 
            return () ) ) )
      ||
      (family Open[i < N + 2] ::= 
         x : unit <- read AllCommitted[i, N + 2] ; 
         return () )
      ||
      (family Commit[i < N + 2] ::= 
         samp flip (()) )
      ||
      (family Out[i < N + 2] ::= 
         sumOpened : bool <- read SumOpened[i, N + 2] ;
         return sumOpened )
    )
  ))
  ;;
  (when (corrupt(i)) --> (
    (family Commit[i < N + 2] ::= 
       advCommit : bool <- read AdvCommitAdvParty[i] ;
       return advCommit )
    ||
    (family Open[i < N + 2] ::= 
       advOpen : unit <- read AdvOpenAdvParty[i] ; 
       return advOpen )
    ||
    (family Out[i < N + 2] ::= 
       out : bool <- read Out[i] ; 
       return out )
  ))
)
)
Protocol ideal + sim
new OkAdvId : unit in
newfamily LeakFlipIdAdv[i < N + 2] : bool in
IDEAL
new Flip : bool in
( (Flip ::= samp flip (()) )
 || 
(family Out[i < N + 2] ::=
 (when honest(i) --> 
   ok : unit <- read OkAdvId ;
   f : bool <- read Flip ;
   return f )
 ;; 
(when corrupt(i) --> 
  out : bool <- read (Out [i]) ;
  return out ) 
)
 || 
(family LeakFlipIdAdv[i < N + 2] ::= 
 ( (when honest(i) --> 
     l : bool <- read (LeakFlipIdAdv[i]) ;
     return l)
   ;; 
   (when corrupt(i) --> 
     f : bool <- read Flip ;
     return f) 
 ) 
) 
)
SIM
newfamily AllOpen[j < N + 3] : unit in
newfamily Commit[i < N + 1] : bool in
new LastCommit : bool in

( ( family AllOpen[j < N + 3] ::=
    (when (j = 0) --> return ()) ;;
    (when (not (j = 0)) --> 
       x : unit <- read (AllOpen[j - 1]) ;
       y : unit <- read (Open[j - 1]) ;
       return () ) )
  ||
  ( family Commit[i < N + 1] ::= 
      samp flip (()) )
  ||
  ( LastCommit ::= 
    x : bool <- read (SumCommit [ N + 1 ]) ; 
    f : bool <- read (LeakFlipIdAdv [ N ]) ; 
    return xor( (x, f) ) )
  ||
  ( family SumCommit[j < N + 3] ::=
    (when (j = 0) --> return False) ;; 
    (when (j = N + 2) --> 
       x : bool <- read (SumCommit [ N + 1 ]) ; 
       f : bool <- read LastCommit ; 
       return xor( (x, f) ) ) ;; 
    (otherwise --> 
       x : bool <- read (SumCommit [j - 1]) ; 
       c : bool <- read (Commit [j - 1]) ; 
       return xor( (x, c) ) ) )
  ||
  ( OkAdvId ::= 
    ao : unit <- read (AllOpen[N + 2]) ; 
    sc : bool <- read (SumCommit[N + 1]) ; 
    return () )
)

begin strict proof

1
start with real over delta
2
add internal family AllCommitted1 indices: i bounds: bound N + 3 typed: unit assigned: (when (i = 0) --> return ()) ;; (when (not (i = 0)) --> x : unit <- read (AllCommitted1[i - 1]) ; y : unit <- read (Committed[i - 1]) ; return () )
3
add internal family SumOpened1 indices: j bounds: bound N + 3 typed: bool assigned: (when (j = 0) --> return False ) ;; (when (not (j = 0)) --> x : bool <- read SumOpened1[j - 1] ; y : bool <- read Opened[j - 1] ; return xor( (x, y) ) )
4
case distinction on group Party[bound N + 2] ( case: ( in the presence of fam AllCommitted1[bound (N + 3)] , fam Committed[bound (N + 2)] rewrite family AllCommitted[bound (N + 2) bound (N + 3)] to x : unit <- read AllCommitted1[j] ; return x by induction on j bound B ( case distinction on family AllCommitted[bound (N + 2) fixedBound B] ( case: ( sym from change fam AllCommitted[bound (N + 2) fixedBound B] with x : unit <- read AllCommitted1[B] ; return x in currentProtocol ( subst fam AllCommitted1[bound (N + 3)] into fam AllCommitted[bound (N + 2) fixedBound B] ) ) case: ( subst fam AllCommitted[bound (N + 2) bound B] into fam AllCommitted[bound (N + 2) fixedBound B] then sym from change fam AllCommitted[bound (N + 2) fixedBound B] with x : unit <- read AllCommitted1[B] ; return x in currentProtocol ( subst fam AllCommitted1[bound (N + 3)] into fam AllCommitted[bound (N + 2) fixedBound B] ) ) ) then merge cases for fam AllCommitted[bound (N + 2) fixedBound B] ) then subst fam AllCommitted[bound (N + 2) bound (N + 3)] into fam Open[bound (N + 2)] then absorb fam AllCommitted[bound (N + 2) bound (N + 3)] then in the presence of fam SumOpened1[bound (N + 3)] rewrite family SumOpened[bound (N + 2) bound (N + 3)] to x : bool <- read SumOpened1[j] ; return x by induction on j bound B ( case distinction on family SumOpened[bound (N + 2) fixedBound B] ( case: ( sym from change fam SumOpened[bound (N + 2) fixedBound B] with x : bool <- read SumOpened1[B] ; return x in currentProtocol ( subst fam SumOpened1[bound (N + 3)] into fam SumOpened[bound (N + 2) fixedBound B] ) ) case: ( subst fam SumOpened[bound (N + 2) bound B] into fam SumOpened[bound (N + 2) fixedBound B] then sym from change fam SumOpened[bound (N + 2) fixedBound B] with x : bool <- read SumOpened1[B] ; return x in currentProtocol ( subst fam SumOpened1[bound (N + 3)] into fam SumOpened[bound (N + 2) fixedBound B] ) ) ) then merge cases for fam SumOpened[bound (N + 2) fixedBound B] ) then subst fam SumOpened[bound (N + 2) bound (N + 3)] into fam Out[bound (N + 2)] then absorb fam SumOpened[bound (N + 2) bound (N + 3)] ) case: (idle) )
5
combine fam Party[bound N + 2]
6
add internal family SumCommit indices: j bounds: bound N + 3 typed: bool assigned: (when (j = 0) --> return False) ;; ( when (not (j = 0)) --> xj : bool <- read SumCommit[j - 1] ; cj : bool <- read Commit[j - 1] ; return xor( (xj, cj) ) )
7
add internal family AllOpen indices: j bounds: bound N + 3 typed: unit assigned: ( when (j = 0) --> return () ) ;; ( when (not (j = 0)) --> x : unit <- read AllOpen[j - 1] ; y : unit <- read Open[j - 1] ; return () )
8
in the presence of fam AllOpen[bound (N + 3)], fam SumCommit[bound (N + 3)], fam Opened[bound (N + 2)] rewrite family SumOpened1[bound (N + 3)] to ao : unit <- read AllOpen[j] ; sc : bool <- read SumCommit[j] ; return sc by induction on j bound B ( case distinction on channel SumOpened1[B] ( case: ( sym from change chn SumOpened1[B] with ao : unit <- read AllOpen[B] ; sc : bool <- read SumCommit[B] ; return sc in currentProtocol ( subst fam AllOpen[bound (N + 3)] into chn SumOpened1[B] then subst fam SumCommit[bound (N + 3)] into chn SumOpened1[B] ) ) case: ( subst fam SumOpened1[bound B] into chn SumOpened1[B] then subst fam Opened[bound (N + 2)] into chn SumOpened1[B] then rename x to y, commit to cj, sc to xj, ao to x in chn SumOpened1[B] then sym from change chn SumOpened1[B] with ao : unit <- read AllOpen[B] ; sc : bool <- read SumCommit[B] ; return sc in currentProtocol ( subst fam AllOpen[bound (N + 3)] into chn SumOpened1[B] then subst fam SumCommit[bound (N + 3)] into chn SumOpened1[B] ) ) ) then merge cases for chn SumOpened1[B] )
9
on branch honest(i) of family Out[bound N + 2] ( subst fam SumOpened1[bound (N + 3)] into fam Out[bound (N + 2)] )
10
absorb fam SumOpened1[bound (N + 3)]
11
split fam Committed[bound N + 2] on first index
12
split fam Commit[bound N + 2] on first index
13
drop read chn Commit[N + 1] from chn Committed[N + 1]
14
split fam AllCommitted1[bound N + 3] on first index
15
subst chn Committed[N + 1] into chn AllCommitted1[N + 2]
16
on branch honest(i) of family Open[bound N + 2] ( subst chn AllCommitted1[N + 2] into fam Open[bound (N + 2)] )
17
absorb chn AllCommitted1[N + 2]
18
in the presence of fam Committed[bound (N + 1)], fam SumCommit[bound (N + 3)] rewrite family AllCommitted1[bound (N + 2)] to sc : bool <- read SumCommit[i] ; return () by induction on i bound B ( case distinction on channel AllCommitted1[B] ( case: ( sym from change chn AllCommitted1[B] with sc : bool <- read SumCommit[B] ; return () in currentProtocol ( subst fam SumCommit[bound (N + 3)] into chn AllCommitted1[B] ) ) case: ( subst fam AllCommitted1[bound B] into chn AllCommitted1[B] then subst fam Committed[bound (N + 1)] into chn AllCommitted1[B] then rename sc to xj, x to cj in chn AllCommitted1[B] then sym from change chn AllCommitted1[B] with sc : bool <- read SumCommit[B] ; return () in currentProtocol ( subst fam SumCommit[bound (N + 3)] into chn AllCommitted1[B] ) ) ) then merge cases for chn AllCommitted1[B] )
19
on branch honest(i) of family Open[bound N + 2]( subst fam AllCommitted1[bound (N + 2)] into fam Open[bound (N + 2)] )
20
absorb fam AllCommitted1[bound (N + 2)]
21
turn neg into otherwise for fam SumCommit[bound(N + 3)]
22
unsplit Committed
23
turn neg into otherwise for fam Committed[bound N + 2]
24
sym from idealPlusSim ( on branch honest(i) of family Out[bound N + 2]( subst chn OkAdvId into fam Out[bound (N + 2)] ) then absorb chn OkAdvId then subst fam LeakFlipIdAdv[bound N + 2] into chn LastCommit then absorb fam LeakFlipIdAdv[bound N + 2] then on branch honest(i) of family Out[bound N + 2] ( sym from change fam Out[bound (N + 2)] with ao : unit <- read AllOpen[N + 2] ; sc : bool <- read SumCommit[N + 2] ; return sc in currentProtocol ( subst fam SumCommit[bound (N + 3)] into fam Out[bound (N + 2)] then subst chn LastCommit into fam Out[bound (N + 2)] then rename x to sc in fam Out[bound (N + 2)] ) ) then fold chn Flip into chn LastCommit then use assumption flipInvariantXorFixed on chn LastCommit then sym from extend (change chn LastCommit with x : bool <- read SumCommit[N + 1] ; commit : bool <- read Commit[N + 1] ; return commit in currentProtocol) with internal channel Commit[N + 1] typed: bool assigned: samp flip (()) ( fold chn Commit[N + 1] into chn LastCommit ) then on branch i = N + 1 of family Opened[bound N + 2] ( rename x to o in fam Opened[bound N + 2] then subst chn LastCommit into fam Opened[bound N + 2] ) then on branch j = N + 2 of family SumCommit[bound N + 3]( subst chn LastCommit into fam SumCommit[bound N + 3] then rename commit to c in fam SumCommit[bound N + 3] ) then absorb chn LastCommit then merge case j = N + 2 with otherwise for fam SumCommit[bound N + 3] then case distinction on family SumCommit[bound N + 3] ( case: ( idle ) case: ( rename c to cj, x to xj in fam SumCommit[bound N + 3] ) ) then on branch i = N + 1 of family Opened[bound N + 2] ( subst fam Open[bound N + 2] into fam Opened[bound N + 2] then sym from change fam Opened[bound (N + 2)] with commit : bool <- read Commit[N + 1] ; o : unit <- read Open[N + 1] ; return commit in currentProtocol ( subst fam Open[bound N + 2] into fam Opened[bound N + 2] ) then rename o to x in fam Opened[bound N + 2] ) then merge cases for fam Opened[bound N + 2] )
25
restructure idealPlusSim
26
check-proof idealPlusSim