module SMCDEL.Examples.DiningCrypto where

import Data.List (delete)
import Data.Maybe (fromJust)

import SMCDEL.Language
import SMCDEL.Symbolic.S5

dcScnInit :: Int -> (Bool,Bool,Bool) -> KnowScene
dcScnInit :: Int -> (Bool, Bool, Bool) -> KnowScene
dcScnInit Int
payer (Bool
b1,Bool
b2,Bool
b3) = ( [Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS [Prp]
props Bdd
law [(Agent, [Prp])]
obs , [Prp]
truths ) where
  props :: [Prp]
props = [ Int -> Prp
P Int
0   -- The NSA paid
          , Int -> Prp
P Int
1   -- Alice paid
          , Int -> Prp
P Int
2   -- Bob paid
          , Int -> Prp
P Int
3   -- Charlie paid
          , Int -> Prp
P Int
4   -- shared bit of Alice and Bob
          , Int -> Prp
P Int
5   -- shared bit of Alice and Charlie
          , Int -> Prp
P Int
6 ] -- shared bit of Bob and Charlie
  law :: Bdd
law   = Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj [ Form
someonepaid, Form
notwopaid ]
  obs :: [(Agent, [Prp])]
obs   = [ (Int -> Agent
forall a. Show a => a -> Agent
show (Int
1::Int),[Int -> Prp
P Int
1, Int -> Prp
P Int
4, Int -> Prp
P Int
5])
          , (Int -> Agent
forall a. Show a => a -> Agent
show (Int
2::Int),[Int -> Prp
P Int
2, Int -> Prp
P Int
4, Int -> Prp
P Int
6])
          , (Int -> Agent
forall a. Show a => a -> Agent
show (Int
3::Int),[Int -> Prp
P Int
3, Int -> Prp
P Int
5, Int -> Prp
P Int
6]) ]
  truths :: [Prp]
truths = [ Int -> Prp
P Int
payer ] [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [ Int -> Prp
P Int
4 | Bool
b1 ] [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [ Int -> Prp
P Int
5 | Bool
b2 ] [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [ Int -> Prp
P Int
6 | Bool
b3 ]

dcScn1 :: KnowScene
dcScn1 :: KnowScene
dcScn1 = Int -> (Bool, Bool, Bool) -> KnowScene
dcScnInit Int
1 (Bool
True,Bool
True,Bool
False)

someonepaid, notwopaid :: Form
someonepaid :: Form
someonepaid = [Form] -> Form
Disj ((Int -> Form) -> [Int] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Prp -> Form
PrpF (Prp -> Form) -> (Int -> Prp) -> Int -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Prp
P) [Int
0..Int
3])
notwopaid :: Form
notwopaid = [Form] -> Form
Conj [ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj [ Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Prp
P Int
x, Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Prp
P Int
y ] | Int
x<-[Int
0..Int
3], Int
y<-[(Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)..Int
3] ]

reveal :: Int -> Form
reveal :: Int -> Form
reveal Int
1 = [Form] -> Form
Xor ((Prp -> Form) -> [Prp] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Form
PrpF [Int -> Prp
P Int
1, Int -> Prp
P Int
4, Int -> Prp
P Int
5])
reveal Int
2 = [Form] -> Form
Xor ((Prp -> Form) -> [Prp] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Form
PrpF [Int -> Prp
P Int
2, Int -> Prp
P Int
4, Int -> Prp
P Int
6])
reveal Int
_ = [Form] -> Form
Xor ((Prp -> Form) -> [Prp] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Form
PrpF [Int -> Prp
P Int
3, Int -> Prp
P Int
5, Int -> Prp
P Int
6])

dcScn2 :: KnowScene
dcScn2 :: KnowScene
dcScn2 = KnowScene -> Form -> KnowScene
forall a b. Update a b => a -> b -> a
update KnowScene
dcScn1 ([Form] -> Form
Conj [Int -> Form
reveal Int
1, Int -> Form
reveal Int
2, Int -> Form
reveal Int
3])

everyoneKnowsWhetherNSApaid :: Form
everyoneKnowsWhetherNSApaid :: Form
everyoneKnowsWhetherNSApaid = [Form] -> Form
Conj [ Agent -> Form -> Form
Kw (Int -> Agent
forall a. Show a => a -> Agent
show Int
i) (Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Prp
P Int
0) | Int
i <- [Int
1..Int
3]::[Int] ]

nobodyknowsWhoPaid :: Form
nobodyknowsWhoPaid :: Form
nobodyknowsWhoPaid = [Form] -> Form
Conj
  [ Form -> Form -> Form
Impl (Prp -> Form
PrpF (Int -> Prp
P Int
1)) ([Form] -> Form
Conj [Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Agent -> Form -> Form
K Agent
"2" (Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Prp
P Int
1), Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Agent -> Form -> Form
K Agent
"3" (Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Prp
P Int
1) ])
  , Form -> Form -> Form
Impl (Prp -> Form
PrpF (Int -> Prp
P Int
2)) ([Form] -> Form
Conj [Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Agent -> Form -> Form
K Agent
"1" (Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Prp
P Int
2), Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Agent -> Form -> Form
K Agent
"3" (Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Prp
P Int
2) ])
  , Form -> Form -> Form
Impl (Prp -> Form
PrpF (Int -> Prp
P Int
3)) ([Form] -> Form
Conj [Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Agent -> Form -> Form
K Agent
"1" (Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Prp
P Int
3), Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Agent -> Form -> Form
K Agent
"2" (Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Prp
P Int
3) ]) ]

dcCheckForm :: Form
dcCheckForm :: Form
dcCheckForm = Form -> Form -> Form
PubAnnounceW (Int -> Form
reveal Int
1) (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Form -> Form -> Form
PubAnnounceW (Int -> Form
reveal Int
2) (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Form -> Form -> Form
PubAnnounceW (Int -> Form
reveal Int
3) (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$
    [Form] -> Form
Conj [ Form
everyoneKnowsWhetherNSApaid, Form
nobodyknowsWhoPaid ]

dcValid :: Bool
dcValid :: Bool
dcValid = KnowStruct -> Form -> Bool
validViaBdd KnowStruct
dcStruct Form
dcCheckForm where (KnowStruct
dcStruct,[Prp]
_) = KnowScene
dcScn1

genDcSomeonepaid :: Int -> Form
genDcSomeonepaid :: Int -> Form
genDcSomeonepaid Int
n = [Form] -> Form
Disj ((Int -> Form) -> [Int] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Prp -> Form
PrpF (Prp -> Form) -> (Int -> Prp) -> Int -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Prp
P) [Int
0..Int
n])

genDcNotwopaid :: Int -> Form
genDcNotwopaid :: Int -> Form
genDcNotwopaid Int
n = [Form] -> Form
Conj [ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj [ Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Prp
P Int
x, Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Prp
P Int
y ] | Int
x<-[Int
0..Int
n], Int
y<-[(Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)..Int
n] ]

-- | Initial structure for Dining Cryptographers (complete graph!)
genDcKnsInit :: Int -> KnowStruct
genDcKnsInit :: Int -> KnowStruct
genDcKnsInit Int
n = [Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS [Prp]
props Bdd
law [(Agent, [Prp])]
obs where
  props :: [Prp]
props = [ Int -> Prp
P Int
0 ] -- The NSA paid
    [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [ (Int -> Prp
P Int
1) .. (Int -> Prp
P Int
n) ] -- agent i paid
    [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [Prp]
sharedbits
  law :: Bdd
law = Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj [Int -> Form
genDcSomeonepaid Int
n, Int -> Form
genDcNotwopaid Int
n]
  obs :: [(Agent, [Prp])]
obs = [ (Int -> Agent
forall a. Show a => a -> Agent
show Int
i, Int -> [Prp]
obsfor Int
i) | Int
i<-[Int
1..Int
n] ]
  sharedbitLabels :: [[Int]]
sharedbitLabels = [ [Int
k,Int
l] | Int
k <- [Int
1..Int
n], Int
l <- [Int
1..Int
n], Int
kInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<Int
l ] -- n(n-1)/2 shared bits
  sharedbitRel :: [([Int], Prp)]
sharedbitRel = [[Int]] -> [Prp] -> [([Int], Prp)]
forall a b. [a] -> [b] -> [(a, b)]
zip [[Int]]
sharedbitLabels [ (Int -> Prp
P (Int -> Prp) -> Int -> Prp
forall a b. (a -> b) -> a -> b
$ Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) .. ]
  sharedbits :: [Prp]
sharedbits =  (([Int], Prp) -> Prp) -> [([Int], Prp)] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map ([Int], Prp) -> Prp
forall a b. (a, b) -> b
snd [([Int], Prp)]
sharedbitRel
  obsfor :: Int -> [Prp]
obsfor Int
i =  Int -> Prp
P Int
i Prp -> [Prp] -> [Prp]
forall a. a -> [a] -> [a]
: (([Int], Prp) -> Prp) -> [([Int], Prp)] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map ([Int], Prp) -> Prp
forall a b. (a, b) -> b
snd ((([Int], Prp) -> Bool) -> [([Int], Prp)] -> [([Int], Prp)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\([Int]
label,Prp
_) -> Int
i Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
label) [([Int], Prp)]
sharedbitRel)

genDcEveryoneKnowsWhetherNSApaid :: Int -> Form
genDcEveryoneKnowsWhetherNSApaid :: Int -> Form
genDcEveryoneKnowsWhetherNSApaid Int
n = [Form] -> Form
Conj [ Agent -> Form -> Form
Kw (Int -> Agent
forall a. Show a => a -> Agent
show Int
i) (Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Prp
P Int
0) | Int
i <- [Int
1..Int
n] ]

genDcReveal :: Int -> Int -> Form
genDcReveal :: Int -> Int -> Form
genDcReveal Int
n Int
i = [Form] -> Form
Xor ((Prp -> Form) -> [Prp] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Form
PrpF [Prp]
ps) where
  (KnS [Prp]
_ Bdd
_ [(Agent, [Prp])]
obs) = Int -> KnowStruct
genDcKnsInit Int
n
  ps :: [Prp]
ps            = Maybe [Prp] -> [Prp]
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe [Prp] -> [Prp]) -> Maybe [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ Agent -> [(Agent, [Prp])] -> Maybe [Prp]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Int -> Agent
forall a. Show a => a -> Agent
show Int
i) [(Agent, [Prp])]
obs

genDcNobodyknowsWhoPaid :: Int -> Form
genDcNobodyknowsWhoPaid :: Int -> Form
genDcNobodyknowsWhoPaid Int
n =
  [Form] -> Form
Conj [ Form -> Form -> Form
Impl (Prp -> Form
PrpF (Int -> Prp
P Int
i)) ([Form] -> Form
Conj [Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Agent -> Form -> Form
K (Int -> Agent
forall a. Show a => a -> Agent
show Int
k) (Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Prp
P Int
i) | Int
k <- Int -> [Int] -> [Int]
forall a. Eq a => a -> [a] -> [a]
delete Int
i [Int
1..Int
n] ]) | Int
i <- [Int
1..Int
n] ]

genDcCheckForm :: Int -> Form
genDcCheckForm :: Int -> Form
genDcCheckForm Int
n =
  [Form] -> Form -> Form
pubAnnounceWhetherStack [ Int -> Int -> Form
genDcReveal Int
n Int
i | Int
i<-[Int
1..Int
n] ] (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$
    [Form] -> Form
Conj [ Int -> Form
genDcEveryoneKnowsWhetherNSApaid Int
n, Int -> Form
genDcNobodyknowsWhoPaid Int
n ]

genDcValid :: Int -> Bool
genDcValid :: Int -> Bool
genDcValid Int
n = KnowStruct -> Form -> Bool
validViaBdd (Int -> KnowStruct
genDcKnsInit Int
n) (Int -> Form
genDcCheckForm Int
n)