提出了一种适用于带有时间戳的安全协议的有色Petri（CPN）形式化分析方法，利用一个非自动时钟来描述协议中涉及的时间因素。对著名的WMF协议建模，利用CPNTools，采用CPNML语言编写查询函数验证协议的新鲜性，从而发现协议的漏洞。应用分析结果表明该方法有效，且操作简单容易理解。