Open AccessOn the Reachability Problem in Cryptographic Protocols
Author(s) -
Roberto M. Amadio,
Denis Lugiez
Publication year - 2000
Publication title -
lecture notes in computer science
Language(s) - English
Resource type - Book series
SCImago Journal Rank - 0.249
H-Index - 400
eISSN - 1611-3349
pISSN - 0302-9743
ISBN - 3-540-67897-2
DOI - 10.1007/3-540-44618-4_28
Subject(s) - reachability , computer science , secrecy , cryptographic protocol , adversary , cryptography , cryptographic primitive , protocol (science) , theoretical computer science , reduction (mathematics) , model checking , state (computer science) , symmetric key algorithm , programming language , computer security , public key cryptography , mathematics , encryption , medicine , alternative medicine , geometry , pathology
We study the verification of secrecy and authenticity properties for cryptographic protocols which rely on symmetric shared keys. The verification can be reduced to check whether a certain parallel program which models the protocol and the specification can reach an erroneous state while interacting with an adversary. Assuming finite principals, we present a decision procedure for the reachability problem which is based on a 'symbolic' reduction system.
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom