From ee82594803dba66e95a5f729e3d7f7c97d9f4a40 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 14 Oct 2007 14:32:17 +0000 Subject: [PATCH] Dining cryptographers example. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@446 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- .../dining_crypt/.anonymityN.pctl.pp | 5 ++ prism-examples/dining_crypt/.autopp | 11 +++ .../dining_crypt/.correctnessN.pctl.pp | 6 ++ .../dining_crypt/.dining_cryptN.nm.pp | 48 +++++++++++++ prism-examples/dining_crypt/README | 10 +++ prism-examples/dining_crypt/anonymity10.pctl | 4 ++ prism-examples/dining_crypt/anonymity15.pctl | 4 ++ prism-examples/dining_crypt/anonymity3.pctl | 4 ++ prism-examples/dining_crypt/anonymity4.pctl | 4 ++ prism-examples/dining_crypt/anonymity5.pctl | 4 ++ prism-examples/dining_crypt/anonymity6.pctl | 4 ++ prism-examples/dining_crypt/anonymity7.pctl | 4 ++ prism-examples/dining_crypt/anonymity8.pctl | 4 ++ prism-examples/dining_crypt/anonymity9.pctl | 4 ++ prism-examples/dining_crypt/auto | 21 ++++++ .../dining_crypt/correctness10.pctl | 5 ++ .../dining_crypt/correctness15.pctl | 5 ++ prism-examples/dining_crypt/correctness3.pctl | 5 ++ prism-examples/dining_crypt/correctness4.pctl | 5 ++ prism-examples/dining_crypt/correctness5.pctl | 5 ++ prism-examples/dining_crypt/correctness6.pctl | 5 ++ prism-examples/dining_crypt/correctness7.pctl | 5 ++ prism-examples/dining_crypt/correctness8.pctl | 5 ++ prism-examples/dining_crypt/correctness9.pctl | 5 ++ prism-examples/dining_crypt/dining_crypt10.nm | 60 ++++++++++++++++ prism-examples/dining_crypt/dining_crypt15.nm | 70 +++++++++++++++++++ prism-examples/dining_crypt/dining_crypt3.nm | 46 ++++++++++++ .../dining_crypt/dining_crypt3.pctl | 0 prism-examples/dining_crypt/dining_crypt4.nm | 48 +++++++++++++ prism-examples/dining_crypt/dining_crypt5.nm | 50 +++++++++++++ prism-examples/dining_crypt/dining_crypt6.nm | 52 ++++++++++++++ prism-examples/dining_crypt/dining_crypt7.nm | 54 ++++++++++++++ prism-examples/dining_crypt/dining_crypt8.nm | 56 +++++++++++++++ prism-examples/dining_crypt/dining_crypt9.nm | 58 +++++++++++++++ 34 files changed, 676 insertions(+) create mode 100644 prism-examples/dining_crypt/.anonymityN.pctl.pp create mode 100755 prism-examples/dining_crypt/.autopp create mode 100644 prism-examples/dining_crypt/.correctnessN.pctl.pp create mode 100644 prism-examples/dining_crypt/.dining_cryptN.nm.pp create mode 100644 prism-examples/dining_crypt/README create mode 100644 prism-examples/dining_crypt/anonymity10.pctl create mode 100644 prism-examples/dining_crypt/anonymity15.pctl create mode 100644 prism-examples/dining_crypt/anonymity3.pctl create mode 100644 prism-examples/dining_crypt/anonymity4.pctl create mode 100644 prism-examples/dining_crypt/anonymity5.pctl create mode 100644 prism-examples/dining_crypt/anonymity6.pctl create mode 100644 prism-examples/dining_crypt/anonymity7.pctl create mode 100644 prism-examples/dining_crypt/anonymity8.pctl create mode 100644 prism-examples/dining_crypt/anonymity9.pctl create mode 100755 prism-examples/dining_crypt/auto create mode 100644 prism-examples/dining_crypt/correctness10.pctl create mode 100644 prism-examples/dining_crypt/correctness15.pctl create mode 100644 prism-examples/dining_crypt/correctness3.pctl create mode 100644 prism-examples/dining_crypt/correctness4.pctl create mode 100644 prism-examples/dining_crypt/correctness5.pctl create mode 100644 prism-examples/dining_crypt/correctness6.pctl create mode 100644 prism-examples/dining_crypt/correctness7.pctl create mode 100644 prism-examples/dining_crypt/correctness8.pctl create mode 100644 prism-examples/dining_crypt/correctness9.pctl create mode 100644 prism-examples/dining_crypt/dining_crypt10.nm create mode 100644 prism-examples/dining_crypt/dining_crypt15.nm create mode 100644 prism-examples/dining_crypt/dining_crypt3.nm create mode 100644 prism-examples/dining_crypt/dining_crypt3.pctl create mode 100644 prism-examples/dining_crypt/dining_crypt4.nm create mode 100644 prism-examples/dining_crypt/dining_crypt5.nm create mode 100644 prism-examples/dining_crypt/dining_crypt6.nm create mode 100644 prism-examples/dining_crypt/dining_crypt7.nm create mode 100644 prism-examples/dining_crypt/dining_crypt8.nm create mode 100644 prism-examples/dining_crypt/dining_crypt9.nm diff --git a/prism-examples/dining_crypt/.anonymityN.pctl.pp b/prism-examples/dining_crypt/.anonymityN.pctl.pp new file mode 100644 index 00000000..386bc10f --- /dev/null +++ b/prism-examples/dining_crypt/.anonymityN.pctl.pp @@ -0,0 +1,5 @@ +#const N# +const int k; + +Pmin=? [ F (#& j=1:N#s#j#=1#end#) & (#+ j=1:N# #func(floor,func(pow,2,N-j))#*agree#j# #end# = k) {"init"&pay>0}{min} ] +Pmax=? [ F (#& j=1:N#s#j#=1#end#) & (#+ j=1:N# #func(floor,func(pow,2,N-j))#*agree#j# #end# = k) {"init"&pay>0}{max} ] diff --git a/prism-examples/dining_crypt/.autopp b/prism-examples/dining_crypt/.autopp new file mode 100755 index 00000000..d16ac97f --- /dev/null +++ b/prism-examples/dining_crypt/.autopp @@ -0,0 +1,11 @@ +#!/bin/csh + +foreach N ( 3 4 5 6 7 8 9 10 15 ) + echo "Generating for N=$N" + prismpp .dining_cryptN.nm.pp $N >! dining_crypt$N.nm + unix2dos dining_crypt$N.nm + prismpp .correctnessN.pctl.pp $N >! correctness$N.pctl + unix2dos correctness$N.pctl + prismpp .anonymityN.pctl.pp $N >! anonymity$N.pctl + unix2dos anonymity$N.pctl +end diff --git a/prism-examples/dining_crypt/.correctnessN.pctl.pp b/prism-examples/dining_crypt/.correctnessN.pctl.pp new file mode 100644 index 00000000..7dd59c2f --- /dev/null +++ b/prism-examples/dining_crypt/.correctnessN.pctl.pp @@ -0,0 +1,6 @@ +#const N# +// Correctness for the case where the master pays +(pay=0) => P>=1 [ F (#& j=1:N#s#j#=1#end#) & func(mod,(#+ j=1:N#agree#j##end#),2)=#func(mod,N,2)# ] + +// Correctness for the case where a cryptographer pays +(pay>0) => P>=1 [ F (#& j=1:N#s#j#=1#end#) & func(mod,(#+ j=1:N#agree#j##end#),2)=#func(mod,N+1,2)# ] diff --git a/prism-examples/dining_crypt/.dining_cryptN.nm.pp b/prism-examples/dining_crypt/.dining_cryptN.nm.pp new file mode 100644 index 00000000..053374f1 --- /dev/null +++ b/prism-examples/dining_crypt/.dining_cryptN.nm.pp @@ -0,0 +1,48 @@ +#const N# +// model of dining cryptographers +// gxn/dxp 15/11/06 + +mdp + +// constants used in renaming (identities of cryptographers) +#for i=1:N# +const int p#i# = #i#; +#end# + +// global variable which decides who pays +// (0 - master pays, i=1..N - cryptographer i pays) +global pay : [0..#N#]; + +// module for first cryptographer +module crypt1 + + coin1 : [0..2]; // value of its coin + s1 : [0..1]; // its status (0 = not done, 1 = done) + agree1 : [0..1]; // what it states (0 = disagree, 1 = agree) + + // flip coin + [] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2); + + // make statement (once relevant coins have been flipped) + // agree (coins the same and does not pay) + [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay!=p1) -> (s1'=1) & (agree1'=1); + // disagree (coins different and does not pay) + [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1); + // disagree (coins the same and pays) + [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay=p1) -> (s1'=1); + // agree (coins different and pays) + [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1) -> (s1'=1) & (agree1'=1); + + // synchronising loop when finished to avoid deadlock + [done] s1=1 -> true; + +endmodule + +// construct further cryptographers with renaming +#for i=2:N# +module crypt#i# = crypt1 [ coin1=coin#i#, s1=s#i#, agree1=agree#i#, p1=p#i#, coin2=coin#func(mod,i,N)+1# ] endmodule +#end# + +// set of initial states +// (cryptographers in their initial state, "pay" can be anything) +init #& i=1:N# coin#i#=0&s#i#=0&agree#i#=0 #end# endinit diff --git a/prism-examples/dining_crypt/README b/prism-examples/dining_crypt/README new file mode 100644 index 00000000..77e593f7 --- /dev/null +++ b/prism-examples/dining_crypt/README @@ -0,0 +1,10 @@ +This case study is based on the well known dining cryptographers problem [Cha88]. + +For more information, see: http://www.prismmodelchecker.org/casestudies/dining_crypt.php + +===================================================================================== + +[Cha88] +D. Chaum +The Dining Cryptographers Problem: Unconditional Sender and Recipient Untraceability +Journal of Cryptology, vol. 1, pp 65-75, 1988 diff --git a/prism-examples/dining_crypt/anonymity10.pctl b/prism-examples/dining_crypt/anonymity10.pctl new file mode 100644 index 00000000..c867814a --- /dev/null +++ b/prism-examples/dining_crypt/anonymity10.pctl @@ -0,0 +1,4 @@ +const int k; + +Pmin=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1&s10=1) & ( 512*agree1 + 256*agree2 + 128*agree3 + 64*agree4 + 32*agree5 + 16*agree6 + 8*agree7 + 4*agree8 + 2*agree9 + 1*agree10 = k) {"init"&pay>0}{min} ] +Pmax=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1&s10=1) & ( 512*agree1 + 256*agree2 + 128*agree3 + 64*agree4 + 32*agree5 + 16*agree6 + 8*agree7 + 4*agree8 + 2*agree9 + 1*agree10 = k) {"init"&pay>0}{max} ] diff --git a/prism-examples/dining_crypt/anonymity15.pctl b/prism-examples/dining_crypt/anonymity15.pctl new file mode 100644 index 00000000..00eb4572 --- /dev/null +++ b/prism-examples/dining_crypt/anonymity15.pctl @@ -0,0 +1,4 @@ +const int k; + +Pmin=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1&s10=1&s11=1&s12=1&s13=1&s14=1&s15=1) & ( 16384*agree1 + 8192*agree2 + 4096*agree3 + 2048*agree4 + 1024*agree5 + 512*agree6 + 256*agree7 + 128*agree8 + 64*agree9 + 32*agree10 + 16*agree11 + 8*agree12 + 4*agree13 + 2*agree14 + 1*agree15 = k) {"init"&pay>0}{min} ] +Pmax=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1&s10=1&s11=1&s12=1&s13=1&s14=1&s15=1) & ( 16384*agree1 + 8192*agree2 + 4096*agree3 + 2048*agree4 + 1024*agree5 + 512*agree6 + 256*agree7 + 128*agree8 + 64*agree9 + 32*agree10 + 16*agree11 + 8*agree12 + 4*agree13 + 2*agree14 + 1*agree15 = k) {"init"&pay>0}{max} ] diff --git a/prism-examples/dining_crypt/anonymity3.pctl b/prism-examples/dining_crypt/anonymity3.pctl new file mode 100644 index 00000000..5a028c0d --- /dev/null +++ b/prism-examples/dining_crypt/anonymity3.pctl @@ -0,0 +1,4 @@ +const int k; + +Pmin=? [ F (s1=1&s2=1&s3=1) & ( 4*agree1 + 2*agree2 + 1*agree3 = k) {"init"&pay>0}{min} ] +Pmax=? [ F (s1=1&s2=1&s3=1) & ( 4*agree1 + 2*agree2 + 1*agree3 = k) {"init"&pay>0}{max} ] diff --git a/prism-examples/dining_crypt/anonymity4.pctl b/prism-examples/dining_crypt/anonymity4.pctl new file mode 100644 index 00000000..352ce78d --- /dev/null +++ b/prism-examples/dining_crypt/anonymity4.pctl @@ -0,0 +1,4 @@ +const int k; + +Pmin=? [ F (s1=1&s2=1&s3=1&s4=1) & ( 8*agree1 + 4*agree2 + 2*agree3 + 1*agree4 = k) {"init"&pay>0}{min} ] +Pmax=? [ F (s1=1&s2=1&s3=1&s4=1) & ( 8*agree1 + 4*agree2 + 2*agree3 + 1*agree4 = k) {"init"&pay>0}{max} ] diff --git a/prism-examples/dining_crypt/anonymity5.pctl b/prism-examples/dining_crypt/anonymity5.pctl new file mode 100644 index 00000000..2dd01637 --- /dev/null +++ b/prism-examples/dining_crypt/anonymity5.pctl @@ -0,0 +1,4 @@ +const int k; + +Pmin=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1) & ( 16*agree1 + 8*agree2 + 4*agree3 + 2*agree4 + 1*agree5 = k) {"init"&pay>0}{min} ] +Pmax=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1) & ( 16*agree1 + 8*agree2 + 4*agree3 + 2*agree4 + 1*agree5 = k) {"init"&pay>0}{max} ] diff --git a/prism-examples/dining_crypt/anonymity6.pctl b/prism-examples/dining_crypt/anonymity6.pctl new file mode 100644 index 00000000..085b2ca2 --- /dev/null +++ b/prism-examples/dining_crypt/anonymity6.pctl @@ -0,0 +1,4 @@ +const int k; + +Pmin=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1) & ( 32*agree1 + 16*agree2 + 8*agree3 + 4*agree4 + 2*agree5 + 1*agree6 = k) {"init"&pay>0}{min} ] +Pmax=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1) & ( 32*agree1 + 16*agree2 + 8*agree3 + 4*agree4 + 2*agree5 + 1*agree6 = k) {"init"&pay>0}{max} ] diff --git a/prism-examples/dining_crypt/anonymity7.pctl b/prism-examples/dining_crypt/anonymity7.pctl new file mode 100644 index 00000000..eb57ee1b --- /dev/null +++ b/prism-examples/dining_crypt/anonymity7.pctl @@ -0,0 +1,4 @@ +const int k; + +Pmin=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1) & ( 64*agree1 + 32*agree2 + 16*agree3 + 8*agree4 + 4*agree5 + 2*agree6 + 1*agree7 = k) {"init"&pay>0}{min} ] +Pmax=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1) & ( 64*agree1 + 32*agree2 + 16*agree3 + 8*agree4 + 4*agree5 + 2*agree6 + 1*agree7 = k) {"init"&pay>0}{max} ] diff --git a/prism-examples/dining_crypt/anonymity8.pctl b/prism-examples/dining_crypt/anonymity8.pctl new file mode 100644 index 00000000..c270b38a --- /dev/null +++ b/prism-examples/dining_crypt/anonymity8.pctl @@ -0,0 +1,4 @@ +const int k; + +Pmin=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1) & ( 128*agree1 + 64*agree2 + 32*agree3 + 16*agree4 + 8*agree5 + 4*agree6 + 2*agree7 + 1*agree8 = k) {"init"&pay>0}{min} ] +Pmax=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1) & ( 128*agree1 + 64*agree2 + 32*agree3 + 16*agree4 + 8*agree5 + 4*agree6 + 2*agree7 + 1*agree8 = k) {"init"&pay>0}{max} ] diff --git a/prism-examples/dining_crypt/anonymity9.pctl b/prism-examples/dining_crypt/anonymity9.pctl new file mode 100644 index 00000000..19fedc8d --- /dev/null +++ b/prism-examples/dining_crypt/anonymity9.pctl @@ -0,0 +1,4 @@ +const int k; + +Pmin=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1) & ( 256*agree1 + 128*agree2 + 64*agree3 + 32*agree4 + 16*agree5 + 8*agree6 + 4*agree7 + 2*agree8 + 1*agree9 = k) {"init"&pay>0}{min} ] +Pmax=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1) & ( 256*agree1 + 128*agree2 + 64*agree3 + 32*agree4 + 16*agree5 + 8*agree6 + 4*agree7 + 2*agree8 + 1*agree9 = k) {"init"&pay>0}{max} ] diff --git a/prism-examples/dining_crypt/auto b/prism-examples/dining_crypt/auto new file mode 100755 index 00000000..051081ab --- /dev/null +++ b/prism-examples/dining_crypt/auto @@ -0,0 +1,21 @@ +#!/bin/csh + +prism dining_crypt3.nm correctness3.pctl +prism dining_crypt4.nm correctness4.pctl +prism dining_crypt5.nm correctness5.pctl +prism dining_crypt6.nm correctness6.pctl +prism dining_crypt7.nm correctness7.pctl +prism dining_crypt8.nm correctness8.pctl +prism dining_crypt9.nm correctness9.pctl +prism dining_crypt10.nm correctness10.pctl +prism dining_crypt15.nm correctness15.pctl + +prism dining_crypt3.nm anonymity3.pctl -const k=0 -m -nopre +prism dining_crypt4.nm anonymity4.pctl -const k=1 -m -nopre +prism dining_crypt5.nm anonymity5.pctl -const k=0 -m -nopre +prism dining_crypt6.nm anonymity6.pctl -const k=1 -m -nopre +prism dining_crypt7.nm anonymity7.pctl -const k=0 -m -nopre +prism dining_crypt8.nm anonymity8.pctl -const k=1 -m -nopre +prism dining_crypt9.nm anonymity9.pctl -const k=0 -m -nopre +prism dining_crypt10.nm anonymity10.pctl -const k=1 -m -nopre +prism dining_crypt15.nm anonymity15.pctl -const k=0 -m -nopre diff --git a/prism-examples/dining_crypt/correctness10.pctl b/prism-examples/dining_crypt/correctness10.pctl new file mode 100644 index 00000000..eddee01a --- /dev/null +++ b/prism-examples/dining_crypt/correctness10.pctl @@ -0,0 +1,5 @@ +// Correctness for the case where the master pays +(pay=0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1&s10=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8+agree9+agree10),2)=0 ] + +// Correctness for the case where a cryptographer pays +(pay>0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1&s10=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8+agree9+agree10),2)=1 ] diff --git a/prism-examples/dining_crypt/correctness15.pctl b/prism-examples/dining_crypt/correctness15.pctl new file mode 100644 index 00000000..b134e607 --- /dev/null +++ b/prism-examples/dining_crypt/correctness15.pctl @@ -0,0 +1,5 @@ +// Correctness for the case where the master pays +(pay=0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1&s10=1&s11=1&s12=1&s13=1&s14=1&s15=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8+agree9+agree10+agree11+agree12+agree13+agree14+agree15),2)=1 ] + +// Correctness for the case where a cryptographer pays +(pay>0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1&s10=1&s11=1&s12=1&s13=1&s14=1&s15=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8+agree9+agree10+agree11+agree12+agree13+agree14+agree15),2)=0 ] diff --git a/prism-examples/dining_crypt/correctness3.pctl b/prism-examples/dining_crypt/correctness3.pctl new file mode 100644 index 00000000..21db4030 --- /dev/null +++ b/prism-examples/dining_crypt/correctness3.pctl @@ -0,0 +1,5 @@ +// Correctness for the case where the master pays +(pay=0) => P>=1 [ F (s1=1&s2=1&s3=1) & func(mod,(agree1+agree2+agree3),2)=1 ] + +// Correctness for the case where a cryptographer pays +(pay>0) => P>=1 [ F (s1=1&s2=1&s3=1) & func(mod,(agree1+agree2+agree3),2)=0 ] diff --git a/prism-examples/dining_crypt/correctness4.pctl b/prism-examples/dining_crypt/correctness4.pctl new file mode 100644 index 00000000..8aebc456 --- /dev/null +++ b/prism-examples/dining_crypt/correctness4.pctl @@ -0,0 +1,5 @@ +// Correctness for the case where the master pays +(pay=0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1) & func(mod,(agree1+agree2+agree3+agree4),2)=0 ] + +// Correctness for the case where a cryptographer pays +(pay>0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1) & func(mod,(agree1+agree2+agree3+agree4),2)=1 ] diff --git a/prism-examples/dining_crypt/correctness5.pctl b/prism-examples/dining_crypt/correctness5.pctl new file mode 100644 index 00000000..2d9bb8f6 --- /dev/null +++ b/prism-examples/dining_crypt/correctness5.pctl @@ -0,0 +1,5 @@ +// Correctness for the case where the master pays +(pay=0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1) & func(mod,(agree1+agree2+agree3+agree4+agree5),2)=1 ] + +// Correctness for the case where a cryptographer pays +(pay>0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1) & func(mod,(agree1+agree2+agree3+agree4+agree5),2)=0 ] diff --git a/prism-examples/dining_crypt/correctness6.pctl b/prism-examples/dining_crypt/correctness6.pctl new file mode 100644 index 00000000..33a76dca --- /dev/null +++ b/prism-examples/dining_crypt/correctness6.pctl @@ -0,0 +1,5 @@ +// Correctness for the case where the master pays +(pay=0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6),2)=0 ] + +// Correctness for the case where a cryptographer pays +(pay>0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6),2)=1 ] diff --git a/prism-examples/dining_crypt/correctness7.pctl b/prism-examples/dining_crypt/correctness7.pctl new file mode 100644 index 00000000..fb712a8f --- /dev/null +++ b/prism-examples/dining_crypt/correctness7.pctl @@ -0,0 +1,5 @@ +// Correctness for the case where the master pays +(pay=0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7),2)=1 ] + +// Correctness for the case where a cryptographer pays +(pay>0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7),2)=0 ] diff --git a/prism-examples/dining_crypt/correctness8.pctl b/prism-examples/dining_crypt/correctness8.pctl new file mode 100644 index 00000000..fd1e9aca --- /dev/null +++ b/prism-examples/dining_crypt/correctness8.pctl @@ -0,0 +1,5 @@ +// Correctness for the case where the master pays +(pay=0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8),2)=0 ] + +// Correctness for the case where a cryptographer pays +(pay>0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8),2)=1 ] diff --git a/prism-examples/dining_crypt/correctness9.pctl b/prism-examples/dining_crypt/correctness9.pctl new file mode 100644 index 00000000..4a279e94 --- /dev/null +++ b/prism-examples/dining_crypt/correctness9.pctl @@ -0,0 +1,5 @@ +// Correctness for the case where the master pays +(pay=0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8+agree9),2)=1 ] + +// Correctness for the case where a cryptographer pays +(pay>0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8+agree9),2)=0 ] diff --git a/prism-examples/dining_crypt/dining_crypt10.nm b/prism-examples/dining_crypt/dining_crypt10.nm new file mode 100644 index 00000000..6b0ab03e --- /dev/null +++ b/prism-examples/dining_crypt/dining_crypt10.nm @@ -0,0 +1,60 @@ +// model of dining cryptographers +// gxn/dxp 15/11/06 + +mdp + +// constants used in renaming (identities of cryptographers) +const int p1 = 1; +const int p2 = 2; +const int p3 = 3; +const int p4 = 4; +const int p5 = 5; +const int p6 = 6; +const int p7 = 7; +const int p8 = 8; +const int p9 = 9; +const int p10 = 10; + +// global variable which decides who pays +// (0 - master pays, i=1..N - cryptographer i pays) +global pay : [0..10]; + +// module for first cryptographer +module crypt1 + + coin1 : [0..2]; // value of its coin + s1 : [0..1]; // its status (0 = not done, 1 = done) + agree1 : [0..1]; // what it states (0 = disagree, 1 = agree) + + // flip coin + [] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2); + + // make statement (once relevant coins have been flipped) + // agree (coins the same and does not pay) + [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay!=p1) -> (s1'=1) & (agree1'=1); + // disagree (coins different and does not pay) + [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1); + // disagree (coins the same and pays) + [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay=p1) -> (s1'=1); + // agree (coins different and pays) + [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1) -> (s1'=1) & (agree1'=1); + + // synchronising loop when finished to avoid deadlock + [done] s1=1 -> true; + +endmodule + +// construct further cryptographers with renaming +module crypt2 = crypt1 [ coin1=coin2, s1=s2, agree1=agree2, p1=p2, coin2=coin3 ] endmodule +module crypt3 = crypt1 [ coin1=coin3, s1=s3, agree1=agree3, p1=p3, coin2=coin4 ] endmodule +module crypt4 = crypt1 [ coin1=coin4, s1=s4, agree1=agree4, p1=p4, coin2=coin5 ] endmodule +module crypt5 = crypt1 [ coin1=coin5, s1=s5, agree1=agree5, p1=p5, coin2=coin6 ] endmodule +module crypt6 = crypt1 [ coin1=coin6, s1=s6, agree1=agree6, p1=p6, coin2=coin7 ] endmodule +module crypt7 = crypt1 [ coin1=coin7, s1=s7, agree1=agree7, p1=p7, coin2=coin8 ] endmodule +module crypt8 = crypt1 [ coin1=coin8, s1=s8, agree1=agree8, p1=p8, coin2=coin9 ] endmodule +module crypt9 = crypt1 [ coin1=coin9, s1=s9, agree1=agree9, p1=p9, coin2=coin10 ] endmodule +module crypt10 = crypt1 [ coin1=coin10, s1=s10, agree1=agree10, p1=p10, coin2=coin1 ] endmodule + +// set of initial states +// (cryptographers in their initial state, "pay" can be anything) +init coin1=0&s1=0&agree1=0 & coin2=0&s2=0&agree2=0 & coin3=0&s3=0&agree3=0 & coin4=0&s4=0&agree4=0 & coin5=0&s5=0&agree5=0 & coin6=0&s6=0&agree6=0 & coin7=0&s7=0&agree7=0 & coin8=0&s8=0&agree8=0 & coin9=0&s9=0&agree9=0 & coin10=0&s10=0&agree10=0 endinit diff --git a/prism-examples/dining_crypt/dining_crypt15.nm b/prism-examples/dining_crypt/dining_crypt15.nm new file mode 100644 index 00000000..3841d0cc --- /dev/null +++ b/prism-examples/dining_crypt/dining_crypt15.nm @@ -0,0 +1,70 @@ +// model of dining cryptographers +// gxn/dxp 15/11/06 + +mdp + +// constants used in renaming (identities of cryptographers) +const int p1 = 1; +const int p2 = 2; +const int p3 = 3; +const int p4 = 4; +const int p5 = 5; +const int p6 = 6; +const int p7 = 7; +const int p8 = 8; +const int p9 = 9; +const int p10 = 10; +const int p11 = 11; +const int p12 = 12; +const int p13 = 13; +const int p14 = 14; +const int p15 = 15; + +// global variable which decides who pays +// (0 - master pays, i=1..N - cryptographer i pays) +global pay : [0..15]; + +// module for first cryptographer +module crypt1 + + coin1 : [0..2]; // value of its coin + s1 : [0..1]; // its status (0 = not done, 1 = done) + agree1 : [0..1]; // what it states (0 = disagree, 1 = agree) + + // flip coin + [] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2); + + // make statement (once relevant coins have been flipped) + // agree (coins the same and does not pay) + [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay!=p1) -> (s1'=1) & (agree1'=1); + // disagree (coins different and does not pay) + [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1); + // disagree (coins the same and pays) + [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay=p1) -> (s1'=1); + // agree (coins different and pays) + [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1) -> (s1'=1) & (agree1'=1); + + // synchronising loop when finished to avoid deadlock + [done] s1=1 -> true; + +endmodule + +// construct further cryptographers with renaming +module crypt2 = crypt1 [ coin1=coin2, s1=s2, agree1=agree2, p1=p2, coin2=coin3 ] endmodule +module crypt3 = crypt1 [ coin1=coin3, s1=s3, agree1=agree3, p1=p3, coin2=coin4 ] endmodule +module crypt4 = crypt1 [ coin1=coin4, s1=s4, agree1=agree4, p1=p4, coin2=coin5 ] endmodule +module crypt5 = crypt1 [ coin1=coin5, s1=s5, agree1=agree5, p1=p5, coin2=coin6 ] endmodule +module crypt6 = crypt1 [ coin1=coin6, s1=s6, agree1=agree6, p1=p6, coin2=coin7 ] endmodule +module crypt7 = crypt1 [ coin1=coin7, s1=s7, agree1=agree7, p1=p7, coin2=coin8 ] endmodule +module crypt8 = crypt1 [ coin1=coin8, s1=s8, agree1=agree8, p1=p8, coin2=coin9 ] endmodule +module crypt9 = crypt1 [ coin1=coin9, s1=s9, agree1=agree9, p1=p9, coin2=coin10 ] endmodule +module crypt10 = crypt1 [ coin1=coin10, s1=s10, agree1=agree10, p1=p10, coin2=coin11 ] endmodule +module crypt11 = crypt1 [ coin1=coin11, s1=s11, agree1=agree11, p1=p11, coin2=coin12 ] endmodule +module crypt12 = crypt1 [ coin1=coin12, s1=s12, agree1=agree12, p1=p12, coin2=coin13 ] endmodule +module crypt13 = crypt1 [ coin1=coin13, s1=s13, agree1=agree13, p1=p13, coin2=coin14 ] endmodule +module crypt14 = crypt1 [ coin1=coin14, s1=s14, agree1=agree14, p1=p14, coin2=coin15 ] endmodule +module crypt15 = crypt1 [ coin1=coin15, s1=s15, agree1=agree15, p1=p15, coin2=coin1 ] endmodule + +// set of initial states +// (cryptographers in their initial state, "pay" can be anything) +init coin1=0&s1=0&agree1=0 & coin2=0&s2=0&agree2=0 & coin3=0&s3=0&agree3=0 & coin4=0&s4=0&agree4=0 & coin5=0&s5=0&agree5=0 & coin6=0&s6=0&agree6=0 & coin7=0&s7=0&agree7=0 & coin8=0&s8=0&agree8=0 & coin9=0&s9=0&agree9=0 & coin10=0&s10=0&agree10=0 & coin11=0&s11=0&agree11=0 & coin12=0&s12=0&agree12=0 & coin13=0&s13=0&agree13=0 & coin14=0&s14=0&agree14=0 & coin15=0&s15=0&agree15=0 endinit diff --git a/prism-examples/dining_crypt/dining_crypt3.nm b/prism-examples/dining_crypt/dining_crypt3.nm new file mode 100644 index 00000000..222151d5 --- /dev/null +++ b/prism-examples/dining_crypt/dining_crypt3.nm @@ -0,0 +1,46 @@ +// model of dining cryptographers +// gxn/dxp 15/11/06 + +mdp + +// constants used in renaming (identities of cryptographers) +const int p1 = 1; +const int p2 = 2; +const int p3 = 3; + +// global variable which decides who pays +// (0 - master pays, i=1..N - cryptographer i pays) +global pay : [0..3]; + +// module for first cryptographer +module crypt1 + + coin1 : [0..2]; // value of its coin + s1 : [0..1]; // its status (0 = not done, 1 = done) + agree1 : [0..1]; // what it states (0 = disagree, 1 = agree) + + // flip coin + [] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2); + + // make statement (once relevant coins have been flipped) + // agree (coins the same and does not pay) + [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay!=p1) -> (s1'=1) & (agree1'=1); + // disagree (coins different and does not pay) + [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1); + // disagree (coins the same and pays) + [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay=p1) -> (s1'=1); + // agree (coins different and pays) + [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1) -> (s1'=1) & (agree1'=1); + + // synchronising loop when finished to avoid deadlock + [done] s1=1 -> true; + +endmodule + +// construct further cryptographers with renaming +module crypt2 = crypt1 [ coin1=coin2, s1=s2, agree1=agree2, p1=p2, coin2=coin3 ] endmodule +module crypt3 = crypt1 [ coin1=coin3, s1=s3, agree1=agree3, p1=p3, coin2=coin1 ] endmodule + +// set of initial states +// (cryptographers in their initial state, "pay" can be anything) +init coin1=0&s1=0&agree1=0 & coin2=0&s2=0&agree2=0 & coin3=0&s3=0&agree3=0 endinit diff --git a/prism-examples/dining_crypt/dining_crypt3.pctl b/prism-examples/dining_crypt/dining_crypt3.pctl new file mode 100644 index 00000000..e69de29b diff --git a/prism-examples/dining_crypt/dining_crypt4.nm b/prism-examples/dining_crypt/dining_crypt4.nm new file mode 100644 index 00000000..390ccdd0 --- /dev/null +++ b/prism-examples/dining_crypt/dining_crypt4.nm @@ -0,0 +1,48 @@ +// model of dining cryptographers +// gxn/dxp 15/11/06 + +mdp + +// constants used in renaming (identities of cryptographers) +const int p1 = 1; +const int p2 = 2; +const int p3 = 3; +const int p4 = 4; + +// global variable which decides who pays +// (0 - master pays, i=1..N - cryptographer i pays) +global pay : [0..4]; + +// module for first cryptographer +module crypt1 + + coin1 : [0..2]; // value of its coin + s1 : [0..1]; // its status (0 = not done, 1 = done) + agree1 : [0..1]; // what it states (0 = disagree, 1 = agree) + + // flip coin + [] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2); + + // make statement (once relevant coins have been flipped) + // agree (coins the same and does not pay) + [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay!=p1) -> (s1'=1) & (agree1'=1); + // disagree (coins different and does not pay) + [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1); + // disagree (coins the same and pays) + [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay=p1) -> (s1'=1); + // agree (coins different and pays) + [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1) -> (s1'=1) & (agree1'=1); + + // synchronising loop when finished to avoid deadlock + [done] s1=1 -> true; + +endmodule + +// construct further cryptographers with renaming +module crypt2 = crypt1 [ coin1=coin2, s1=s2, agree1=agree2, p1=p2, coin2=coin3 ] endmodule +module crypt3 = crypt1 [ coin1=coin3, s1=s3, agree1=agree3, p1=p3, coin2=coin4 ] endmodule +module crypt4 = crypt1 [ coin1=coin4, s1=s4, agree1=agree4, p1=p4, coin2=coin1 ] endmodule + +// set of initial states +// (cryptographers in their initial state, "pay" can be anything) +init coin1=0&s1=0&agree1=0 & coin2=0&s2=0&agree2=0 & coin3=0&s3=0&agree3=0 & coin4=0&s4=0&agree4=0 endinit diff --git a/prism-examples/dining_crypt/dining_crypt5.nm b/prism-examples/dining_crypt/dining_crypt5.nm new file mode 100644 index 00000000..5d4d678d --- /dev/null +++ b/prism-examples/dining_crypt/dining_crypt5.nm @@ -0,0 +1,50 @@ +// model of dining cryptographers +// gxn/dxp 15/11/06 + +mdp + +// constants used in renaming (identities of cryptographers) +const int p1 = 1; +const int p2 = 2; +const int p3 = 3; +const int p4 = 4; +const int p5 = 5; + +// global variable which decides who pays +// (0 - master pays, i=1..N - cryptographer i pays) +global pay : [0..5]; + +// module for first cryptographer +module crypt1 + + coin1 : [0..2]; // value of its coin + s1 : [0..1]; // its status (0 = not done, 1 = done) + agree1 : [0..1]; // what it states (0 = disagree, 1 = agree) + + // flip coin + [] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2); + + // make statement (once relevant coins have been flipped) + // agree (coins the same and does not pay) + [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay!=p1) -> (s1'=1) & (agree1'=1); + // disagree (coins different and does not pay) + [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1); + // disagree (coins the same and pays) + [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay=p1) -> (s1'=1); + // agree (coins different and pays) + [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1) -> (s1'=1) & (agree1'=1); + + // synchronising loop when finished to avoid deadlock + [done] s1=1 -> true; + +endmodule + +// construct further cryptographers with renaming +module crypt2 = crypt1 [ coin1=coin2, s1=s2, agree1=agree2, p1=p2, coin2=coin3 ] endmodule +module crypt3 = crypt1 [ coin1=coin3, s1=s3, agree1=agree3, p1=p3, coin2=coin4 ] endmodule +module crypt4 = crypt1 [ coin1=coin4, s1=s4, agree1=agree4, p1=p4, coin2=coin5 ] endmodule +module crypt5 = crypt1 [ coin1=coin5, s1=s5, agree1=agree5, p1=p5, coin2=coin1 ] endmodule + +// set of initial states +// (cryptographers in their initial state, "pay" can be anything) +init coin1=0&s1=0&agree1=0 & coin2=0&s2=0&agree2=0 & coin3=0&s3=0&agree3=0 & coin4=0&s4=0&agree4=0 & coin5=0&s5=0&agree5=0 endinit diff --git a/prism-examples/dining_crypt/dining_crypt6.nm b/prism-examples/dining_crypt/dining_crypt6.nm new file mode 100644 index 00000000..35c92144 --- /dev/null +++ b/prism-examples/dining_crypt/dining_crypt6.nm @@ -0,0 +1,52 @@ +// model of dining cryptographers +// gxn/dxp 15/11/06 + +mdp + +// constants used in renaming (identities of cryptographers) +const int p1 = 1; +const int p2 = 2; +const int p3 = 3; +const int p4 = 4; +const int p5 = 5; +const int p6 = 6; + +// global variable which decides who pays +// (0 - master pays, i=1..N - cryptographer i pays) +global pay : [0..6]; + +// module for first cryptographer +module crypt1 + + coin1 : [0..2]; // value of its coin + s1 : [0..1]; // its status (0 = not done, 1 = done) + agree1 : [0..1]; // what it states (0 = disagree, 1 = agree) + + // flip coin + [] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2); + + // make statement (once relevant coins have been flipped) + // agree (coins the same and does not pay) + [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay!=p1) -> (s1'=1) & (agree1'=1); + // disagree (coins different and does not pay) + [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1); + // disagree (coins the same and pays) + [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay=p1) -> (s1'=1); + // agree (coins different and pays) + [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1) -> (s1'=1) & (agree1'=1); + + // synchronising loop when finished to avoid deadlock + [done] s1=1 -> true; + +endmodule + +// construct further cryptographers with renaming +module crypt2 = crypt1 [ coin1=coin2, s1=s2, agree1=agree2, p1=p2, coin2=coin3 ] endmodule +module crypt3 = crypt1 [ coin1=coin3, s1=s3, agree1=agree3, p1=p3, coin2=coin4 ] endmodule +module crypt4 = crypt1 [ coin1=coin4, s1=s4, agree1=agree4, p1=p4, coin2=coin5 ] endmodule +module crypt5 = crypt1 [ coin1=coin5, s1=s5, agree1=agree5, p1=p5, coin2=coin6 ] endmodule +module crypt6 = crypt1 [ coin1=coin6, s1=s6, agree1=agree6, p1=p6, coin2=coin1 ] endmodule + +// set of initial states +// (cryptographers in their initial state, "pay" can be anything) +init coin1=0&s1=0&agree1=0 & coin2=0&s2=0&agree2=0 & coin3=0&s3=0&agree3=0 & coin4=0&s4=0&agree4=0 & coin5=0&s5=0&agree5=0 & coin6=0&s6=0&agree6=0 endinit diff --git a/prism-examples/dining_crypt/dining_crypt7.nm b/prism-examples/dining_crypt/dining_crypt7.nm new file mode 100644 index 00000000..b57ad0fa --- /dev/null +++ b/prism-examples/dining_crypt/dining_crypt7.nm @@ -0,0 +1,54 @@ +// model of dining cryptographers +// gxn/dxp 15/11/06 + +mdp + +// constants used in renaming (identities of cryptographers) +const int p1 = 1; +const int p2 = 2; +const int p3 = 3; +const int p4 = 4; +const int p5 = 5; +const int p6 = 6; +const int p7 = 7; + +// global variable which decides who pays +// (0 - master pays, i=1..N - cryptographer i pays) +global pay : [0..7]; + +// module for first cryptographer +module crypt1 + + coin1 : [0..2]; // value of its coin + s1 : [0..1]; // its status (0 = not done, 1 = done) + agree1 : [0..1]; // what it states (0 = disagree, 1 = agree) + + // flip coin + [] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2); + + // make statement (once relevant coins have been flipped) + // agree (coins the same and does not pay) + [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay!=p1) -> (s1'=1) & (agree1'=1); + // disagree (coins different and does not pay) + [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1); + // disagree (coins the same and pays) + [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay=p1) -> (s1'=1); + // agree (coins different and pays) + [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1) -> (s1'=1) & (agree1'=1); + + // synchronising loop when finished to avoid deadlock + [done] s1=1 -> true; + +endmodule + +// construct further cryptographers with renaming +module crypt2 = crypt1 [ coin1=coin2, s1=s2, agree1=agree2, p1=p2, coin2=coin3 ] endmodule +module crypt3 = crypt1 [ coin1=coin3, s1=s3, agree1=agree3, p1=p3, coin2=coin4 ] endmodule +module crypt4 = crypt1 [ coin1=coin4, s1=s4, agree1=agree4, p1=p4, coin2=coin5 ] endmodule +module crypt5 = crypt1 [ coin1=coin5, s1=s5, agree1=agree5, p1=p5, coin2=coin6 ] endmodule +module crypt6 = crypt1 [ coin1=coin6, s1=s6, agree1=agree6, p1=p6, coin2=coin7 ] endmodule +module crypt7 = crypt1 [ coin1=coin7, s1=s7, agree1=agree7, p1=p7, coin2=coin1 ] endmodule + +// set of initial states +// (cryptographers in their initial state, "pay" can be anything) +init coin1=0&s1=0&agree1=0 & coin2=0&s2=0&agree2=0 & coin3=0&s3=0&agree3=0 & coin4=0&s4=0&agree4=0 & coin5=0&s5=0&agree5=0 & coin6=0&s6=0&agree6=0 & coin7=0&s7=0&agree7=0 endinit diff --git a/prism-examples/dining_crypt/dining_crypt8.nm b/prism-examples/dining_crypt/dining_crypt8.nm new file mode 100644 index 00000000..a02cebc4 --- /dev/null +++ b/prism-examples/dining_crypt/dining_crypt8.nm @@ -0,0 +1,56 @@ +// model of dining cryptographers +// gxn/dxp 15/11/06 + +mdp + +// constants used in renaming (identities of cryptographers) +const int p1 = 1; +const int p2 = 2; +const int p3 = 3; +const int p4 = 4; +const int p5 = 5; +const int p6 = 6; +const int p7 = 7; +const int p8 = 8; + +// global variable which decides who pays +// (0 - master pays, i=1..N - cryptographer i pays) +global pay : [0..8]; + +// module for first cryptographer +module crypt1 + + coin1 : [0..2]; // value of its coin + s1 : [0..1]; // its status (0 = not done, 1 = done) + agree1 : [0..1]; // what it states (0 = disagree, 1 = agree) + + // flip coin + [] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2); + + // make statement (once relevant coins have been flipped) + // agree (coins the same and does not pay) + [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay!=p1) -> (s1'=1) & (agree1'=1); + // disagree (coins different and does not pay) + [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1); + // disagree (coins the same and pays) + [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay=p1) -> (s1'=1); + // agree (coins different and pays) + [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1) -> (s1'=1) & (agree1'=1); + + // synchronising loop when finished to avoid deadlock + [done] s1=1 -> true; + +endmodule + +// construct further cryptographers with renaming +module crypt2 = crypt1 [ coin1=coin2, s1=s2, agree1=agree2, p1=p2, coin2=coin3 ] endmodule +module crypt3 = crypt1 [ coin1=coin3, s1=s3, agree1=agree3, p1=p3, coin2=coin4 ] endmodule +module crypt4 = crypt1 [ coin1=coin4, s1=s4, agree1=agree4, p1=p4, coin2=coin5 ] endmodule +module crypt5 = crypt1 [ coin1=coin5, s1=s5, agree1=agree5, p1=p5, coin2=coin6 ] endmodule +module crypt6 = crypt1 [ coin1=coin6, s1=s6, agree1=agree6, p1=p6, coin2=coin7 ] endmodule +module crypt7 = crypt1 [ coin1=coin7, s1=s7, agree1=agree7, p1=p7, coin2=coin8 ] endmodule +module crypt8 = crypt1 [ coin1=coin8, s1=s8, agree1=agree8, p1=p8, coin2=coin1 ] endmodule + +// set of initial states +// (cryptographers in their initial state, "pay" can be anything) +init coin1=0&s1=0&agree1=0 & coin2=0&s2=0&agree2=0 & coin3=0&s3=0&agree3=0 & coin4=0&s4=0&agree4=0 & coin5=0&s5=0&agree5=0 & coin6=0&s6=0&agree6=0 & coin7=0&s7=0&agree7=0 & coin8=0&s8=0&agree8=0 endinit diff --git a/prism-examples/dining_crypt/dining_crypt9.nm b/prism-examples/dining_crypt/dining_crypt9.nm new file mode 100644 index 00000000..485345d2 --- /dev/null +++ b/prism-examples/dining_crypt/dining_crypt9.nm @@ -0,0 +1,58 @@ +// model of dining cryptographers +// gxn/dxp 15/11/06 + +mdp + +// constants used in renaming (identities of cryptographers) +const int p1 = 1; +const int p2 = 2; +const int p3 = 3; +const int p4 = 4; +const int p5 = 5; +const int p6 = 6; +const int p7 = 7; +const int p8 = 8; +const int p9 = 9; + +// global variable which decides who pays +// (0 - master pays, i=1..N - cryptographer i pays) +global pay : [0..9]; + +// module for first cryptographer +module crypt1 + + coin1 : [0..2]; // value of its coin + s1 : [0..1]; // its status (0 = not done, 1 = done) + agree1 : [0..1]; // what it states (0 = disagree, 1 = agree) + + // flip coin + [] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2); + + // make statement (once relevant coins have been flipped) + // agree (coins the same and does not pay) + [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay!=p1) -> (s1'=1) & (agree1'=1); + // disagree (coins different and does not pay) + [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1); + // disagree (coins the same and pays) + [] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay=p1) -> (s1'=1); + // agree (coins different and pays) + [] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1) -> (s1'=1) & (agree1'=1); + + // synchronising loop when finished to avoid deadlock + [done] s1=1 -> true; + +endmodule + +// construct further cryptographers with renaming +module crypt2 = crypt1 [ coin1=coin2, s1=s2, agree1=agree2, p1=p2, coin2=coin3 ] endmodule +module crypt3 = crypt1 [ coin1=coin3, s1=s3, agree1=agree3, p1=p3, coin2=coin4 ] endmodule +module crypt4 = crypt1 [ coin1=coin4, s1=s4, agree1=agree4, p1=p4, coin2=coin5 ] endmodule +module crypt5 = crypt1 [ coin1=coin5, s1=s5, agree1=agree5, p1=p5, coin2=coin6 ] endmodule +module crypt6 = crypt1 [ coin1=coin6, s1=s6, agree1=agree6, p1=p6, coin2=coin7 ] endmodule +module crypt7 = crypt1 [ coin1=coin7, s1=s7, agree1=agree7, p1=p7, coin2=coin8 ] endmodule +module crypt8 = crypt1 [ coin1=coin8, s1=s8, agree1=agree8, p1=p8, coin2=coin9 ] endmodule +module crypt9 = crypt1 [ coin1=coin9, s1=s9, agree1=agree9, p1=p9, coin2=coin1 ] endmodule + +// set of initial states +// (cryptographers in their initial state, "pay" can be anything) +init coin1=0&s1=0&agree1=0 & coin2=0&s2=0&agree2=0 & coin3=0&s3=0&agree3=0 & coin4=0&s4=0&agree4=0 & coin5=0&s5=0&agree5=0 & coin6=0&s6=0&agree6=0 & coin7=0&s7=0&agree7=0 & coin8=0&s8=0&agree8=0 & coin9=0&s9=0&agree9=0 endinit