Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

10

FUIN
2008

favoriteEmaildiscussreport

103views more FUIN 2008»

LDYIS: a Framework for Model Checking Security Protocols

13 years 4 months ago

LDYIS: a Framework for Model Checking Security Protocols

Download www.doc.ic.ac.uk

We present a formalism for the automatic verification of security protocols based on multi-agent systems semantics. We give the syntax and semantics of a temporal-epistemic securityspecialised logic and provide a lazy-intruder model for the protocol rules that we argue to be particularly suitable for verification purposes. We exemplify the technique by finding a (known) bug in the traditional NSPK protocol.

Alessio Lomuscio, Wojciech Penczek

Real-time Traffic

Automatic Verification | FUIN 2008 | Multi-agent Systems Semantics | Temporal-epistemic Securityspecialised Logic |

claim paper

Related Content

» ASPIER An Automated Framework for Verifying Security Protocol Implementations

» LTL Model Checking for Security Protocols

» SLEDE lightweight verification of sensor network security protocol implementations

» Security protocols properties and their monitoring

» ModelBased Design and Analysis of PermissionBased Security

» Synthesis of attack actions using model checking for the verification of security protocol...

» SATBased ModelChecking of Security Protocols Using Planning Graph Analysis

» A MachineChecked Formalization of the Random Oracle Model

» Formal Security Analysis with Interacting State Machines

Post Info
More Details (n/a)

Added	10 Dec 2010
Updated	10 Dec 2010
Type	Journal
Year	2008
Where	FUIN
Authors	Alessio Lomuscio, Wojciech Penczek

Comments (0)