Show simple item record

dc.contributor.author
Mödersheim, Sebastian
dc.date.accessioned
2017-08-14T09:58:01Z
dc.date.available
2017-06-10T19:31:43Z
dc.date.available
2017-08-14T09:58:01Z
dc.date.issued
2011
dc.identifier.uri
http://hdl.handle.net/20.500.11850/69791
dc.identifier.doi
10.3929/ethz-a-006775802
dc.description.abstract
We formally investigate the relationship between several models that are widely used in protocol verification, namely variants of the inductive model of message traces inspired by Paulson’s approach, and models based on rewriting. More precisely, we prove several overapproximation relationships between models, i.e. that one model allows strictly more traces or reachable states than the other. This is common in verification: often an over-approximation is easier to prove correct than the original model, and proving the over-approximation is safe implies that the original model is safe—provided that the models are indeed in an overapproximation relation. We also show that some over-approximations are not sound with respect to authentication goals. The precise formal account that we give on the relation of the models allows us to correct the situation.
en_US
dc.format
application/pdf
dc.language.iso
en
en_US
dc.publisher
ETH, Department of Computer Science
en_US
dc.rights.uri
http://rightsstatements.org/page/InC-NC/1.0/
dc.subject
VERIFICATION (SOFTWARE ENGINEERING)
en_US
dc.subject
NETWORK PROTOCOLS + COMMUNICATION PROTOCOLS (COMPUTER SYSTEMS)
en_US
dc.subject
NETZWERKPROTOKOLLE + KOMMUNIKATIONSPROTOKOLLE (COMPUTERSYSTEME)
en_US
dc.subject
VERIFIKATION (SOFTWARE ENGINEERING)
en_US
dc.title
On the relationships between models in protocol verification (extended version)
en_US
dc.type
Report
dc.rights.license
In Copyright - Non-Commercial Use Permitted
ethz.journal.title
Technical report
ethz.journal.volume
512, rev.1.2
en_US
ethz.size
26 p.
en_US
ethz.code.ddc
DDC - DDC::0 - Computer science, information & general works::004 - Data processing, computer science
en_US
ethz.notes
Technical Reports D-INFK.
en_US
ethz.identifier.nebis
006775802
ethz.publication.place
Zurich
en_US
ethz.publication.status
published
en_US
ethz.leitzahl
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science
en_US
ethz.date.deposited
2017-06-10T19:34:36Z
ethz.source
ECOL
ethz.source
ECIT
ethz.identifier.importid
imp59366b15636c924840
ethz.identifier.importid
imp593650d3a955e44165
ethz.ecolpid
eth:4808
ethz.ecitpid
pub:110500
ethz.eth
yes
en_US
ethz.availability
Open access
en_US
ethz.rosetta.installDate
2017-07-26T15:15:23Z
ethz.rosetta.lastUpdated
2020-02-15T06:44:26Z
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.atitle=On%20the%20relationships%20between%20models%20in%20protocol%20verification%20(extended%20version)&rft.jtitle=Technical%20report&rft.date=2011&rft.volume=512,%20rev.1.2&rft.au=M%C3%B6dersheim,%20Sebastian&rft.genre=report&
 Search via SFX

Files in this item

Thumbnail

Publication type

Show simple item record