در حال نمایش موارد 1 - 5 از 5
A Decentralized Online Sortition Protocol
(Iranian Society of Cryptology, 2018-01-01)
We propose a new online sortition protocol which is decentralized. We argue that our protocol has safety, fairness, randomness, non-reputation and openness properties. Sortition is a process that makes random decision and ...
A computational model and convergence theorem for rumor dissemination in social networks
(Iranian Society of Cryptology, 2013-07-01)
The spread of rumors, which are known as unverified statements of uncertain origin, may threaten the society and it's controlling, is important for national security councils of countries. If it would be possible to identify ...
Process algebraic modeling of authentication protocols for analysis of parallel multi-session executions
(Iranian Society of Cryptology, 2009-01-01)
Many security protocols have the aim of authenticating one agent acting as initiator to another agent acting as responder and vice versa. Sometimes, the authentication fails because of executing several parallel sessions of a protocol, and because an agent may play both the initiator and responder role in parallel sessions. We take advantage of the notion of transition systems to specify authentication for parallel multiple session's execution. To model the authentication, two main notions called 1. agent's scope and 2. agent's recognizability are introduced, which consider the difference of ability of agents due to their different roles in the protocol and different access to keys and secrets. To formalize above notions, a process algebra provided by some primitives for manipulating cryptographic messages is used. We formalize some security protocols and examine our definition of authentication for them. We just discuss the symmetric key case....
A short introduction to two approaches in formal verification of security protocols: model checking and theorem proving
(Iranian Society of Cryptology, 2016-01-01)
In this paper, we shortly review two formal approaches in verification of security protocols; model checking and theorem proving. Model checking is based on studying the behavior of protocols via generating all different behaviors of a protocol and checking whether the desired goals are satisfied in all instances or not. We investigate Scyther operational semantics as n example of this approach and then we model and verify some famous security protocols using Scyther. Theorem proving is based on deriving the desired goals from assumption of protocols via a deduction system. We define a deduction system named Simple Logic for Authentication to formally define the notion of authenticated communication based on the structure of the messages, and then we several famous protocols using our proposed deduction system and compare it with the verification results of Scyther model checking....
Distributed Contingency Logic and Security
(Iranian Society of Cryptology, 2018-07-01)
In information security, ignorance is not bliss. It is always stated that hiding the protocols (let the other be ignorant about it) does not increase the security of organizations. However, there are cases that ignorance ...