diff --git a/spdl/kaochow-palm.spdl b/spdl/kaochow-palm.spdl new file mode 100644 index 0000000..d74fbf9 --- /dev/null +++ b/spdl/kaochow-palm.spdl @@ -0,0 +1,34 @@ +usertype Sessionkey; +secret k: Function; + +protocol kaochowPalm(I,R,S) +{ + role I + { + const ni: Nonce; + var X: Nonce; + var KX: Sessionkey; + + } + + role R + { + } + + role S + { + } +} + +const Alice,Bob,Simon,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +compromised sk(Eve); + +run kaochowPalm.I(Agent,Agent,Simon); +run kaochowPalm.R(Agent,Agent,Simon); +run kaochowPalm.S(Agent,Agent,Simon); +run kaochowPalm.I(Agent,Agent,Simon); +run kaochowPalm.R(Agent,Agent,Simon); +run kaochowPalm.S(Agent,Agent,Simon);