Files used in lecture 13:

qlock0.maude
qlock.maude
nspk.maude
nspk.mod
invariants.mod
template.mod
proof1.mod
proof2.mod
proof3.mod
proof4.mod
proof5.mod
proof5-1.mod

 

Possible solustions of the exercise of lecture 13:

nspk-for-secrecy.maude