Verification of current-state opacity using Petri nets