Commit c759543a authored by acholewa's avatar acholewa

Removed the composition specifications (which haven't been implemented yet)...

Removed the composition specifications (which haven't been implemented yet) from our examples folder.
parent fc709c75
spec NSL;DB is
composing NSL ; DB .
A ;1 B : A |-> B, B |-> A, N |-> n(A, r) .
B ;1 A : A |-> B, B |-> A1, N |-> NA1 .
Attacks
0 .
B.NSL executes up to 2 .
Intruder learns n(B.NSL, r1) .
//Tells us how we should instantiate the attack strand.
Subst(B.NSL) = B |-> b, A1 |-> a .
ends
spec NSL;KD is
composing NSL ; KD .
//nsl-A ;* kd-B kd-A
nsl-init ;* kd-resp : A |-> B, B |-> A, K |-> h(n(A, r) ; NB), K2 |-> key .
nsl-init ;* kd-init : A |-> A, B |-> B, K |-> key, K2 |-> h(n(A, r) ; NB) .
nsl-B ;* kd-A : A |-> B, B |-> A1, K |-> h(NA1 ; n(B, r1)) .
nsl-B ;* kd-B : A |-> A1, B |-> B, K |-> h(NA1 ; n(B, r1)) .
ends
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment