[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] FW: access list question with pvs file



I attached the wrong file yesterday.


From: Long Duong [mailto:long@xxxxxxxxxxxxxxxxxxxx]
Sent: Wednesday, May 21, 2008 12:55 PM
To: 'pvs-help@xxxxxxxxxxx'
Subject: access list question with pvs file




I realize my attempt yesterday at asking my question didn’t have enough

information so I’m sending my pvs file with the question again.


I’m trying to construct a machine that keeps a running list of add requests

from arbitrary users modeled as nat IDs. When the machine encounters a

later  access request by that same ID, the access is allowed.  I’m trying

to prove that any given access allowed through to the machine output must

have been preceded by a previous [add ID] machine input, see theorem




in the attached pvs file.


I’m having a hard time trying to prove this.  Thank you for any help with the

proof or with any suggestion for a better model.


Long Duong, Ph.D

RedPhone Security



Attachment: prog_filter.pvs
Description: Binary data