loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2009 International Conference on Availability, Reliability and Security
Algebraic Properties in Alice and Bob Notation
Fukuoka Institute of Technology, Fukuoka, Japan
March 16-March 19
ISBN: 978-0-7695-3564-7
Alice and Bob notation is a popular way to describe security protocols: it is intuitive, succinct, and yet expressive. Several formal protocol specification languages are based on this notation. One of the most severe limitations of these languages is the lack of algebraic reasoning, which is required for instance for the correct interpretation of Diffie-Hellman based protocols. As a consequence, previous approaches either cannot handle such protocols at all or require manual annotation. We generalize previous approaches and give the first formal semantics for a language based on Alice and Bob notation that is defined over an arbitrary algebraic theory. In particular, it defines unambiguously how the protocol is supposed to be executed by honest agents, based on the considered algebraic properties of the operators.
Index Terms:
Protocol Verifcation, Alice and Bob, Algebraic Reasoning, Semantics
Citation:
Sebastian Mödersheim, "Algebraic Properties in Alice and Bob Notation," ares, pp.433-440, 2009 International Conference on Availability, Reliability and Security, 2009
Usage of this product signifies your acceptance of the Terms of Use.