DRM Paradiso Formal Analysis

mCRL spec/analysis demonstrating the replay attack on the original NPGCT protocol. The attack trace can be found here.
mCRL spec/analysis demonstrating the unfair situation attack on the original NPGCT protocol. The attack trace can be found here.
mCRL spec/analysis to verify correct working of the new Nuovo protocol.

$Id: formal.php,v 1.6 2010/02/05 09:14:22 srijith Exp $

If you would like to get a masters degree in our department, check out the (English-language) program in Parallel and Distributed Systems.