Formal Specification and Verification of Modular Security Policy Based on Colored Petri Nets

2011 ◽  
Vol 8 (6) ◽  
pp. 852-865 ◽  
Author(s):  
Hejiao Huang ◽  
H. Kirchner
Keyword(s):  
Petri Nets ◽  
Formal Specification ◽  
Security Policy ◽  
Colored Petri Nets ◽  
Formal Specification And Verification ◽  
Specification And Verification

scholarly journals Enhancing formal specification and verification of e-commerce protocol

2017 ◽  
Vol 6 (1) ◽  
pp. 13
Author(s):  
Hasan Al-Refai ◽  
Khaldoun Batiha
Keyword(s):  
Formal Specification ◽  
Electronic Payment ◽  
Complex Phase ◽  
Transaction Process ◽  
Protocol Performance ◽  
Formal Specification And Verification ◽  
Security Properties ◽  
Set Protocol ◽  
Specification And Verification

Lots of work have been attempted to enhance the SET protocol performance special attention is on E-payment phase. This paper thoroughly analyzes recent works on payment phase; it has been found that this subject requires considerable enhancements, since there are areas, which require further study such as: E-payment phase in SET protocol.E-payment phase is vast and complex phase it has long series of steps. The behavior of environment is assumed by the phase and is restricted to the rules built by their proposed protocol. This paper will follow Ph-Spi calculus for formalizing and analyzing enhanced payment phase of SET protocol by reducing the number of transactions with many additional operators.A new agent controller will be formally modeled, which we can rely upon to make automated decisions during interaction with a dynamic protocol environment. So, this agent controller is used to terminate the transaction process in any case of fraud or attack. This paper is conjunction between our previous works of E-payment phase in SET protocol and other works in Ph-Spi calculus in purpose of analyzing and proving the main security properties: authentication and privacy to evaluate the efficiency of the enhanced security of electronic payment phase for SET protocol (E-SET) using Ph-Spi calculus.

Sign in / Sign up

Export Citation Format

Share Document