Deciding Security for a Fragment of ASLan

Publication: ResearchReport – Annual report year: 2012

Documents

View graph of relations

ASLan is the input language of the verification tools of the AVANTSSAR platform, and an extension of the AVISPA Intermediate Format IF. One of ASLan's core features over IF is to integrate a transition system with Horn clauses that are evaluated at every state. This allows for modeling many common situations in security such as the interaction between the work ow of a system with its access control policies.
While even the transition relation is undecidable for ASLan in general, we show the security problem is decidable for a large and useful fragment that we call TASLan, as long as we bound the number of steps of honest participants. The restriction of TASLan is that all messages and predicates must be in a certain sense unambiguous in their interpretation, excluding \type-confusions" similar to some tagging results for security protocols.
Original languageEnglish
Publication date2012
PublisherTechnical University of Denmark
Number of pages24
StatePublished
NameIMM-Technical Report-2012
Number06
Download as:
Download as PDF
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
Word

Download statistics

No data available

ID: 9709978