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

Oops,

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

Hi,

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

add_access_order

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

651.204.3372

Attachment: prog_filter.pvs
Description: Binary data