Verification of language-based opacity in Petri nets using verifier
SEATZU, CARLA;GIUA, ALESSANDRO
2016-01-01
Abstract
A system is said to be language opaque if the intruder cannot infer if the generated event sequence belongs to a secret based on its partial observation. In this paper we address the problem of verifying language-based opacity in systems modeled by bounded labeled Petri nets. We generalize the notion of language opacity to strict language opacity to deal with the case where the intruder is only interested in a subset of transitions. Furthermore, we show that strict language opacity is identical to language opacity for a special class of secrets. A verifier is constructed to analyze strict language opacity under the assumption that the intruder only cares about observable transitions.File | Size | Format | |
---|---|---|---|
16acc_draft.pdf Solo gestori archivio
Type: versione post-print
Size 414.93 kB
Format Adobe PDF
|
414.93 kB | Adobe PDF | & nbsp; View / Open Request a copy |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.