Title :
Computational Semantics of a Verification Logic of Local Sessions
Author_Institution :
Dept. of Comput. Sci., Guangdong Polytech. Normal Univ., Guangzhou, China
Abstract :
We propose a computational semantics for a previously developed protocol security logic, Logic of Local Sessions (LLS), replacing its earlier symbolic semantics based on the Dolev-Yao model. With the new semantics, the protocol verification of LLS is more close to the real execution, while the proofs can still be carried out at a symbolic level using the original proof system and the automatic verification tool. Our results hold under standard cryptographic assumptions.
Keywords :
cryptographic protocols; formal verification; theorem proving; Dolev-Yao model; LLS; automatic verification tool; computational semantics; cryptographic assumptions; proof system; protocol security logic; protocol verification; symbolic semantics; verification logic of local sessions; Computational model; Computational semantics; Indistinguishability; Logic of Local Sessions;
Conference_Titel :
Computational and Information Sciences (ICCIS), 2013 Fifth International Conference on
Conference_Location :
Shiyang
DOI :
10.1109/ICCIS.2013.224
