From 3cb999f8200fd2c88e36f3af6af21add91e7106a Mon Sep 17 00:00:00 2001 From: gijs Date: Mon, 23 May 2005 12:35:58 +0000 Subject: [PATCH] Replaced all tabs by spaces. --- spdl/SPORE/andrew-ban-concrete.spdl | 44 +++++----- spdl/SPORE/andrew-ban.spdl | 58 ++++++------- spdl/SPORE/andrew-lowe-ban.spdl | 50 ++++++------ spdl/SPORE/andrew.spdl | 50 ++++++------ spdl/SPORE/ccitt509-1.spdl | 24 +++--- spdl/SPORE/ccitt509-1c.spdl | 24 +++--- spdl/SPORE/ccitt509-3.spdl | 24 +++--- spdl/SPORE/ccitt509-ban3.spdl | 20 ++--- spdl/SPORE/denning-sacco-lowe.spdl | 40 ++++----- spdl/SPORE/denning-sacco.spdl | 44 +++++----- spdl/SPORE/kaochow-v2.spdl | 66 +++++++-------- spdl/SPORE/kaochow-v3.spdl | 70 ++++++++-------- spdl/SPORE/kaochow.spdl | 66 +++++++-------- spdl/SPORE/ksl-lowe.spdl | 94 +++++++++++----------- spdl/SPORE/ksl.spdl | 94 +++++++++++----------- spdl/SPORE/needham-schroeder-lowe.spdl | 16 ++-- spdl/SPORE/needham-schroeder-sk-amend.spdl | 14 ++-- spdl/SPORE/needham-schroeder-sk.spdl | 16 ++-- spdl/SPORE/needham-schroeder.spdl | 16 ++-- spdl/SPORE/neumannstub-hwang.spdl | 76 ++++++++--------- spdl/SPORE/neumannstub.spdl | 76 ++++++++--------- spdl/SPORE/otwayrees.spdl | 60 +++++++------- spdl/SPORE/smartright.spdl | 18 ++--- spdl/SPORE/splice-as-cj.spdl | 72 ++++++++--------- spdl/SPORE/splice-as-hc.spdl | 72 ++++++++--------- spdl/SPORE/splice-as.spdl | 72 ++++++++--------- spdl/SPORE/tmn.spdl | 50 ++++++------ spdl/SPORE/wmf-lowe.spdl | 36 ++++----- spdl/SPORE/wmf.spdl | 36 ++++----- spdl/SPORE/woo-lam-pi-1.spdl | 24 +++--- spdl/SPORE/woo-lam-pi-2.spdl | 24 +++--- spdl/SPORE/woo-lam-pi-3.spdl | 24 +++--- spdl/SPORE/woo-lam-pi-f.spdl | 24 +++--- spdl/SPORE/woo-lam-pi.spdl | 24 +++--- spdl/SPORE/woo-lam.spdl | 30 +++---- spdl/SPORE/yahalom-ban.spdl | 60 +++++++------- spdl/SPORE/yahalom-lowe.spdl | 58 ++++++------- spdl/SPORE/yahalom-paulson.spdl | 60 +++++++------- spdl/SPORE/yahalom.spdl | 60 +++++++------- 39 files changed, 893 insertions(+), 893 deletions(-) diff --git a/spdl/SPORE/andrew-ban-concrete.spdl b/spdl/SPORE/andrew-ban-concrete.spdl index 059f917..7cbde7c 100644 --- a/spdl/SPORE/andrew-ban-concrete.spdl +++ b/spdl/SPORE/andrew-ban-concrete.spdl @@ -24,33 +24,33 @@ secret k: Function; protocol andrewConcrete(I,R) { - role I - { - const ni: Nonce; - var nr: Nonce; + role I + { + const ni: Nonce; + var nr: Nonce; var kir: SessionKey; - send_1(I,R, I,ni ); - read_2(R,I, {ni,kir}k(I,R) ); - send_3(I,R, {ni}kir); + send_1(I,R, I,ni ); + read_2(R,I, {ni,kir}k(I,R) ); + send_3(I,R, {ni}kir); claim_4(I,Secret,kir); - claim_5(I,Nisynch); - read_6(R,I, nr); - } - - role R - { - var ni: Nonce; - const nr: Nonce; + claim_5(I,Nisynch); + read_6(R,I, nr); + } + + role R + { + var ni: Nonce; + const nr: Nonce; const kir: SessionKey; - read_1(I,R, I,ni ); - send_2(R,I, {ni,kir}k(I,R) ); - read_3(I,R, {ni}kir); - send_6(R,I, nr); - claim_7(R,Secret,kir); - claim_8(R,Nisynch); - } + read_1(I,R, I,ni ); + send_2(R,I, {ni,kir}k(I,R) ); + read_3(I,R, {ni}kir); + send_6(R,I, nr); + claim_7(R,Secret,kir); + claim_8(R,Nisynch); + } } const Alice,Bob,Eve: Agent; diff --git a/spdl/SPORE/andrew-ban.spdl b/spdl/SPORE/andrew-ban.spdl index 1aa9b8b..dee1d2f 100644 --- a/spdl/SPORE/andrew-ban.spdl +++ b/spdl/SPORE/andrew-ban.spdl @@ -16,37 +16,37 @@ secret k: Function; protocol andrewBan(I,R) { - role I - { - const ni: Nonce; - var nr,nr2: Nonce; - var kir: SessionKey; + role I + { + const ni: Nonce; + var nr,nr2: Nonce; + var kir: SessionKey; - send_1(I,R, I,{ni}k(I,R) ); - read_2(R,I, {ni,nr}k(I,R) ); - send_3(I,R, {nr}k(I,R) ); - read_4(R,I, {kir,nr2,ni}k(I,R) ); - claim_5(I,Nisynch); - claim_5b(I,Niagree); - claim_6(I,Secret, kir); - claim_7(I,Secret, k(I,R)); - } - - role R - { - var ni: Nonce; - const nr,nr2: Nonce; - const kir: SessionKey; + send_1(I,R, I,{ni}k(I,R) ); + read_2(R,I, {ni,nr}k(I,R) ); + send_3(I,R, {nr}k(I,R) ); + read_4(R,I, {kir,nr2,ni}k(I,R) ); + claim_5(I,Nisynch); + claim_5b(I,Niagree); + claim_6(I,Secret, kir); + claim_7(I,Secret, k(I,R)); + } + + role R + { + var ni: Nonce; + const nr,nr2: Nonce; + const kir: SessionKey; - read_1(I,R, I,{ni}k(I,R) ); - send_2(R,I, {ni,nr}k(I,R) ); - read_3(I,R, {nr}k(I,R) ); - send_4(R,I, {kir,nr2,ni}k(I,R) ); - claim_8(R,Nisynch); - claim_8b(R,Niagree); - claim_9(R,Secret, kir); - claim_10(R,Secret, k(I,R)); - } + read_1(I,R, I,{ni}k(I,R) ); + send_2(R,I, {ni,nr}k(I,R) ); + read_3(I,R, {nr}k(I,R) ); + send_4(R,I, {kir,nr2,ni}k(I,R) ); + claim_8(R,Nisynch); + claim_8b(R,Niagree); + claim_9(R,Secret, kir); + claim_10(R,Secret, k(I,R)); + } } const Alice,Bob,Eve: Agent; diff --git a/spdl/SPORE/andrew-lowe-ban.spdl b/spdl/SPORE/andrew-lowe-ban.spdl index 6693afb..bbb0468 100644 --- a/spdl/SPORE/andrew-lowe-ban.spdl +++ b/spdl/SPORE/andrew-lowe-ban.spdl @@ -23,33 +23,33 @@ secret k: Function; protocol andrewLoweBan(I,R) { - role I - { - const ni: Nonce; - var nr: Nonce; - var kir: SessionKey; + role I + { + const ni: Nonce; + var nr: Nonce; + var kir: SessionKey; - send_1(I,R, I,ni ); - read_2(R,I, {ni,kir,R}k(I,R) ); - send_3(I,R, {ni}kir ); - claim_5(I,Nisynch); - claim_6(I,Secret, kir); - read_4(R,I, nr ); - } - - role R - { - var ni: Nonce; - const nr: Nonce; - const kir: SessionKey; + send_1(I,R, I,ni ); + read_2(R,I, {ni,kir,R}k(I,R) ); + send_3(I,R, {ni}kir ); + claim_5(I,Nisynch); + claim_6(I,Secret, kir); + read_4(R,I, nr ); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + const kir: SessionKey; - read_1(I,R, I,ni ); - send_2(R,I, {ni,kir,R}k(I,R) ); - read_3(I,R, {ni}kir ); - send_4(R,I, nr ); - claim_8(R,Nisynch); - claim_9(R,Secret, kir); - } + read_1(I,R, I,ni ); + send_2(R,I, {ni,kir,R}k(I,R) ); + read_3(I,R, {ni}kir ); + send_4(R,I, nr ); + claim_8(R,Nisynch); + claim_9(R,Secret, kir); + } } const Alice,Bob,Eve: Agent; diff --git a/spdl/SPORE/andrew.spdl b/spdl/SPORE/andrew.spdl index ae53219..bd88ebd 100644 --- a/spdl/SPORE/andrew.spdl +++ b/spdl/SPORE/andrew.spdl @@ -15,33 +15,33 @@ const succ: Function; protocol andrew(I,R) { - role I - { - const ni: Nonce; - var nr,nr2: Nonce; - var kir: SessionKey; + role I + { + const ni: Nonce; + var nr,nr2: Nonce; + var kir: SessionKey; - send_1(I,R, I,{ni}k(I,R) ); - read_2(R,I, {succ(ni),nr}k(I,R) ); - send_3(I,R, {succ(nr)}k(I,R) ); - read_4(R,I, {kir,nr2}k(I,R) ); - claim_5(I,Secret,kir); - claim_6(I,Nisynch); - } - - role R - { - var ni: Nonce; - const nr,nr2: Nonce; - const kir: SessionKey; + send_1(I,R, I,{ni}k(I,R) ); + read_2(R,I, {succ(ni),nr}k(I,R) ); + send_3(I,R, {succ(nr)}k(I,R) ); + read_4(R,I, {kir,nr2}k(I,R) ); + claim_5(I,Secret,kir); + claim_6(I,Nisynch); + } + + role R + { + var ni: Nonce; + const nr,nr2: Nonce; + const kir: SessionKey; - read_1(I,R, I,{ni}k(I,R) ); - send_2(R,I, {succ(ni),nr}k(I,R) ); - read_3(I,R, {succ(nr)}k(I,R) ); - send_4(R,I, {kir,nr2}k(I,R) ); - claim_7(R,Secret,kir); - claim_8(R,Nisynch); - } + read_1(I,R, I,{ni}k(I,R) ); + send_2(R,I, {succ(ni),nr}k(I,R) ); + read_3(I,R, {succ(nr)}k(I,R) ); + send_4(R,I, {kir,nr2}k(I,R) ); + claim_7(R,Secret,kir); + claim_8(R,Nisynch); + } } const Alice,Bob,Eve: Agent; diff --git a/spdl/SPORE/ccitt509-1.spdl b/spdl/SPORE/ccitt509-1.spdl index 4f84af6..8cd3354 100644 --- a/spdl/SPORE/ccitt509-1.spdl +++ b/spdl/SPORE/ccitt509-1.spdl @@ -16,24 +16,24 @@ usertype Timestamp; protocol ccitt5091(I,R) { - role I - { - const Ta: Timestamp; + role I + { + const Ta: Timestamp; const Na,Xa,Ya: Nonce; - send_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I)); + send_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I)); # claim_2(I,Nisynch); # This claim is useless as there are no preceding read events - } - - role R - { - var Ta: Timestamp; + } + + role R + { + var Ta: Timestamp; var Na,Xa,Ya: Nonce; - read_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I)); - claim_3(R,Nisynch); + read_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I)); + claim_3(R,Nisynch); # There should also be Fresh Xa and Fresh Ya claims here - } + } } const Alice,Bob,Eve: Agent; diff --git a/spdl/SPORE/ccitt509-1c.spdl b/spdl/SPORE/ccitt509-1c.spdl index e6fc1db..a8b8560 100644 --- a/spdl/SPORE/ccitt509-1c.spdl +++ b/spdl/SPORE/ccitt509-1c.spdl @@ -15,24 +15,24 @@ usertype Timestamp; protocol ccitt5091c(I,R) { - role I - { - const Ta: Timestamp; + role I + { + const Ta: Timestamp; const Na,Xa,Ya: Nonce; - send_1(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I)); + send_1(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I)); # claim_2(I,Nisynch); # This claim is useless as there are no preceding read events - } - - role R - { - var Ta: Timestamp; + } + + role R + { + var Ta: Timestamp; var Na,Xa,Ya: Nonce; - read_1(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I)); - claim_3(R,Nisynch); + read_1(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I)); + claim_3(R,Nisynch); # There should also be Fresh Xa and Fresh Ya claims here - } + } } const Alice,Bob,Eve: Agent; diff --git a/spdl/SPORE/ccitt509-3.spdl b/spdl/SPORE/ccitt509-3.spdl index c42bba0..dbb9e87 100644 --- a/spdl/SPORE/ccitt509-3.spdl +++ b/spdl/SPORE/ccitt509-3.spdl @@ -15,31 +15,31 @@ usertype Timestamp; protocol ccitt5093(I,R) { - role I - { - const Ta: Timestamp; + role I + { + const Ta: Timestamp; var Tb: Timestamp; const Na,Xa,Ya: Nonce; var Xb,Nb,Yb: Nonce; - send_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I)); + send_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I)); read_2(R,I, R,{Tb, Nb, I, Na, Xb,{Yb}pk(I)}sk(R)); send_3(I,R, I, {Nb}sk(I)); claim_4(I,Nisynch); - } - - role R - { - var Ta: Timestamp; + } + + role R + { + var Ta: Timestamp; const Tb: Timestamp; var Na,Xa,Ya: Nonce; const Xb,Yb,Nb: Nonce; - read_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I)); + read_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I)); send_2(R,I, R,{Tb, Nb, I, Na, Xb,{Yb}pk(I)}sk(R)); read_3(I,R, I, {Nb}sk(I)); - claim_5(R,Nisynch); + claim_5(R,Nisynch); # There should also be Fresh Xa and Fresh Ya claims here - } + } } const Alice,Bob,Eve: Agent; diff --git a/spdl/SPORE/ccitt509-ban3.spdl b/spdl/SPORE/ccitt509-ban3.spdl index d01a089..b69c34b 100644 --- a/spdl/SPORE/ccitt509-ban3.spdl +++ b/spdl/SPORE/ccitt509-ban3.spdl @@ -17,28 +17,28 @@ inversekeys(pk,sk); protocol ccitt509ban3(I,R) { - role I - { + role I + { const Na,Xa,Ya: Nonce; var Xb,Nb,Yb: Nonce; - send_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I)); + send_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I)); read_2(R,I, R,{Nb, I, Na, Xb,{Yb}pk(I)}sk(R)); send_3(I,R, I,{R, Nb}sk(I)); claim_4(I,Nisynch); - } - - role R - { + } + + role R + { var Na,Xa,Ya: Nonce; const Xb,Yb,Nb: Nonce; - read_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I)); + read_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I)); send_2(R,I, R,{Nb, I, Na, Xb,{Yb}pk(I)}sk(R)); read_3(I,R, I,{R, Nb}sk(I)); - claim_5(R,Nisynch); + claim_5(R,Nisynch); # There should also be Fresh Xa and Fresh Ya claims here - } + } } const Alice,Bob,Eve: Agent; diff --git a/spdl/SPORE/denning-sacco-lowe.spdl b/spdl/SPORE/denning-sacco-lowe.spdl index fde57ed..2c4bb10 100644 --- a/spdl/SPORE/denning-sacco-lowe.spdl +++ b/spdl/SPORE/denning-sacco-lowe.spdl @@ -21,42 +21,42 @@ const dec: PseudoFunction; protocol denningSaccoLowe(I,R,S) { - role I - { + role I + { var W: Ticket; - var Kir: SessionKey; + var Kir: SessionKey; var T: TimeStamp; var Nr: Nonce; - send_1(I,S, I,R ); - read_2(S,I, {R, Kir, T, W}k(I,S) ); - send_3(I,R, W); + send_1(I,S, I,R ); + read_2(S,I, {R, Kir, T, W}k(I,S) ); + send_3(I,R, W); read_4(R,I, {Nr}Kir); send_5(I,R, {{Nr}dec}Kir); - claim_6(I,Niagree); - } - - role R - { + claim_6(I,Niagree); + } + + role R + { var Kir: SessionKey; var T: TimeStamp; const Nr: Nonce; - read_3(I,R, {Kir,I,T}k(R,S)); + read_3(I,R, {Kir,I,T}k(R,S)); send_4(R,I, {Nr}Kir); read_5(I,R, {{Nr}dec}Kir); - claim_8(R,Niagree); - } - + claim_8(R,Niagree); + } + role S - { + { var W: Ticket; - const Kir: SessionKey; + const Kir: SessionKey; const T: TimeStamp; - read_1(I,S, I,R ); - send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S)); - } + read_1(I,S, I,R ); + send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S)); + } } const Alice,Bob,Simon,Eve: Agent; diff --git a/spdl/SPORE/denning-sacco.spdl b/spdl/SPORE/denning-sacco.spdl index 1b8e6b6..2b27823 100644 --- a/spdl/SPORE/denning-sacco.spdl +++ b/spdl/SPORE/denning-sacco.spdl @@ -16,36 +16,36 @@ secret k: Function; protocol denningSacco(I,R,S) { - role I - { + role I + { var W: Ticket; - var Kir: SessionKey; - var T: TimeStamp; - - send_1(I,S, I,R ); - read_2(S,I, {R, Kir, T, W}k(I,S) ); - send_3(I,R, W); - claim_4(I,Nisynch); - } - - role R - { var Kir: SessionKey; var T: TimeStamp; - read_3(I,R, {Kir,I,T}k(R,S)); - claim_8(R,Nisynch); - } - + send_1(I,S, I,R ); + read_2(S,I, {R, Kir, T, W}k(I,S) ); + send_3(I,R, W); + claim_4(I,Nisynch); + } + + role R + { + var Kir: SessionKey; + var T: TimeStamp; + + read_3(I,R, {Kir,I,T}k(R,S)); + claim_8(R,Nisynch); + } + role S - { + { var W: Ticket; - const Kir: SessionKey; + const Kir: SessionKey; const T: TimeStamp; - read_1(I,S, I,R ); - send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S)); - } + read_1(I,S, I,R ); + send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S)); + } } const Alice,Bob,Simon,Eve: Agent; diff --git a/spdl/SPORE/kaochow-v2.spdl b/spdl/SPORE/kaochow-v2.spdl index 6ce2b78..b8007b3 100644 --- a/spdl/SPORE/kaochow-v2.spdl +++ b/spdl/SPORE/kaochow-v2.spdl @@ -14,45 +14,45 @@ secret k: Function; protocol kaochow2(I,R,S) { - role I - { - const ni: Nonce; - var nr: Nonce; - var kir,kt: Sessionkey; + role I + { + const ni: Nonce; + var nr: Nonce; + var kir,kt: Sessionkey; - send_1 (I,S, I,R,ni); - read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr ); - send_4 (I,R, {nr,kir}kt ); + send_1 (I,S, I,R,ni); + read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr ); + send_4 (I,R, {nr,kir}kt ); - claim_5 (I, Nisynch); - claim_6 (I, Niagree); - claim_7 (I, Secret, kir); - } - - role R - { - var ni: Nonce; - const nr: Nonce; - var kir,kt: Sessionkey; - var T: Ticket; + claim_5 (I, Nisynch); + claim_6 (I, Niagree); + claim_7 (I, Secret, kir); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + var kir,kt: Sessionkey; + var T: Ticket; - read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) ); - send_3 (R,I, R, T, {ni, kir}kt, nr ); - read_4 (I,R, {nr,kir}kt ); + read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) ); + send_3 (R,I, R, T, {ni, kir}kt, nr ); + read_4 (I,R, {nr,kir}kt ); - claim_8 (R, Nisynch); - claim_9 (R, Niagree); - claim_10 (R, Secret, kir); - } + claim_8 (R, Nisynch); + claim_9 (R, Niagree); + claim_10 (R, Secret, kir); + } - role S - { - var ni: Nonce; - const kir, kt: Sessionkey; + role S + { + var ni: Nonce; + const kir, kt: Sessionkey; - read_1 (I,S, I,R,ni); - send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) ); - } + read_1 (I,S, I,R,ni); + send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) ); + } } const Alice,Bob,Simon,Eve: Agent; diff --git a/spdl/SPORE/kaochow-v3.spdl b/spdl/SPORE/kaochow-v3.spdl index 22067f3..11a2a3d 100644 --- a/spdl/SPORE/kaochow-v3.spdl +++ b/spdl/SPORE/kaochow-v3.spdl @@ -15,47 +15,47 @@ secret k: Function; protocol kaochow3(I,R,S) { - role I - { - const ni: Nonce; - var nr: Nonce; - var kir,kt: Sessionkey; - var T2: Ticket; + role I + { + const ni: Nonce; + var nr: Nonce; + var kir,kt: Sessionkey; + var T2: Ticket; - send_1 (I,S, I,R,ni); - read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 ); - send_4 (I,R, {nr,kir}kt, T2 ); + send_1 (I,S, I,R,ni); + read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 ); + send_4 (I,R, {nr,kir}kt, T2 ); - claim_5 (I, Nisynch); - claim_6 (I, Niagree); - claim_7 (I, Secret, kir); - } - - role R - { - var ni: Nonce; - const nr: Nonce; - var kir,kt: Sessionkey; - var T: Ticket; - const tr: Timestamp; + claim_5 (I, Nisynch); + claim_6 (I, Niagree); + claim_7 (I, Secret, kir); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + var kir,kt: Sessionkey; + var T: Ticket; + const tr: Timestamp; - read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) ); - send_3 (R,I, R, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) ); - read_4 (I,R, {nr,kir}kt, {I,R,tr,kir}k(R,S) ); + read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) ); + send_3 (R,I, R, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) ); + read_4 (I,R, {nr,kir}kt, {I,R,tr,kir}k(R,S) ); - claim_8 (R, Nisynch); - claim_9 (R, Niagree); - claim_10 (R, Secret, kir); - } + claim_8 (R, Nisynch); + claim_9 (R, Niagree); + claim_10 (R, Secret, kir); + } - role S - { - var ni: Nonce; - const kir, kt: Sessionkey; + role S + { + var ni: Nonce; + const kir, kt: Sessionkey; - read_1 (I,S, I,R,ni); - send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) ); - } + read_1 (I,S, I,R,ni); + send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) ); + } } const Alice,Bob,Simon,Eve: Agent; diff --git a/spdl/SPORE/kaochow.spdl b/spdl/SPORE/kaochow.spdl index 842b127..c9eca39 100644 --- a/spdl/SPORE/kaochow.spdl +++ b/spdl/SPORE/kaochow.spdl @@ -14,45 +14,45 @@ secret k: Function; protocol kaochow(I,R,S) { - role I - { - const ni: Nonce; - var nr: Nonce; - var kir: Sessionkey; + role I + { + const ni: Nonce; + var nr: Nonce; + var kir: Sessionkey; - send_1 (I,S, I,R,ni); - read_3 (R,I, {I,R,ni,kir}k(I,S), {ni}kir, nr ); - send_4 (I,R, {nr}kir ); + send_1 (I,S, I,R,ni); + read_3 (R,I, {I,R,ni,kir}k(I,S), {ni}kir, nr ); + send_4 (I,R, {nr}kir ); - claim_5 (I, Nisynch); - claim_6 (I, Niagree); - claim_7 (I, Secret, kir); - } - - role R - { - var ni: Nonce; - const nr: Nonce; - var kir: Sessionkey; - var T; + claim_5 (I, Nisynch); + claim_6 (I, Niagree); + claim_7 (I, Secret, kir); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + var kir: Sessionkey; + var T; - read_2 (S,R, T, { I,R,ni,kir }k(R,S) ); - send_3 (R,I, T, {ni}kir, nr ); - read_4 (I,R, {nr}kir ); + read_2 (S,R, T, { I,R,ni,kir }k(R,S) ); + send_3 (R,I, T, {ni}kir, nr ); + read_4 (I,R, {nr}kir ); - claim_8 (R, Nisynch); - claim_9 (R, Niagree); - claim_10 (R, Secret, kir); - } + claim_8 (R, Nisynch); + claim_9 (R, Niagree); + claim_10 (R, Secret, kir); + } - role S - { - var ni: Nonce; - const kir: Sessionkey; + role S + { + var ni: Nonce; + const kir: Sessionkey; - read_1 (I,S, I,R,ni); - send_2 (S,R, {I,R,ni,kir}k(I,S), { I,R,ni,kir }k(R,S) ); - } + read_1 (I,S, I,R,ni); + send_2 (S,R, {I,R,ni,kir}k(I,S), { I,R,ni,kir }k(R,S) ); + } } const Alice,Bob,Simon,Eve: Agent; diff --git a/spdl/SPORE/ksl-lowe.spdl b/spdl/SPORE/ksl-lowe.spdl index f952381..25e8da3 100644 --- a/spdl/SPORE/ksl-lowe.spdl +++ b/spdl/SPORE/ksl-lowe.spdl @@ -25,58 +25,58 @@ compromised k(e,s); protocol kslLowe(A,B,S) { - role A - { - const Na, Ma: Nonce; - var Nc, Mb: Nonce; - var T: Ticket; - var Kab: SessionKey; - - send_1(A,B, Na, A); - read_4(B,A, { Na,B,Kab }k(A,S), T, Nc, {B,Na}Kab ); - send_5(A,B, { Nc }Kab ); - - send_6(A,B, Ma,T ); - read_7(B,A, Mb,{Ma, B}Kab ); - send_8(A,B, {A,Mb}Kab ); + role A + { + const Na, Ma: Nonce; + var Nc, Mb: Nonce; + var T: Ticket; + var Kab: SessionKey; + + send_1(A,B, Na, A); + read_4(B,A, { Na,B,Kab }k(A,S), T, Nc, {B,Na}Kab ); + send_5(A,B, { Nc }Kab ); + + send_6(A,B, Ma,T ); + read_7(B,A, Mb,{Ma, B}Kab ); + send_8(A,B, {A,Mb}Kab ); - claim_A1(A,Secret, Kab); - claim_A2(A,Niagree); - claim_A3(A,Nisynch); - } + claim_A1(A,Secret, Kab); + claim_A2(A,Niagree); + claim_A3(A,Nisynch); + } - role B - { - var Na,Ma: Nonce; - const Nb,Nc,Mb: Nonce; - var Kab: SessionKey; - const Kbb: TicketKey; - const Tb: GeneralizedTimestamp; - var T: Ticket; - - read_1(A,B, Na, A); - send_2(B,S, Na, A, Nb, B ); - read_3(S,B, { A, Nb, Kab }k(B,S), T ); - send_4(B,A, T, { Tb, A, Kab }Kbb, Nc, {B, Na}Kab ); - read_5(A,B, { Nc }Kab ); - - read_6(A,B, Ma,{ Tb, A, Kab }Kbb ); - send_7(B,A, Mb,{Ma,B}Kab ); - read_8(A,B, {A,Mb}Kab ); + role B + { + var Na,Ma: Nonce; + const Nb,Nc,Mb: Nonce; + var Kab: SessionKey; + const Kbb: TicketKey; + const Tb: GeneralizedTimestamp; + var T: Ticket; + + read_1(A,B, Na, A); + send_2(B,S, Na, A, Nb, B ); + read_3(S,B, { A, Nb, Kab }k(B,S), T ); + send_4(B,A, T, { Tb, A, Kab }Kbb, Nc, {B, Na}Kab ); + read_5(A,B, { Nc }Kab ); + + read_6(A,B, Ma,{ Tb, A, Kab }Kbb ); + send_7(B,A, Mb,{Ma,B}Kab ); + read_8(A,B, {A,Mb}Kab ); - claim_B1(B,Secret, Kab); - claim_B2(B,Niagree); - claim_B3(B,Nisynch); - } + claim_B1(B,Secret, Kab); + claim_B2(B,Niagree); + claim_B3(B,Nisynch); + } - role S - { - var Na, Nb: Nonce; - const Kab: SessionKey; + role S + { + var Na, Nb: Nonce; + const Kab: SessionKey; - read_2(B,S, Na, A, Nb, B ); - send_3(S,B, { A, Nb, Kab }k(B,S), { Na,B,Kab }k(A,S) ); - } + read_2(B,S, Na, A, Nb, B ); + send_3(S,B, { A, Nb, Kab }k(B,S), { Na,B,Kab }k(A,S) ); + } } run kslLowe.A(a,b,s); diff --git a/spdl/SPORE/ksl.spdl b/spdl/SPORE/ksl.spdl index 8c8f821..bbb2c31 100644 --- a/spdl/SPORE/ksl.spdl +++ b/spdl/SPORE/ksl.spdl @@ -22,58 +22,58 @@ compromised k(e,s); protocol ksl(A,B,S) { - role A - { - const Na, Ma: Nonce; - var Nc, Mb: Nonce; - var T: Ticket; - var Kab: SessionKey; - - send_1(A,B, Na, A); - read_4(B,A, { Na,B,Kab }k(A,S), T, Nc, {Na}Kab ); - send_5(A,B, { Nc }Kab ); - - send_6(A,B, Ma,T ); - read_7(B,A, Mb,{Ma}Kab ); - send_8(A,B, {Mb}Kab ); + role A + { + const Na, Ma: Nonce; + var Nc, Mb: Nonce; + var T: Ticket; + var Kab: SessionKey; + + send_1(A,B, Na, A); + read_4(B,A, { Na,B,Kab }k(A,S), T, Nc, {Na}Kab ); + send_5(A,B, { Nc }Kab ); + + send_6(A,B, Ma,T ); + read_7(B,A, Mb,{Ma}Kab ); + send_8(A,B, {Mb}Kab ); - claim_A1(A,Secret, Kab); - claim_A2(A,Niagree); - claim_A3(A,Nisynch); - } + claim_A1(A,Secret, Kab); + claim_A2(A,Niagree); + claim_A3(A,Nisynch); + } - role B - { - var Na,Ma: Nonce; - const Nb,Nc,Mb: Nonce; - var Kab: SessionKey; - const Kbb: TicketKey; - const Tb: GeneralizedTimestamp; - var T: Ticket; - - read_1(A,B, Na, A); - send_2(B,S, Na, A, Nb, B ); - read_3(S,B, { Nb, A, Kab }k(B,S), T ); - send_4(B,A, T, { Tb, A, Kab }Kbb, Nc, {Na}Kab ); - read_5(A,B, { Nc }Kab ); - - read_6(A,B, Ma,{ Tb, A, Kab }Kbb ); - send_7(B,A, Mb,{Ma}Kab ); - read_8(A,B, {Mb}Kab ); + role B + { + var Na,Ma: Nonce; + const Nb,Nc,Mb: Nonce; + var Kab: SessionKey; + const Kbb: TicketKey; + const Tb: GeneralizedTimestamp; + var T: Ticket; + + read_1(A,B, Na, A); + send_2(B,S, Na, A, Nb, B ); + read_3(S,B, { Nb, A, Kab }k(B,S), T ); + send_4(B,A, T, { Tb, A, Kab }Kbb, Nc, {Na}Kab ); + read_5(A,B, { Nc }Kab ); + + read_6(A,B, Ma,{ Tb, A, Kab }Kbb ); + send_7(B,A, Mb,{Ma}Kab ); + read_8(A,B, {Mb}Kab ); - claim_B1(B,Secret, Kab); - claim_B2(B,Niagree); - claim_B3(B,Nisynch); - } + claim_B1(B,Secret, Kab); + claim_B2(B,Niagree); + claim_B3(B,Nisynch); + } - role S - { - var Na, Nb: Nonce; - const Kab: SessionKey; + role S + { + var Na, Nb: Nonce; + const Kab: SessionKey; - read_2(B,S, Na, A, Nb, B ); - send_3(S,B, { Nb, A, Kab }k(B,S), { Na,B,Kab }k(A,S) ); - } + read_2(B,S, Na, A, Nb, B ); + send_3(S,B, { Nb, A, Kab }k(B,S), { Na,B,Kab }k(A,S) ); + } } run ksl.A(a,b,s); diff --git a/spdl/SPORE/needham-schroeder-lowe.spdl b/spdl/SPORE/needham-schroeder-lowe.spdl index 6b6393a..399ce52 100644 --- a/spdl/SPORE/needham-schroeder-lowe.spdl +++ b/spdl/SPORE/needham-schroeder-lowe.spdl @@ -16,22 +16,22 @@ inversekeys(pk,sk); protocol needhamschroederpkLowe(I,R,S) { - role I - { + role I + { const Ni: Nonce; var Nr: Nonce; - send_1(I,S, (I,R)); + send_1(I,S, (I,R)); read_2(S,I, {pk(R), R}sk(S)); send_3(I,R,{Ni,I}pk(R)); read_6(R,I, {Ni,Nr,R}pk(I)); send_7(I,R, {Nr}pk(R)); claim_I1(I,Secret,Ni); claim_I2(I,Secret,Nr); - } - - role R - { + } + + role R + { const Nr: Nonce; var Ni: Nonce; @@ -42,7 +42,7 @@ protocol needhamschroederpkLowe(I,R,S) read_7(I,R,{Nr}pk(R)); claim_R1(R,Secret,Nr); claim_R2(R,Secret,Ni); - } + } role S { diff --git a/spdl/SPORE/needham-schroeder-sk-amend.spdl b/spdl/SPORE/needham-schroeder-sk-amend.spdl index 31c3dcf..656a140 100644 --- a/spdl/SPORE/needham-schroeder-sk-amend.spdl +++ b/spdl/SPORE/needham-schroeder-sk-amend.spdl @@ -23,8 +23,8 @@ usertype Ticket; protocol needhamschroederskamend(I,R,S) { - role I - { + role I + { const Ni: Nonce; var Nr: Nonce; var Kir: SessionKey; @@ -40,10 +40,10 @@ protocol needhamschroederskamend(I,R,S) claim_I2(I,Secret,Kir); claim_I3(I,Nisynch); - } - - role R - { + } + + role R + { const Nr: Nonce; var Kir: SessionKey; @@ -54,7 +54,7 @@ protocol needhamschroederskamend(I,R,S) read_7(I,R,{{Nr}dec}Kir); claim_R1(R,Secret,Nr); claim_R3(R,Nisynch); - } + } role S { diff --git a/spdl/SPORE/needham-schroeder-sk.spdl b/spdl/SPORE/needham-schroeder-sk.spdl index 26508ba..851d440 100644 --- a/spdl/SPORE/needham-schroeder-sk.spdl +++ b/spdl/SPORE/needham-schroeder-sk.spdl @@ -19,24 +19,24 @@ usertype Ticket; protocol needhamschroedersk(I,R,S) { - role I - { + role I + { const Ni: Nonce; var Nr: Nonce; var Kir: SessionKey; var T: Ticket; - send_1(I,S,(I,R,Ni)); + send_1(I,S,(I,R,Ni)); read_2(S,I, {Ni,R,Kir,T}k(I,S)); send_3(I,R,T); read_4(R,I,{Nr}Kir); send_5(I,R,{{Nr}dec}Kir); claim_I2(I,Secret,Kir); claim_I3(I,Nisynch); - } - - role R - { + } + + role R + { const Nr: Nonce; var Kir: SessionKey; @@ -45,7 +45,7 @@ protocol needhamschroedersk(I,R,S) read_5(I,R,{{Nr}dec}Kir); claim_R1(R,Secret,Kir); claim_R3(R,Nisynch); - } + } role S { diff --git a/spdl/SPORE/needham-schroeder.spdl b/spdl/SPORE/needham-schroeder.spdl index b73385d..37bbd6d 100644 --- a/spdl/SPORE/needham-schroeder.spdl +++ b/spdl/SPORE/needham-schroeder.spdl @@ -16,22 +16,22 @@ inversekeys(pk,sk); protocol needhamschroederpk(I,R,S) { - role I - { + role I + { const Ni: Nonce; var Nr: Nonce; - send_1(I,S,(I,R)); + send_1(I,S,(I,R)); read_2(S,I, {pk(R), R}sk(S)); send_3(I,R,{Ni,I}pk(R)); read_6(R,I, {Ni, Nr}pk(I)); send_7(I,R, {Nr}pk(R)); claim_I1(I,Secret,Ni); claim_I2(I,Secret,Nr); - } - - role R - { + } + + role R + { const Nr: Nonce; var Ni: Nonce; @@ -42,7 +42,7 @@ protocol needhamschroederpk(I,R,S) read_7(I,R,{Nr}pk(R)); claim_R1(R,Secret,Nr); claim_R2(R,Secret,Ni); - } + } role S { diff --git a/spdl/SPORE/neumannstub-hwang.spdl b/spdl/SPORE/neumannstub-hwang.spdl index d8a7230..ed76187 100644 --- a/spdl/SPORE/neumannstub-hwang.spdl +++ b/spdl/SPORE/neumannstub-hwang.spdl @@ -25,55 +25,55 @@ compromised k(e,s); protocol neustubHwang(I,R,S) { - role I - { - const Ni,Mi: Nonce; - var Nr,Mr: Nonce; - var T: Ticket; + role I + { + const Ni,Mi: Nonce; + var Nr,Mr: Nonce; + var T: Ticket; var Tb: TimeStamp; - var Kir: SessionKey; - - send_1(I,R, I, Ni); - read_3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr); + var Kir: SessionKey; + + send_1(I,R, I, Ni); + read_3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr); send_4(I,R,T,{Nr}Kir); send_5(I,R,Mi,T); - read_6(R,I,Mr,{Mr}Kir); - send_7(I,R,{Mr}Kir); - - claim_I1(I,Secret, Kir); - claim_I2(I,Niagree); - claim_I3(I,Nisynch); - } + read_6(R,I,Mr,{Mr}Kir); + send_7(I,R,{Mr}Kir); + + claim_I1(I,Secret, Kir); + claim_I2(I,Niagree); + claim_I3(I,Nisynch); + } - role R - { - var Ni,Mi: Nonce; - const Nr,Mr: Nonce; - var Kir: SessionKey; - const Tb: TimeStamp; - var T: Ticket; - + role R + { + var Ni,Mi: Nonce; + const Nr,Mr: Nonce; + var Kir: SessionKey; + const Tb: TimeStamp; + var T: Ticket; + read_1(I,R, I, Ni); send_2(R,S, R, {I, Ni, Tb, Nr}k(R,S)); read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir); read_5(I,R,Mi,T); - send_6(R,I,Mr,{Mr}Kir); - read_7(I,R,{Mr}Kir); - - claim_R1(R,Secret, Kir); - claim_R2(R,Niagree); - claim_R3(R,Nisynch); - } + send_6(R,I,Mr,{Mr}Kir); + read_7(I,R,{Mr}Kir); + + claim_R1(R,Secret, Kir); + claim_R2(R,Niagree); + claim_R3(R,Nisynch); + } - role S - { - var Ni, Nr: Nonce; - const Kir: SessionKey; + role S + { + var Ni, Nr: Nonce; + const Kir: SessionKey; var Tb: TimeStamp; - read_2(R,S, R, {I,Ni,Tb,Nr}k(R,S)); - send_3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr ); - } + read_2(R,S, R, {I,Ni,Tb,Nr}k(R,S)); + send_3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr ); + } } run neustubHwang.A(a,b,s); diff --git a/spdl/SPORE/neumannstub.spdl b/spdl/SPORE/neumannstub.spdl index 07e97de..b551818 100644 --- a/spdl/SPORE/neumannstub.spdl +++ b/spdl/SPORE/neumannstub.spdl @@ -22,55 +22,55 @@ compromised k(e,s); protocol neustub(I,R,S) { - role I - { - const Ni,Mi: Nonce; - var Nr,Mr: Nonce; - var T: Ticket; + role I + { + const Ni,Mi: Nonce; + var Nr,Mr: Nonce; + var T: Ticket; var Tb: TimeStamp; - var Kir: SessionKey; - - send_1(I,R, I, Ni); - read_3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr); + var Kir: SessionKey; + + send_1(I,R, I, Ni); + read_3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr); send_4(I,R,T,{Nr}Kir); send_5(I,R,Mi,T); - read_6(R,I,Mr,{Mi}Kir); - send_7(I,R,{Mr}Kir); - - claim_I1(I,Secret, Kir); - claim_I2(I,Niagree); - claim_I3(I,Nisynch); - } + read_6(R,I,Mr,{Mi}Kir); + send_7(I,R,{Mr}Kir); + + claim_I1(I,Secret, Kir); + claim_I2(I,Niagree); + claim_I3(I,Nisynch); + } - role R - { - var Ni,Mi: Nonce; - const Nr,Mr: Nonce; - var Kir: SessionKey; - const Tb: TimeStamp; - var T: Ticket; - + role R + { + var Ni,Mi: Nonce; + const Nr,Mr: Nonce; + var Kir: SessionKey; + const Tb: TimeStamp; + var T: Ticket; + read_1(I,R, I, Ni); send_2(R,S, R, {I, Ni, Tb}k(R,S),Nr); read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir); read_5(I,R,Mi,T); - send_6(R,I,Mr,{Mi}Kir); - read_7(I,R,{Mr}Kir); - - claim_R1(R,Secret, Kir); - claim_R2(R,Niagree); - claim_R3(R,Nisynch); - } + send_6(R,I,Mr,{Mi}Kir); + read_7(I,R,{Mr}Kir); + + claim_R1(R,Secret, Kir); + claim_R2(R,Niagree); + claim_R3(R,Nisynch); + } - role S - { - var Ni, Nr: Nonce; - const Kir: SessionKey; + role S + { + var Ni, Nr: Nonce; + const Kir: SessionKey; var Tb: TimeStamp; - read_2(R,S, R, {I,Ni,Tb}k(R,S), Nr); - send_3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr ); - } + read_2(R,S, R, {I,Ni,Tb}k(R,S), Nr); + send_3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr ); + } } run neustub.A(a,b,s); diff --git a/spdl/SPORE/otwayrees.spdl b/spdl/SPORE/otwayrees.spdl index 274edc3..f6fd1d8 100644 --- a/spdl/SPORE/otwayrees.spdl +++ b/spdl/SPORE/otwayrees.spdl @@ -16,44 +16,44 @@ usertype String,SessionKey,Ticket; protocol otwayrees(I,R,S) { - role I - { - const Ni : Nonce; - const M : String; - var Kir : SessionKey; + role I + { + const Ni : Nonce; + const M : String; + var Kir : SessionKey; - send_1(I,R, M,I,R,{Ni,M,I,R}k(I,S) ); - read_4(R,I, M,{Ni,Kir}k(I,S) ); + send_1(I,R, M,I,R,{Ni,M,I,R}k(I,S) ); + read_4(R,I, M,{Ni,Kir}k(I,S) ); - claim_I1(I, Secret,Kir); + claim_I1(I, Secret,Kir); #claim_I2(I, Nisynch); - } + } - role R - { - var M : String; - const Nr : Nonce; - var Kir : SessionKey; - var T1,T2: Ticket; + role R + { + var M : String; + const Nr : Nonce; + var Kir : SessionKey; + var T1,T2: Ticket; - read_1(I,R, M,I,R, T1 ); - send_2(R,S, M,I,R, T1, { Nr,M,I,R }k(R,S) ); - read_3(S,R, M, T2, { Nr,Kir }k(R,S) ); - send_4(R,I, M, T2 ); + read_1(I,R, M,I,R, T1 ); + send_2(R,S, M,I,R, T1, { Nr,M,I,R }k(R,S) ); + read_3(S,R, M, T2, { Nr,Kir }k(R,S) ); + send_4(R,I, M, T2 ); - claim_R1(R, Secret,Kir); + claim_R1(R, Secret,Kir); #claim_R2(R, Nisynch); - } + } - role S - { - var Ni,Nr : Nonce; - var M : String; - const Kir : SessionKey; - - read_2(R,S, M,I,R, { Ni,M,I,R}k(I,S), { Nr,M,I,R }k(R,S) ); - send_3(S,R, M, { Ni,Kir }k(I,S) , { Nr,Kir }k(R,S) ); - } + role S + { + var Ni,Nr : Nonce; + var M : String; + const Kir : SessionKey; + + read_2(R,S, M,I,R, { Ni,M,I,R}k(I,S), { Nr,M,I,R }k(R,S) ); + send_3(S,R, M, { Ni,Kir }k(I,S) , { Nr,Kir }k(R,S) ); + } } const Alice, Bob, Eve, Simon: Agent; diff --git a/spdl/SPORE/smartright.spdl b/spdl/SPORE/smartright.spdl index 788e073..d2d27cb 100644 --- a/spdl/SPORE/smartright.spdl +++ b/spdl/SPORE/smartright.spdl @@ -25,9 +25,9 @@ const Vor: XorKey; protocol smartright(I,R) { - role I - { - const VoKey: SessionKey; + role I + { + const VoKey: SessionKey; const VoR: XorKey; const CW; var VoRi: Nonce; @@ -35,10 +35,10 @@ protocol smartright(I,R) send_1(I,R, {VoKey,{CW}VoR}k(I,R)); read_2(R,I, VoRi); send_3(I,R, VoR, {{VoRi}hash}VoKey); - } - - role R - { + } + + role R + { var T: Ticket; var VoR: XorKey; var VoKey: SessionKey; @@ -48,8 +48,8 @@ protocol smartright(I,R) send_2(R,I, VoRi); read_3(I,R, VoR,{{VoRi}hash}VoKey); - claim_R1(R,Nisynch); - } + claim_R1(R,Nisynch); + } } const Alice,Bob,Eve: Agent; diff --git a/spdl/SPORE/splice-as-cj.spdl b/spdl/SPORE/splice-as-cj.spdl index a7be252..8ce1d39 100644 --- a/spdl/SPORE/splice-as-cj.spdl +++ b/spdl/SPORE/splice-as-cj.spdl @@ -21,50 +21,50 @@ inversekeys (inc,dec); protocol spliceASCJ(I,R,S) { role I - { - const N1,N2: Nonce; - const T: TimeStamp; - const L: LifeTime; + { + const N1,N2: Nonce; + const T: TimeStamp; + const L: LifeTime; - send_1(I,S, I, R, N1 ); - read_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); - send_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) ); - read_6(R,I, R, I, {{N2}inc}pk(I) ); + send_1(I,S, I, R, N1 ); + read_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); + send_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) ); + read_6(R,I, R, I, {{N2}inc}pk(I) ); - claim_7(I, Secret, N2); - claim_9(I, Niagree); - claim_10(I, Nisynch); - } + claim_7(I, Secret, N2); + claim_9(I, Niagree); + claim_10(I, Nisynch); + } - role S - { - var N1,N3: Nonce; + role S + { + var N1,N3: Nonce; - read_1(I,S, I, R, N1 ); - send_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); - read_4(R,S, R, I, N3 ); - send_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); - } + read_1(I,S, I, R, N1 ); + send_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); + read_4(R,S, R, I, N3 ); + send_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); + } - role R - { - const N3: Nonce; - var N2: Nonce; - var T: TimeStamp; - var L: LifeTime; + role R + { + const N3: Nonce; + var N2: Nonce; + var T: TimeStamp; + var L: LifeTime; - var ni: Nonce; - const nr: Nonce; + var ni: Nonce; + const nr: Nonce; - read_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) ); - send_4(R,S, R, I, N3 ); - read_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); - send_6(R,I, R, I, {{N2}inc}pk(I) ); + read_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) ); + send_4(R,S, R, I, N3 ); + read_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); + send_6(R,I, R, I, {{N2}inc}pk(I) ); - claim_8(R, Secret, N2); - claim_11(R, Niagree); - claim_12(R, Nisynch); - } + claim_8(R, Secret, N2); + claim_11(R, Niagree); + claim_12(R, Nisynch); + } } const Alice,Bob,Simon,Eve: Agent; diff --git a/spdl/SPORE/splice-as-hc.spdl b/spdl/SPORE/splice-as-hc.spdl index 931132b..8ddf292 100644 --- a/spdl/SPORE/splice-as-hc.spdl +++ b/spdl/SPORE/splice-as-hc.spdl @@ -16,50 +16,50 @@ inversekeys (inc,dec); protocol spliceASHC(I,R,S) { role I - { - const N1,N2: Nonce; - const T: TimeStamp; - const L: LifeTime; + { + const N1,N2: Nonce; + const T: TimeStamp; + const L: LifeTime; - send_1(I,S, I, R, N1 ); - read_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); - send_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); - read_6(R,I, R, I, {R, {N2}inc}pk(I) ); + send_1(I,S, I, R, N1 ); + read_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); + send_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); + read_6(R,I, R, I, {R, {N2}inc}pk(I) ); - claim_7(I, Secret, N2); - claim_9(I, Niagree); - claim_10(I, Nisynch); - } + claim_7(I, Secret, N2); + claim_9(I, Niagree); + claim_10(I, Nisynch); + } - role S - { - var N1,N3: Nonce; + role S + { + var N1,N3: Nonce; - read_1(I,S, I, R, N1 ); - send_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); - read_4(R,S, R, I, N3 ); - send_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) ); - } + read_1(I,S, I, R, N1 ); + send_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); + read_4(R,S, R, I, N3 ); + send_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) ); + } - role R - { - const N3: Nonce; - var N2: Nonce; - var T: TimeStamp; - var L: LifeTime; + role R + { + const N3: Nonce; + var N2: Nonce; + var T: TimeStamp; + var L: LifeTime; - var ni: Nonce; - const nr: Nonce; + var ni: Nonce; + const nr: Nonce; - read_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); - send_4(R,S, R, I, N3 ); - read_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) ); - send_6(R,I, R, I, {R, {N2}inc}pk(I) ); + read_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); + send_4(R,S, R, I, N3 ); + read_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) ); + send_6(R,I, R, I, {R, {N2}inc}pk(I) ); - claim_8(R, Secret, N2); - claim_11(R, Niagree); - claim_12(R, Nisynch); - } + claim_8(R, Secret, N2); + claim_11(R, Niagree); + claim_12(R, Nisynch); + } } const Alice,Bob,Simon,Eve: Agent; diff --git a/spdl/SPORE/splice-as.spdl b/spdl/SPORE/splice-as.spdl index 6952245..72f223c 100644 --- a/spdl/SPORE/splice-as.spdl +++ b/spdl/SPORE/splice-as.spdl @@ -21,50 +21,50 @@ inversekeys (inc,dec); protocol spliceAS(I,R,S) { role I - { - const N1,N2: Nonce; - const T: TimeStamp; - const L: LifeTime; + { + const N1,N2: Nonce; + const T: TimeStamp; + const L: LifeTime; - send_1(I,S, I, R, N1 ); - read_2(S,I, S, {S, I, N1, pk(R)}sk(S) ); - send_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); - read_6(R,I, R, I, {R, {N2}inc}pk(I) ); + send_1(I,S, I, R, N1 ); + read_2(S,I, S, {S, I, N1, pk(R)}sk(S) ); + send_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); + read_6(R,I, R, I, {R, {N2}inc}pk(I) ); - claim_7(I, Secret, N2); - claim_9(I, Niagree); - claim_10(I, Nisynch); - } + claim_7(I, Secret, N2); + claim_9(I, Niagree); + claim_10(I, Nisynch); + } - role S - { - var N1,N3: Nonce; + role S + { + var N1,N3: Nonce; - read_1(I,S, I, R, N1 ); - send_2(S,I, S, {S, I, N1, pk(R)}sk(S) ); - read_4(R,S, R, I, N3 ); - send_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); - } + read_1(I,S, I, R, N1 ); + send_2(S,I, S, {S, I, N1, pk(R)}sk(S) ); + read_4(R,S, R, I, N3 ); + send_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); + } - role R - { - const N3: Nonce; - var N2: Nonce; - var T: TimeStamp; - var L: LifeTime; + role R + { + const N3: Nonce; + var N2: Nonce; + var T: TimeStamp; + var L: LifeTime; - var ni: Nonce; - const nr: Nonce; + var ni: Nonce; + const nr: Nonce; - read_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); - send_4(R,S, R, I, N3 ); - read_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); - send_6(R,I, R, I, {R, {N2}inc}pk(I) ); + read_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); + send_4(R,S, R, I, N3 ); + read_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); + send_6(R,I, R, I, {R, {N2}inc}pk(I) ); - claim_8(R, Secret, N2); - claim_11(R, Niagree); - claim_12(R, Nisynch); - } + claim_8(R, Secret, N2); + claim_11(R, Niagree); + claim_12(R, Nisynch); + } } const Alice,Bob,Simon,Eve: Agent; diff --git a/spdl/SPORE/tmn.spdl b/spdl/SPORE/tmn.spdl index 173abca..f3934a0 100644 --- a/spdl/SPORE/tmn.spdl +++ b/spdl/SPORE/tmn.spdl @@ -12,37 +12,37 @@ inversekeys(pk,sk); protocol tmn(I,R,S) { - role I - { - const Ki: Key; - var Kr: Key; + role I + { + const Ki: Key; + var Kr: Key; - send_1(I,S, R,{Ki}pk(S) ); - read_4(S,I, R,{Kr}Ki ); + send_1(I,S, R,{Ki}pk(S) ); + read_4(S,I, R,{Kr}Ki ); - claim_I1(I,Secret,Ki); - claim_I2(I,Secret,Kr); - } - - role R - { - const Kr: Key; + claim_I1(I,Secret,Ki); + claim_I2(I,Secret,Kr); + } + + role R + { + const Kr: Key; - read_2(S,R, I ); - send_3(R,S, I, { Kr }pk(S) ); + read_2(S,R, I ); + send_3(R,S, I, { Kr }pk(S) ); - claim_R1(R,Secret,Kr); - } + claim_R1(R,Secret,Kr); + } - role S - { - var Ki,Kr: Key; + role S + { + var Ki,Kr: Key; - read_1(I,S, R,{Ki}pk(S) ); - send_2(S,R, I ); - read_3(R,S, I, { Kr }pk(S) ); - send_4(S,I, R,{Kr}Ki ); - } + read_1(I,S, R,{Ki}pk(S) ); + send_2(S,R, I ); + read_3(R,S, I, { Kr }pk(S) ); + send_4(S,I, R,{Kr}Ki ); + } } const Alice,Bob,Eve,Simon: Agent; diff --git a/spdl/SPORE/wmf-lowe.spdl b/spdl/SPORE/wmf-lowe.spdl index a74118d..66c992d 100644 --- a/spdl/SPORE/wmf-lowe.spdl +++ b/spdl/SPORE/wmf-lowe.spdl @@ -18,44 +18,44 @@ secret k: Function; protocol wmfLowe(I,R,S) { - role I - { - const Kir: Key; + role I + { + const Kir: Key; const Ti: TimeStamp; - var Kr: Key; + var Kr: Key; var Nr: Nonce; - send_1(I,S, I, {Ti, R, Kir}k(I,S)); + send_1(I,S, I, {Ti, R, Kir}k(I,S)); read_3(R,I,{Nr}Kir); send_4(I,R,{{Nr}succ}Kir); - claim_I1(I,Secret,Kir); + claim_I1(I,Secret,Kir); claim_I2(I,Nisynch); - } - - role R - { + } + + role R + { var Ts: TimeStamp; var Kir: Key; const Nr: Nonce; - read_2(S,R, {Ts, I, Kir}k(R,S) ); + read_2(S,R, {Ts, I, Kir}k(R,S) ); send_3(R,I, {Nr}Kir); read_4(I,R, {{Nr}succ}Kir); - claim_R1(R,Secret,Kir); + claim_R1(R,Secret,Kir); claim_R2(R,Nisynch); - } + } - role S - { - var Kir: Key; + role S + { + var Kir: Key; const Ts: TimeStamp; var Ti: TimeStamp; - read_1(I,S, I,{Ti, R, Kir}k(I,S) ); + read_1(I,S, I,{Ti, R, Kir}k(I,S) ); send_2(S,R, {Ts, I, Kir}k(R,S)); - } + } } const Alice,Bob,Eve,Simon: Agent; diff --git a/spdl/SPORE/wmf.spdl b/spdl/SPORE/wmf.spdl index cd953ff..0a01f83 100644 --- a/spdl/SPORE/wmf.spdl +++ b/spdl/SPORE/wmf.spdl @@ -11,37 +11,37 @@ secret k: Function; protocol wmf(I,R,S) { - role I - { - const Kir: Key; + role I + { + const Kir: Key; const Ti: TimeStamp; - var Kr: Key; + var Kr: Key; - send_1(I,S, I, {Ti, R, Kir}k(I,S)); + send_1(I,S, I, {Ti, R, Kir}k(I,S)); - claim_I1(I,Secret,Kir); - } - - role R - { + claim_I1(I,Secret,Kir); + } + + role R + { var Ts: TimeStamp; var Kir: Key; - read_2(S,R, {Ts, I, Kir}k(R,S) ); + read_2(S,R, {Ts, I, Kir}k(R,S) ); - claim_R1(R,Secret,Kir); + claim_R1(R,Secret,Kir); claim_R2(R,Nisynch); - } + } - role S - { - var Kir: Key; + role S + { + var Kir: Key; const Ts: TimeStamp; var Ti: TimeStamp; - read_1(I,S, I,{Ti, R, Kir}k(I,S) ); + read_1(I,S, I,{Ti, R, Kir}k(I,S) ); send_2(S,R, {Ts, I, Kir}k(R,S)); - } + } } const Alice,Bob,Eve,Simon: Agent; diff --git a/spdl/SPORE/woo-lam-pi-1.spdl b/spdl/SPORE/woo-lam-pi-1.spdl index 21dee6d..945043f 100644 --- a/spdl/SPORE/woo-lam-pi-1.spdl +++ b/spdl/SPORE/woo-lam-pi-1.spdl @@ -14,18 +14,18 @@ secret k: Function; protocol woolamPi1(I,R,S) { - role I - { - var Nr: Nonce; + role I + { + var Nr: Nonce; - send_1(I,R, I); + send_1(I,R, I); read_2(R,I, Nr); send_3(I,R, {I,R,Nr}k(I,S)); - } - - role R - { + } + + role R + { const Nr: Nonce; var T: Ticket; @@ -36,15 +36,15 @@ protocol woolamPi1(I,R,S) read_5(S,R, {I,R, Nr}k(R,S)); claim_R1(R,Nisynch); - } + } - role S - { + role S + { var Nr: Nonce; read_4(R,S, {I,R, {I,R,Nr}k(I,S)}k(R,S)); send_5(S,R, {I,R,Nr}k(R,S)); - } + } } const Alice,Bob,Eve,Simon: Agent; diff --git a/spdl/SPORE/woo-lam-pi-2.spdl b/spdl/SPORE/woo-lam-pi-2.spdl index f885ec9..11d5faf 100644 --- a/spdl/SPORE/woo-lam-pi-2.spdl +++ b/spdl/SPORE/woo-lam-pi-2.spdl @@ -14,18 +14,18 @@ secret k: Function; protocol woolamPi2(I,R,S) { - role I - { - var Nr: Nonce; + role I + { + var Nr: Nonce; - send_1(I,R, I); + send_1(I,R, I); read_2(R,I, Nr); send_3(I,R, {I,Nr}k(I,S)); - } - - role R - { + } + + role R + { const Nr: Nonce; var T: Ticket; @@ -36,15 +36,15 @@ protocol woolamPi2(I,R,S) read_5(S,R, {I, Nr}k(R,S)); claim_R1(R,Nisynch); - } + } - role S - { + role S + { var Nr: Nonce; read_4(R,S, {I, {I,Nr}k(I,S)}k(R,S)); send_5(S,R, {I,Nr}k(R,S)); - } + } } const Alice,Bob,Eve,Simon: Agent; diff --git a/spdl/SPORE/woo-lam-pi-3.spdl b/spdl/SPORE/woo-lam-pi-3.spdl index 932afbf..06e7237 100644 --- a/spdl/SPORE/woo-lam-pi-3.spdl +++ b/spdl/SPORE/woo-lam-pi-3.spdl @@ -14,18 +14,18 @@ secret k: Function; protocol woolamPi3(I,R,S) { - role I - { - var Nr: Nonce; + role I + { + var Nr: Nonce; - send_1(I,R, I); + send_1(I,R, I); read_2(R,I, Nr); send_3(I,R, {Nr}k(I,S)); - } - - role R - { + } + + role R + { const Nr: Nonce; var T: Ticket; @@ -36,15 +36,15 @@ protocol woolamPi3(I,R,S) read_5(S,R, {I, Nr}k(R,S)); claim_R1(R,Nisynch); - } + } - role S - { + role S + { var Nr: Nonce; read_4(R,S, {I, {Nr}k(I,S)}k(R,S)); send_5(S,R, {I,Nr}k(R,S)); - } + } } const Alice,Bob,Eve,Simon: Agent; diff --git a/spdl/SPORE/woo-lam-pi-f.spdl b/spdl/SPORE/woo-lam-pi-f.spdl index edbecfb..72680bf 100644 --- a/spdl/SPORE/woo-lam-pi-f.spdl +++ b/spdl/SPORE/woo-lam-pi-f.spdl @@ -14,18 +14,18 @@ secret k: Function; protocol woolamPif(I,R,S) { - role I - { - var Nr: Nonce; + role I + { + var Nr: Nonce; - send_1(I,R, I); + send_1(I,R, I); read_2(R,I, Nr); send_3(I,R, {I,R,Nr}k(I,S)); - } - - role R - { + } + + role R + { const Nr: Nonce; var T: Ticket; @@ -36,15 +36,15 @@ protocol woolamPif(I,R,S) read_5(S,R, {I, R, Nr}k(R,S)); claim_R1(R,Nisynch); - } + } - role S - { + role S + { var Nr: Nonce; read_4(R,S, {I, R, Nr,{I,R,Nr}k(I,S)}k(R,S)); send_5(S,R, {I, R, Nr}k(R,S)); - } + } } const Alice,Bob,Eve,Simon: Agent; diff --git a/spdl/SPORE/woo-lam-pi.spdl b/spdl/SPORE/woo-lam-pi.spdl index 37b7233..fc8385f 100644 --- a/spdl/SPORE/woo-lam-pi.spdl +++ b/spdl/SPORE/woo-lam-pi.spdl @@ -18,18 +18,18 @@ secret k: Function; protocol woolamPi(I,R,S) { - role I - { - var Nr: Nonce; + role I + { + var Nr: Nonce; - send_1(I,R, I); + send_1(I,R, I); read_2(R,I, Nr); send_3(I,R, {Nr}k(I,S)); - } - - role R - { + } + + role R + { const Nr: Nonce; var T: Ticket; @@ -40,15 +40,15 @@ protocol woolamPi(I,R,S) read_5(S,R, {Nr}k(R,S)); claim_R1(R,Nisynch); - } + } - role S - { + role S + { var Nr: Nonce; read_4(R,S, {I,{Nr}k(I,S)}k(R,S)); send_5(S,R, {Nr}k(R,S)); - } + } } const Alice,Bob,Eve,Simon: Agent; diff --git a/spdl/SPORE/woo-lam.spdl b/spdl/SPORE/woo-lam.spdl index b494771..fc1b160 100644 --- a/spdl/SPORE/woo-lam.spdl +++ b/spdl/SPORE/woo-lam.spdl @@ -16,25 +16,25 @@ secret k: Function; protocol woolam(I,R,S) { - role I - { + role I + { const N1: Nonce; var Kir: Key; - var N2: Nonce; + var N2: Nonce; - send_1(I,R, I, N1); + send_1(I,R, I, N1); read_2(R,I, R, N2); send_3(I,R, {I, R, N1, N2}k(I,S)); read_6(R,I, {R, N1, N2, Kir}k(I,S), {N1,N2}Kir); send_7(I,R, {N2}Kir); - claim_I1(I,Secret,Kir); + claim_I1(I,Secret,Kir); claim_I2(I,Nisynch); - } - - role R - { + } + + role R + { const N2: Nonce; var N1: Nonce; var Kir: Key; @@ -48,18 +48,18 @@ protocol woolam(I,R,S) send_6(R,I, T2, {N1,N2}Kir); read_7(I,R, {N2}Kir); - claim_R1(R,Secret,Kir); + claim_R1(R,Secret,Kir); claim_R2(R,Nisynch); - } + } - role S - { - const Kir: Key; + role S + { + const Kir: Key; var N1,N2: Nonce; read_4(R,S, {I, R, N1, N2}k(I,S), {I, R, N1, N2}k(R,S)); send_5(S,R, {R, N1, N2, Kir}k(I,S), {I, N1, N2, Kir}k(R,S)); - } + } } const Alice,Bob,Eve,Simon: Agent; diff --git a/spdl/SPORE/yahalom-ban.spdl b/spdl/SPORE/yahalom-ban.spdl index 17220b0..f4eb64e 100644 --- a/spdl/SPORE/yahalom-ban.spdl +++ b/spdl/SPORE/yahalom-ban.spdl @@ -15,44 +15,44 @@ usertype Ticket, Key; protocol yahalomBAN(I,R,S) { - role I - { - const Ni: Nonce; - var Nr: Nonce; - var T: Ticket; - var Kir: Key; + role I + { + const Ni: Nonce; + var Nr: Nonce; + var T: Ticket; + var Kir: Key; - send_1(I,R, I,Ni); - read_3(S,I, Nr, {R,Kir,Ni}k(I,S), T ); - send_4(I,R, T, {Nr}Kir ); + send_1(I,R, I,Ni); + read_3(S,I, Nr, {R,Kir,Ni}k(I,S), T ); + send_4(I,R, T, {Nr}Kir ); - claim_I1(I, Secret,Kir); - claim_I2(I, Nisynch); - } + claim_I1(I, Secret,Kir); + claim_I2(I, Nisynch); + } - role R - { - const Nr: Nonce; - var Ni: Nonce; - var T: Ticket; - var Kir: Key; + role R + { + const Nr: Nonce; + var Ni: Nonce; + var T: Ticket; + var Kir: Key; - read_1(I,R, I,Ni); - send_2(R,S, R, Nr, {I,Ni}k(R,S) ); - read_4(I,R, {I,Kir,Nr}k(R,S) , {Nr}Kir ); + read_1(I,R, I,Ni); + send_2(R,S, R, Nr, {I,Ni}k(R,S) ); + read_4(I,R, {I,Kir,Nr}k(R,S) , {Nr}Kir ); - claim_R1(R, Secret,Kir); + claim_R1(R, Secret,Kir); claim_R2(R, Nisynch); - } + } - role S - { - const Kir: Key; - var Ni,Nr: Nonce; + role S + { + const Kir: Key; + var Ni,Nr: Nonce; - read_2(R,S, R, {I,Ni,Nr}k(R,S) ); - send_3(S,I, {R,Kir,Ni,Nr}k(I,S), {I,Kir}k(R,S) ); - } + read_2(R,S, R, {I,Ni,Nr}k(R,S) ); + send_3(S,I, {R,Kir,Ni,Nr}k(I,S), {I,Kir}k(R,S) ); + } } const Alice,Bob,Simon : Agent; diff --git a/spdl/SPORE/yahalom-lowe.spdl b/spdl/SPORE/yahalom-lowe.spdl index ab0c6e5..65790f9 100644 --- a/spdl/SPORE/yahalom-lowe.spdl +++ b/spdl/SPORE/yahalom-lowe.spdl @@ -12,44 +12,44 @@ usertype Key; protocol yahalomLowe(I,R,S) { - role I - { - const Ni: Nonce; - var Nr: Nonce; - var Kir: Key; + role I + { + const Ni: Nonce; + var Nr: Nonce; + var Kir: Key; - send_1(I,R, I,Ni); - read_3(S,I, {R,Kir,Ni,Nr}k(I,S) ); - send_5(I,R, {I, R, S, Nr}Kir ); + send_1(I,R, I,Ni); + read_3(S,I, {R,Kir,Ni,Nr}k(I,S) ); + send_5(I,R, {I, R, S, Nr}Kir ); - claim_I1(I, Secret,Kir); - claim_I2(I, Nisynch); - } + claim_I1(I, Secret,Kir); + claim_I2(I, Nisynch); + } - role R - { - const Nr: Nonce; - var Ni: Nonce; - var Kir: Key; + role R + { + const Nr: Nonce; + var Ni: Nonce; + var Kir: Key; - read_1(I,R, I,Ni); - send_2(R,S, {I,Ni,Nr}k(R,S) ); - read_4(S,R, {I,Kir}k(R,S)); - read_5(I,R, {I, R, S, Nr}Kir); + read_1(I,R, I,Ni); + send_2(R,S, {I,Ni,Nr}k(R,S) ); + read_4(S,R, {I,Kir}k(R,S)); + read_5(I,R, {I, R, S, Nr}Kir); - claim_R1(R, Secret,Kir); + claim_R1(R, Secret,Kir); claim_R2(R, Nisynch); - } + } - role S - { - const Kir: Key; - var Ni,Nr: Nonce; + role S + { + const Kir: Key; + var Ni,Nr: Nonce; - read_2(R,S, {I,Ni,Nr}k(R,S) ); - send_3(S,I, {R,Kir,Ni,Nr}k(I,S)); + read_2(R,S, {I,Ni,Nr}k(R,S) ); + send_3(S,I, {R,Kir,Ni,Nr}k(I,S)); send_4(S,R, {I,Kir}k(R,S)); - } + } } const Alice,Bob,Simon : Agent; diff --git a/spdl/SPORE/yahalom-paulson.spdl b/spdl/SPORE/yahalom-paulson.spdl index bed720d..b94aa96 100644 --- a/spdl/SPORE/yahalom-paulson.spdl +++ b/spdl/SPORE/yahalom-paulson.spdl @@ -15,44 +15,44 @@ usertype Ticket, Key; protocol yahalomPaulson(I,R,S) { - role I - { - const Ni: Nonce; - var Nr: Nonce; - var T: Ticket; - var Kir: Key; + role I + { + const Ni: Nonce; + var Nr: Nonce; + var T: Ticket; + var Kir: Key; - send_1(I,R, I,Ni); - read_3(S,I, Nr, {R,Kir,Ni}k(I,S), T ); - send_4(I,R, T, {Nr}Kir ); + send_1(I,R, I,Ni); + read_3(S,I, Nr, {R,Kir,Ni}k(I,S), T ); + send_4(I,R, T, {Nr}Kir ); - claim_I1(I, Secret,Kir); - claim_I2(I, Nisynch); - } + claim_I1(I, Secret,Kir); + claim_I2(I, Nisynch); + } - role R - { - const Nr: Nonce; - var Ni: Nonce; - var T: Ticket; - var Kir: Key; + role R + { + const Nr: Nonce; + var Ni: Nonce; + var T: Ticket; + var Kir: Key; - read_1(I,R, I,Ni); - send_2(R,S, R, Nr, {I,Ni}k(R,S) ); - read_4(I,R, {I,R, Kir, Nr}k(R,S) , {Nr}Kir ); + read_1(I,R, I,Ni); + send_2(R,S, R, Nr, {I,Ni}k(R,S) ); + read_4(I,R, {I,R, Kir, Nr}k(R,S) , {Nr}Kir ); - claim_R1(R, Secret,Kir); + claim_R1(R, Secret,Kir); claim_R2(R, Nisynch); - } + } - role S - { - const Kir: Key; - var Ni,Nr: Nonce; + role S + { + const Kir: Key; + var Ni,Nr: Nonce; - read_2(R,S, R, Nr, {I,Ni}k(R,S) ); - send_3(S,I, Nr, {R,Kir,Ni}k(I,S), {I,R,Kir,Nr}k(R,S) ); - } + read_2(R,S, R, Nr, {I,Ni}k(R,S) ); + send_3(S,I, Nr, {R,Kir,Ni}k(I,S), {I,R,Kir,Nr}k(R,S) ); + } } const Alice,Bob,Simon : Agent; diff --git a/spdl/SPORE/yahalom.spdl b/spdl/SPORE/yahalom.spdl index 126f5f3..d30354c 100644 --- a/spdl/SPORE/yahalom.spdl +++ b/spdl/SPORE/yahalom.spdl @@ -15,44 +15,44 @@ usertype Ticket, Key; protocol yahalom(I,R,S) { - role I - { - const Ni: Nonce; - var Nr: Nonce; - var T: Ticket; - var Kir: Key; + role I + { + const Ni: Nonce; + var Nr: Nonce; + var T: Ticket; + var Kir: Key; - send_1(I,R, I,Ni); - read_3(S,I, {R,Kir,Ni,Nr}k(I,S), T ); - send_4(I,R, T, {Nr}Kir ); + send_1(I,R, I,Ni); + read_3(S,I, {R,Kir,Ni,Nr}k(I,S), T ); + send_4(I,R, T, {Nr}Kir ); - claim_I1(I, Secret,Kir); - claim_I2(I, Nisynch); - } + claim_I1(I, Secret,Kir); + claim_I2(I, Nisynch); + } - role R - { - const Nr: Nonce; - var Ni: Nonce; - var T: Ticket; - var Kir: Key; + role R + { + const Nr: Nonce; + var Ni: Nonce; + var T: Ticket; + var Kir: Key; - read_1(I,R, I,Ni); - send_2(R,S, R, {I,Ni,Nr}k(R,S) ); - read_4(I,R, {I,Kir}k(R,S) , {Nr}Kir ); + read_1(I,R, I,Ni); + send_2(R,S, R, {I,Ni,Nr}k(R,S) ); + read_4(I,R, {I,Kir}k(R,S) , {Nr}Kir ); - claim_R1(R, Secret,Kir); + claim_R1(R, Secret,Kir); claim_R2(R, Nisynch); - } + } - role S - { - const Kir: Key; - var Ni,Nr: Nonce; + role S + { + const Kir: Key; + var Ni,Nr: Nonce; - read_2(R,S, R, {I,Ni,Nr}k(R,S) ); - send_3(S,I, {R,Kir,Ni,Nr}k(I,S), {I,Kir}k(R,S) ); - } + read_2(R,S, R, {I,Ni,Nr}k(R,S) ); + send_3(S,I, {R,Kir,Ni,Nr}k(I,S), {I,Kir}k(R,S) ); + } } const Alice,Bob,Simon : Agent;