diff --git a/spdl/simplest.spdl b/spdl/simplest.spdl new file mode 100644 index 0000000..22f3f62 --- /dev/null +++ b/spdl/simplest.spdl @@ -0,0 +1,19 @@ + +secret k: Nonce; +const Alice,Bob,Charlie: Agent; +const ne: Nonce; + +protocol simplest(I) +{ + role I + { + var x: Nonce; + const n: Nonce; + + read(I,I, x); + send(I,I, n, {n, x}k ); + } +} + +run simplest.I(Alice); +run simplest.I(Alice);